:: AMISTD_1 semantic presentation

REAL is non empty non trivial non finite V46() V47() V48() V52() V55() V56() V58() non with_non-empty_elements non empty-membered set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal V46() V47() V48() V49() V50() V51() V52() V53() V55() non with_non-empty_elements non empty-membered countable denumerable Element of bool REAL
bool REAL is non empty non trivial non finite non empty-membered set
omega is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal V46() V47() V48() V49() V50() V51() V52() V53() V55() non with_non-empty_elements non empty-membered countable denumerable set
bool omega is non empty non trivial non finite non empty-membered set
bool NAT is non empty non trivial non finite non empty-membered set
COMPLEX is non empty non trivial non finite V46() V52() non empty-membered set
RAT is non empty non trivial non finite V46() V47() V48() V49() V52() non empty-membered set
INT is non empty non trivial non finite V46() V47() V48() V49() V50() V52() non empty-membered set
{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial V16() V17() Function-like one-to-one constant functional finite finite-yielding V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative V46() V47() V48() V49() V50() V51() V52() V55() V56() V57() V58() initial Cardinal-yielding countable V138() V139() Function-yielding V153() V154() set
the Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial V16() V17() Function-like one-to-one constant functional finite finite-yielding V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative V46() V47() V48() V49() V50() V51() V52() V55() V56() V57() V58() initial Cardinal-yielding countable V138() V139() Function-yielding V153() V154() set is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial V16() V17() Function-like one-to-one constant functional finite finite-yielding V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non negative V46() V47() V48() V49() V50() V51() V52() V55() V56() V57() V58() initial Cardinal-yielding countable V138() V139() Function-yielding V153() V154() set
2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
ExtREAL is non empty V47() V58() set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial V16() V17() Function-like one-to-one constant functional finite finite-yielding V30() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V41() ext-real non negative V46() V47() V48() V49() V50() V51() V52() V55() V56() V57() V58() initial Cardinal-yielding countable V113() V138() V139() Function-yielding V153() V154() Element of NAT
{0} is non empty trivial functional finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() with_common_domain countable Element of bool NAT
[0,{},{}] is V23() V24() set
[0,{}] is non empty V23() set
{0,{}} is non empty functional finite V30() V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable set
{0} is non empty trivial functional finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() with_common_domain countable set
{{0,{}},{0}} is non empty finite V30() with_non-empty_elements non empty-membered countable set
[[0,{}],{}] is non empty V23() set
{[0,{}],{}} is non empty finite countable set
{[0,{}]} is Relation-like non empty trivial Function-like constant finite 1 -element with_non-empty_elements non empty-membered countable V139() set
{{[0,{}],{}},{[0,{}]}} is non empty finite V30() with_non-empty_elements non empty-membered countable set
{[0,{},{}]} is Relation-like non empty trivial finite 1 -element standard-ins homogeneous J/A-independent V71() countable set
0 .--> 0 is Relation-like NAT -defined {0} -defined NAT -valued non empty trivial Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V139() Function-yielding V153() set
{0} --> 0 is Relation-like {0} -defined NAT -valued {0} -valued non empty Function-like constant finite total quasi_total Cardinal-yielding countable V139() Function-yielding V153() Element of bool [:{0},{0}:]
[:{0},{0}:] is Relation-like non empty finite countable set
bool [:{0},{0}:] is non empty finite V30() countable set
III is non empty non with_non-empty_elements set
N is with_non-empty_values AMI-Struct over III
the InstructionsF of N is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the carrier of N is set
the_Values_of N is Relation-like non-empty the carrier of N -defined Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined III -valued Function-like total quasi_total Element of bool [: the carrier of N,III:]
[: the carrier of N,III:] is Relation-like set
bool [: the carrier of N,III:] is non empty set
the ValuesF of N is Relation-like III -defined non empty Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined Function-like total set
product ( the Object-Kind of N * the ValuesF of N) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) is non empty functional set
the Execution of N is Relation-like the InstructionsF of N -defined Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):]
[: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is Relation-like non empty set
bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is non empty set
S is Element of the InstructionsF of N
the Execution of N . S is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))
s is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total set
( the Execution of N . S) . s is set
product (the_Values_of N) is non empty functional with_common_domain product-like set
[:(product (the_Values_of N)),(product (the_Values_of N)):] is Relation-like non empty set
bool [:(product (the_Values_of N)),(product (the_Values_of N)):] is non empty set
P is Relation-like product (the_Values_of N) -defined product (the_Values_of N) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [:(product (the_Values_of N)),(product (the_Values_of N)):]
c₆ is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total Element of product (the_Values_of N)
P . c₆ is Relation-like the carrier of N -defined Function-like the_Values_of N -compatible total Element of product (the_Values_of N)
III is non empty non with_non-empty_elements set
Trivial-AMI III is non empty trivial finite 1 -element with_non-empty_values IC-Ins-separated strict halting AMI-Struct over III
III is non empty non with_non-empty_elements set
N is non empty with_non-empty_values AMI-Struct over III
the InstructionsF of N is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
InsCodes the InstructionsF of N is non empty set
K78( the InstructionsF of N) is set
dom the InstructionsF of N is non empty set
dom (dom the InstructionsF of N) is set
III is non empty non with_non-empty_elements set
N is non empty with_non-empty_values AMI-Struct over III
the InstructionsF of N is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
III is non empty non with_non-empty_elements set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over III
the InstructionsF of N is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the carrier of N is non empty set
the_Values_of N is Relation-like non-empty non empty-yielding the carrier of N -defined non empty Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined III -valued non empty Function-like total quasi_total Element of bool [: the carrier of N,III:]
[: the carrier of N,III:] is Relation-like non empty set
bool [: the carrier of N,III:] is non empty set
the ValuesF of N is Relation-like III -defined non empty Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined non empty Function-like total set
product (the_Values_of N) is non empty functional with_common_domain product-like set
s is Element of the InstructionsF of N
S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable set
{ (IC (Exec (s,b₁))) where b₁ is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total Element of product (the_Values_of N) : IC b₁ = S } is set
P is set
c₆ is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total Element of product (the_Values_of N)
Exec (s,c₆) is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set
product ( the Object-Kind of N * the ValuesF of N) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) is non empty functional set
the Execution of N is Relation-like the InstructionsF of N -defined Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):]
[: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is Relation-like non empty set
bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is non empty set
the Execution of N . s is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))
( the Execution of N . s) . c₆ is Relation-like Function-like set
IC (Exec (s,c₆)) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
IC is V85(N) Element of the carrier of N
the ZeroF of N is Element of the carrier of N
(Exec (s,c₆)) . (IC ) is set
IC c₆ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
c₆ . (IC ) is set
III is non empty non with_non-empty_elements set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over III
the InstructionsF of N is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the carrier of N is non empty set
the_Values_of N is Relation-like non-empty non empty-yielding the carrier of N -defined non empty Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined III -valued non empty Function-like total quasi_total Element of bool [: the carrier of N,III:]
[: the carrier of N,III:] is Relation-like non empty set
bool [: the carrier of N,III:] is non empty set
the ValuesF of N is Relation-like III -defined non empty Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined non empty Function-like total set
product (the_Values_of N) is non empty functional with_common_domain product-like set
P is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set
IC is V85(N) Element of the carrier of N
the ZeroF of N is Element of the carrier of N
s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
P +* ((IC ),s) is Relation-like the carrier of N -defined the carrier of N -defined non empty Function-like the_Values_of N -compatible total total set
c₆ is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set
dom c₆ is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
dom P is non empty Element of bool the carrier of N
bool the carrier of N is non empty set
s is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total Element of product (the_Values_of N)
IC s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s . (IC ) is set
S is Element of the InstructionsF of N
c₆ +* (s,S) is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set
CurInstr ((c₆ +* (s,S)),s) is Element of the InstructionsF of N
(c₆ +* (s,S)) /. (IC s) is Element of the InstructionsF of N
(c₆ +* (s,S)) . s is Element of the InstructionsF of N
Following ((c₆ +* (s,S)),(P +* ((IC ),s))) is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set
CurInstr ((c₆ +* (s,S)),(P +* ((IC ),s))) is Element of the InstructionsF of N
IC (P +* ((IC ),s)) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(P +* ((IC ),s)) . (IC ) is set
(c₆ +* (s,S)) /. (IC (P +* ((IC ),s))) is Element of the InstructionsF of N
Exec ((CurInstr ((c₆ +* (s,S)),(P +* ((IC ),s)))),(P +* ((IC ),s))) is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set
product ( the Object-Kind of N * the ValuesF of N) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) is non empty functional set
the Execution of N is Relation-like the InstructionsF of N -defined Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):]
[: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is Relation-like non empty set
bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is non empty set
the Execution of N . (CurInstr ((c₆ +* (s,S)),(P +* ((IC ),s)))) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))
( the Execution of N . (CurInstr ((c₆ +* (s,S)),(P +* ((IC ),s))))) . (P +* ((IC ),s)) is Relation-like Function-like set
IC (Following ((c₆ +* (s,S)),(P +* ((IC ),s)))) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(Following ((c₆ +* (s,S)),(P +* ((IC ),s)))) . (IC ) is set
(III,N,s,S) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ (IC (Exec (S,b₁))) where b₁ is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total Element of product (the_Values_of N) : IC b₁ = s } is set
III is non empty non with_non-empty_elements set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over III
the InstructionsF of N is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
S is Element of the InstructionsF of N
(III,N,s,S) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
the carrier of N is non empty set
the_Values_of N is Relation-like non-empty non empty-yielding the carrier of N -defined non empty Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined III -valued non empty Function-like total quasi_total Element of bool [: the carrier of N,III:]
[: the carrier of N,III:] is Relation-like non empty set
bool [: the carrier of N,III:] is non empty set
the ValuesF of N is Relation-like III -defined non empty Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined non empty Function-like total set
product (the_Values_of N) is non empty functional with_common_domain product-like set
{ (IC (Exec (S,b₁))) where b₁ is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total Element of product (the_Values_of N) : IC b₁ = s } is set
III is non empty non with_non-empty_elements set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over III
the InstructionsF of N is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
S is Element of the InstructionsF of N
{ (III,N,b₁,S) where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT : verum } is set
meet { (III,N,b₁,S) where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT : verum } is set
bool NAT is non empty non trivial non finite non empty-membered Element of bool (bool NAT)
bool (bool NAT) is non empty non trivial non finite non empty-membered set
P is set
c₆ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(III,N,c₆,S) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
the carrier of N is non empty set
the_Values_of N is Relation-like non-empty non empty-yielding the carrier of N -defined non empty Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined III -valued non empty Function-like total quasi_total Element of bool [: the carrier of N,III:]
[: the carrier of N,III:] is Relation-like non empty set
bool [: the carrier of N,III:] is non empty set
the ValuesF of N is Relation-like III -defined non empty Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined non empty Function-like total set
product (the_Values_of N) is non empty functional with_common_domain product-like set
{ (IC (Exec (S,b₁))) where b₁ is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total Element of product (the_Values_of N) : IC b₁ = c₆ } is set
P is Element of bool (bool NAT)
meet P is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
III is non empty non with_non-empty_elements set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over III
the InstructionsF of N is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable set
{ ((III,N,S,b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
union { ((III,N,S,b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
bool NAT is non empty non trivial non finite non empty-membered Element of bool (bool NAT)
bool (bool NAT) is non empty non trivial non finite non empty-membered set
P is set
c₆ is Element of the InstructionsF of N
(III,N,S,c₆) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
the carrier of N is non empty set
the_Values_of N is Relation-like non-empty non empty-yielding the carrier of N -defined non empty Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined III -valued non empty Function-like total quasi_total Element of bool [: the carrier of N,III:]
[: the carrier of N,III:] is Relation-like non empty set
bool [: the carrier of N,III:] is non empty set
the ValuesF of N is Relation-like III -defined non empty Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined non empty Function-like total set
product (the_Values_of N) is non empty functional with_common_domain product-like set
{ (IC (Exec (c₆,b₁))) where b₁ is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total Element of product (the_Values_of N) : IC b₁ = S } is set
(III,N,c₆) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ (III,N,b₁,c₆) where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT : verum } is set
meet { (III,N,b₁,c₆) where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT : verum } is set
(III,N,S,c₆) \ (III,N,c₆) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
P is Element of bool (bool NAT)
union P is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
III is non empty non with_non-empty_elements set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over III
the InstructionsF of N is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
S is Element of the InstructionsF of N
(III,N,S) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ (III,N,b₁,S) where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT : verum } is set
meet { (III,N,b₁,S) where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT : verum } is set
kk is set
s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(III,N,s,S) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
the carrier of N is non empty set
the_Values_of N is Relation-like non-empty non empty-yielding the carrier of N -defined non empty Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined III -valued non empty Function-like total quasi_total Element of bool [: the carrier of N,III:]
[: the carrier of N,III:] is Relation-like non empty set
bool [: the carrier of N,III:] is non empty set
the ValuesF of N is Relation-like III -defined non empty Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined non empty Function-like total set
product (the_Values_of N) is non empty functional with_common_domain product-like set
{ (IC (Exec (S,b₁))) where b₁ is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total Element of product (the_Values_of N) : IC b₁ = s } is set
{s} is non empty trivial finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(III,N,s,S) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
{ (IC (Exec (S,b₁))) where b₁ is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total Element of product (the_Values_of N) : IC b₁ = s } is set
{s} is non empty trivial finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
III is non empty non with_non-empty_elements set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over III
the InstructionsF of N is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
{S} is non empty trivial finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
s is Element of the InstructionsF of N
(III,N,S,s) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
the carrier of N is non empty set
the_Values_of N is Relation-like non-empty non empty-yielding the carrier of N -defined non empty Function-like total set
the Object-Kind of N is Relation-like the carrier of N -defined III -valued non empty Function-like total quasi_total Element of bool [: the carrier of N,III:]
[: the carrier of N,III:] is Relation-like non empty set
bool [: the carrier of N,III:] is non empty set
the ValuesF of N is Relation-like III -defined non empty Function-like total set
the Object-Kind of N * the ValuesF of N is Relation-like the carrier of N -defined non empty Function-like total set
product (the_Values_of N) is non empty functional with_common_domain product-like set
{ (IC (Exec (s,b₁))) where b₁ is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total Element of product (the_Values_of N) : IC b₁ = S } is set
P is set
c₆ is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total Element of product (the_Values_of N)
Exec (s,c₆) is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set
product ( the Object-Kind of N * the ValuesF of N) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) is non empty functional set
the Execution of N is Relation-like the InstructionsF of N -defined Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):]
[: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is Relation-like non empty set
bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is non empty set
the Execution of N . s is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))
( the Execution of N . s) . c₆ is Relation-like Function-like set
IC (Exec (s,c₆)) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
IC is V85(N) Element of the carrier of N
the ZeroF of N is Element of the carrier of N
(Exec (s,c₆)) . (IC ) is set
IC c₆ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
c₆ . (IC ) is set
the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set
the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set
s is set
dom the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
IC is V85(N) Element of the carrier of N
the ZeroF of N is Element of the carrier of N
dom the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set is non empty Element of bool the carrier of N
bool the carrier of N is non empty set
the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S) is Relation-like the carrier of N -defined the carrier of N -defined non empty Function-like the_Values_of N -compatible total total set
IC ( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S)) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S)) . (IC ) is set
the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set +* (S,s) is Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set
CurInstr (( the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set +* (S,s)),( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S))) is Element of the InstructionsF of N
( the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set +* (S,s)) /. (IC ( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S))) is Element of the InstructionsF of N
( the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set +* (S,s)) . S is Element of the InstructionsF of N
Following (( the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set +* (S,s)),( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S))) is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set
Exec ((CurInstr (( the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set +* (S,s)),( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S)))),( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S))) is Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set
product ( the Object-Kind of N * the ValuesF of N) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) is non empty functional set
the Execution of N is Relation-like the InstructionsF of N -defined Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):]
[: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is Relation-like non empty set
bool [: the InstructionsF of N,(Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))):] is non empty set
the Execution of N . (CurInstr (( the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set +* (S,s)),( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S)))) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of N * the ValuesF of N)),(product ( the Object-Kind of N * the ValuesF of N)))
( the Execution of N . (CurInstr (( the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set +* (S,s)),( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S))))) . ( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S)) is Relation-like Function-like set
IC (Following (( the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set +* (S,s)),( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S)))) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(Following (( the Relation-like NAT -defined the InstructionsF of N -valued non empty Function-like total set +* (S,s)),( the Relation-like the carrier of N -defined non empty Function-like the_Values_of N -compatible total set +* ((IC ),S)))) . (IC ) is set
III is non empty non with_non-empty_elements set
III is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
<*s*> is Relation-like NAT -defined NAT -valued non empty trivial Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V139() FinSequence of NAT
P is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V139() FinSequence of NAT
P /. 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
len P is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
P /. (len P) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
c₆ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
c₆ + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
P /. (c₆ + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
P /. c₆ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(N,S,(P /. c₆)) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
{ ((N,S,(P /. c₆),b₁) \ (N,S,b₁)) where b₁ is Element of the InstructionsF of S : verum } is set
union { ((N,S,(P /. c₆),b₁) \ (N,S,b₁)) where b₁ is Element of the InstructionsF of S : verum } is set
III is non empty non with_non-empty_elements set
N is non empty with_non-empty_values IC-Ins-separated AMI-Struct over III
S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
S + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
s is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V139() FinSequence of NAT
s /. 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
len s is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
s /. (len s) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s -| (S + 1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V139() set
(S + 1) .. s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
rng s is non empty finite V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
len (s -| (S + 1)) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
((S + 1) .. s) - 1 is V16() V17() ext-real set
(len (s -| (S + 1))) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
dom s is non empty finite V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
s /. ((len (s -| (S + 1))) + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s . ((S + 1) .. s) is set
s . 1 is set
s is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V139() FinSequence of NAT
len s is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
s /. (len s) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
dom s is non empty finite V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
s /. (len s) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s . (len s) is set
s . (len s) is set
rng s is non empty finite V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
{(S + 1)} is non empty trivial finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() with_non-empty_elements non empty-membered countable Element of bool NAT
(rng s) /\ {(S + 1)} is finite V46() V47() V48() V49() V50() V51() V55() V56() V57() countable Element of bool NAT
kk is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s /. ((S + 1) .. s) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
<*(s /. (len s)),(s /. ((S + 1) .. s))*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V139() FinSequence of NAT
P is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V139() FinSequence of NAT
len P is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
dom P is non empty finite V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
P /. (len P) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
P . 2 is set
u is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
P /. u is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
P . 1 is set
u + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
P /. (u + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(len s) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
s /. ((len s) + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(III,N,(P /. u)) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
the InstructionsF of N is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
{ ((III,N,(P /. u),b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
union { ((III,N,(P /. u),b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
u is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
u + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
s /. u is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s . u is set
s . u is set
s /. u is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s /. (u + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s . (u + 1) is set
s . (u + 1) is set
s /. (u + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(III,N,(s /. u)) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ ((III,N,(s /. u),b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
union { ((III,N,(s /. u),b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
P /. 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s /. 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s . 1 is set
(III,N,S) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ ((III,N,S,b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
union { ((III,N,S,b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
u is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
<*y,t*> is Relation-like NAT -defined NAT -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V139() FinSequence of NAT
c₁₄ is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V139() FinSequence of NAT
len c₁₄ is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
dom c₁₄ is non empty finite V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
c₁₄ /. 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
c₁₄ . 1 is set
n is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
c₁₄ /. n is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
c₁₄ /. (n + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
c₁₄ . 2 is set
(III,N,(c₁₄ /. n)) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ ((III,N,(c₁₄ /. n),b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
union { ((III,N,(c₁₄ /. n),b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
c₁₄ /. (len c₁₄) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s -' S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(s -' S) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
c₆ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V139() FinSequence of NAT
len c₆ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
dom c₆ is finite V46() V47() V48() V49() V50() V51() V55() V56() V57() countable Element of bool NAT
s is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V139() FinSequence of NAT
s /. 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
len s is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
s /. (len s) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
dom s is non empty finite V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
s . 1 is set
S + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
(S + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s - S is V16() V17() ext-real set
s . (len s) is set
S + ((s -' S) + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
(S + ((s -' S) + 1)) -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
S + (s -' S) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(S + (s -' S)) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
((S + (s -' S)) + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
s /. (s + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s /. s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(III,N,(s /. s)) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ ((III,N,(s /. s),b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
union { ((III,N,(s /. s),b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
s . s is set
S + s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(S + s) -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s . (s + 1) is set
S + (s + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
(S + (s + 1)) -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(S + s) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
((S + s) + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
((S + s) -' 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
P is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like Cardinal-yielding countable V139() FinSequence of NAT
P /. 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
len P is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
P /. (len P) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
c₆ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
P /. c₆ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
c₆ + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable V113() Element of NAT
P /. (c₆ + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
P /. (c₆ + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
(III,N,(P /. c₆)) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ ((III,N,(P /. c₆),b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
union { ((III,N,(P /. c₆),b₁) \ (III,N,b₁)) where b₁ is Element of the InstructionsF of N : verum } is set
kk is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
P /. (c₆ + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
P /. (c₆ + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
P /. 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
c₆ is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
[:NAT,NAT,NAT:] is non empty set
[1,0,0] is V23() V24() Element of [:NAT,NAT,NAT:]
[1,0] is non empty V23() set
{1,0} is non empty finite V30() V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable set
{1} is non empty trivial finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() with_non-empty_elements non empty-membered countable set
{{1,0},{1}} is non empty finite V30() with_non-empty_elements non empty-membered countable set
[[1,0],0] is non empty V23() set
{[1,0],0} is non empty finite countable set
{[1,0]} is Relation-like non empty trivial Function-like constant finite 1 -element with_non-empty_elements non empty-membered countable V139() set
{{[1,0],0},{[1,0]}} is non empty finite V30() with_non-empty_elements non empty-membered countable set
[0,0,0] is V23() V24() Element of [:NAT,NAT,NAT:]
[0,0] is non empty V23() set
{0,0} is non empty functional finite V30() V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable set
{{0,0},{0}} is non empty finite V30() with_non-empty_elements non empty-membered countable set
[[0,0],0] is non empty V23() set
{[0,0],0} is non empty finite countable set
{[0,0]} is Relation-like non empty trivial Function-like constant finite 1 -element with_non-empty_elements non empty-membered countable V139() set
{{[0,0],0},{[0,0]}} is non empty finite V30() with_non-empty_elements non empty-membered countable set
{[1,0,0],[0,0,0]} is Relation-like non empty finite standard-ins homogeneous J/A-independent V71() countable Element of bool [:NAT,NAT,NAT:]
bool [:NAT,NAT,NAT:] is non empty set
N is non empty non with_non-empty_elements set
{[0,0,0],[1,0,0]} is Relation-like non empty finite standard-ins homogeneous J/A-independent V71() countable Element of bool [:NAT,NAT,NAT:]
N --> NAT is Relation-like non-empty non empty-yielding N -defined bool REAL -valued non empty Function-like constant total quasi_total Cardinal-yielding Element of bool [:N,(bool REAL):]
[:N,(bool REAL):] is Relation-like non empty non trivial non finite non empty-membered set
bool [:N,(bool REAL):] is non empty non trivial non finite non empty-membered set
{NAT} is non empty trivial finite 1 -element with_non-empty_elements non empty-membered countable set
[:N,{NAT}:] is Relation-like non empty set
(0 .--> 0) * (N --> NAT) is Relation-like non-empty NAT -defined bool REAL -valued Function-like finite countable V139() set
0 .--> NAT is Relation-like NAT -defined {0} -defined bool REAL -valued non empty trivial Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V139() set
{0} --> NAT is Relation-like non-empty non empty-yielding {0} -defined bool REAL -valued {NAT} -valued non empty Function-like constant finite total quasi_total Cardinal-yielding countable V139() Element of bool [:{0},{NAT}:]
[:{0},{NAT}:] is Relation-like non empty finite countable set
bool [:{0},{NAT}:] is non empty finite V30() countable set
dom ((0 .--> 0) * (N --> NAT)) is trivial functional finite V30() V46() V47() V48() V49() V50() V51() V55() V56() V57() with_common_domain countable Element of bool {0}
bool {0} is non empty finite V30() countable set
dom (0 .--> 0) is non empty trivial functional finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() with_common_domain countable Element of bool {0}
rng (0 .--> 0) is non empty trivial finite 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
[:{0},N:] is Relation-like non empty set
bool [:{0},N:] is non empty set
s is Relation-like {0} -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [:{0},N:]
(N --> NAT) * s is Relation-like non-empty non empty-yielding {0} -defined bool REAL -valued non empty Function-like finite total quasi_total countable V139() Element of bool [:{0},(bool REAL):]
[:{0},(bool REAL):] is Relation-like non empty non trivial non finite non empty-membered set
bool [:{0},(bool REAL):] is non empty non trivial non finite non empty-membered set
product ((N --> NAT) * s) is non empty functional with_common_domain product-like set
s is Relation-like {0} -defined non empty Function-like (N --> NAT) * s -compatible total V139() Element of product ((N --> NAT) * s)
s . 0 is set
succ (s . 0) is non empty set
0 .--> (succ (s . 0)) is Relation-like NAT -defined {0} -defined non empty trivial Function-like one-to-one constant finite 1 -element countable V139() set
{0} --> (succ (s . 0)) is Relation-like non-empty non empty-yielding {0} -defined {(succ (s . 0))} -valued non empty Function-like constant finite total quasi_total countable V139() Element of bool [:{0},{(succ (s . 0))}:]
{(succ (s . 0))} is non empty trivial finite 1 -element with_non-empty_elements non empty-membered countable set
[:{0},{(succ (s . 0))}:] is Relation-like non empty finite countable set
bool [:{0},{(succ (s . 0))}:] is non empty finite V30() countable set
s +* (0 .--> (succ (s . 0))) is Relation-like non empty Function-like set
dom (s +* (0 .--> (succ (s . 0)))) is non empty trivial functional finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() with_common_domain countable Element of bool {0}
dom s is non empty trivial functional finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() with_common_domain countable Element of bool {0}
bool {0} is non empty finite V30() countable set
dom (0 .--> (succ (s . 0))) is non empty trivial functional finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() with_common_domain countable Element of bool {0}
(dom s) \/ (dom (0 .--> (succ (s . 0)))) is non empty trivial functional finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() with_common_domain countable Element of bool {0}
(dom s) \/ {0} is non empty finite V30() V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable set
{0} \/ {0} is non empty finite V30() V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
dom ((N --> NAT) * s) is non empty trivial functional finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() with_common_domain countable Element of bool {0}
kk is set
((N --> NAT) * s) . kk is set
(s +* (0 .--> (succ (s . 0)))) . kk is set
(0 .--> (succ (s . 0))) . kk is set
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative V46() V47() V48() V49() V50() V51() V55() V56() V57() countable V113() Element of NAT
succ P is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative countable set
P + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative V46() V47() V48() V49() V50() V51()