:: 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() V53() V54() V55() V56() V57() countable V113() Element of NAT
[:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):] is Relation-like non empty set
bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):] is non empty set
s is Relation-like product ((N --> NAT) * s) -defined product ((N --> NAT) * s) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):]
[1,0,0] .--> s is Relation-like [:NAT,NAT,NAT:] -defined {[1,0,0]} -defined bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[1,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins countable set
{[1,0,0]} --> s is Relation-like non-empty non empty-yielding {[1,0,0]} -defined bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):] -valued {s} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[1,0,0]},{s}:]
{s} is non empty trivial functional finite 1 -element with_non-empty_elements non empty-membered with_common_domain countable set
[:{[1,0,0]},{s}:] is Relation-like non empty finite countable set
bool [:{[1,0,0]},{s}:] is non empty finite V30() countable set
id (product ((N --> NAT) * s)) is Relation-like product ((N --> NAT) * s) -defined product ((N --> NAT) * s) -valued non empty Function-like one-to-one total quasi_total onto bijective V128() V130() V131() V135() Function-yielding V153() Element of bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):]
[0,0,0] .--> (id (product ((N --> NAT) * s))) is Relation-like [:NAT,NAT,NAT:] -defined {[0,0,0]} -defined bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[0,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins homogeneous J/A-independent V71() countable set
{[0,0,0]} --> (id (product ((N --> NAT) * s))) is Relation-like non-empty non empty-yielding {[0,0,0]} -defined bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):] -valued {(id (product ((N --> NAT) * s)))} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[0,0,0]},{(id (product ((N --> NAT) * s)))}:]
{(id (product ((N --> NAT) * s)))} is non empty trivial functional finite 1 -element with_non-empty_elements non empty-membered with_common_domain countable set
[:{[0,0,0]},{(id (product ((N --> NAT) * s)))}:] is Relation-like non empty finite countable set
bool [:{[0,0,0]},{(id (product ((N --> NAT) * s)))}:] is non empty finite V30() countable set
([1,0,0] .--> s) +* ([0,0,0] .--> (id (product ((N --> NAT) * s)))) is Relation-like [:NAT,NAT,NAT:] -defined bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):] -valued non empty Function-like finite countable V139() Function-yielding V153() set
dom (([1,0,0] .--> s) +* ([0,0,0] .--> (id (product ((N --> NAT) * s))))) is non empty finite countable set
dom ([1,0,0] .--> s) is Relation-like non empty trivial finite 1 -element countable Element of bool {[1,0,0]}
bool {[1,0,0]} is non empty finite V30() countable set
dom ([0,0,0] .--> (id (product ((N --> NAT) * s)))) is Relation-like non empty trivial finite 1 -element countable Element of bool {[0,0,0]}
bool {[0,0,0]} is non empty finite V30() countable set
(dom ([1,0,0] .--> s)) \/ (dom ([0,0,0] .--> (id (product ((N --> NAT) * s))))) is Relation-like non empty finite countable set
{[1,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins countable Element of bool [:NAT,NAT,NAT:]
{[1,0,0]} \/ (dom ([0,0,0] .--> (id (product ((N --> NAT) * s))))) is Relation-like non empty finite countable set
{[0,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins homogeneous J/A-independent V71() countable Element of bool [:NAT,NAT,NAT:]
{[1,0,0]} \/ {[0,0,0]} is Relation-like non empty finite countable Element of bool [:NAT,NAT,NAT:]
rng ([1,0,0] .--> s) is non empty trivial finite 1 -element countable Element of bool (bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):])
bool (bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):]) is non empty set
{s} is non empty trivial functional finite 1 -element with_non-empty_elements non empty-membered with_common_domain countable Element of bool (bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):])
rng ([0,0,0] .--> (id (product ((N --> NAT) * s)))) is non empty trivial finite 1 -element countable Element of bool (bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):])
{(id (product ((N --> NAT) * s)))} is non empty trivial functional finite 1 -element with_non-empty_elements non empty-membered with_common_domain countable Element of bool (bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):])
rng (([1,0,0] .--> s) +* ([0,0,0] .--> (id (product ((N --> NAT) * s))))) is non empty finite countable Element of bool (bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):])
(rng ([1,0,0] .--> s)) \/ (rng ([0,0,0] .--> (id (product ((N --> NAT) * s))))) is non empty finite countable Element of bool (bool [:(product ((N --> NAT) * s)),(product ((N --> NAT) * s)):])
Funcs ((product ((N --> NAT) * s)),(product ((N --> NAT) * s))) is non empty functional FUNCTION_DOMAIN of product ((N --> NAT) * s), product ((N --> NAT) * s)
P is set
[:{[1,0,0],[0,0,0]},(Funcs ((product ((N --> NAT) * s)),(product ((N --> NAT) * s)))):] is Relation-like non empty set
bool [:{[1,0,0],[0,0,0]},(Funcs ((product ((N --> NAT) * s)),(product ((N --> NAT) * s)))):] is non empty set
P is Relation-like epsilon-transitive epsilon-connected ordinal natural V16() V17() Function-like finite cardinal V41() ext-real non negative countable V113() V139() Element of {0}
P is Relation-like {[1,0,0],[0,0,0]} -defined Funcs ((product ((N --> NAT) * s)),(product ((N --> NAT) * s))) -valued non empty Function-like finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[1,0,0],[0,0,0]},(Funcs ((product ((N --> NAT) * s)),(product ((N --> NAT) * s)))):]
AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) is strict AMI-Struct over N
the carrier of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) is set
the ZeroF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) is Element of the carrier of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #)
the InstructionsF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) is Relation-like the carrier of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) -defined N -valued Function-like total quasi_total Element of bool [: the carrier of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #),N:]
[: the carrier of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #),N:] is Relation-like set
bool [: the carrier of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #),N:] is non empty set
the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) is Relation-like N -defined non empty Function-like total set
the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) is Relation-like the carrier of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) -defined Function-like total set
the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) is Relation-like the carrier of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) -defined Function-like total set
product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #)) is functional with_common_domain product-like set
[:(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))):] is Relation-like set
bool [:(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))):] is non empty set
the Execution of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) is Relation-like the InstructionsF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) -defined Funcs ((product ( the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product ( the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #)))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #),(Funcs ((product ( the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product ( the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))))):]
product ( the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #)) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product ( the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #)))) is non empty functional set
[: the InstructionsF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #),(Funcs ((product ( the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product ( the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))))):] is Relation-like non empty set
bool [: the InstructionsF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #),(Funcs ((product ( the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product ( the Object-Kind of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #) * the ValuesF of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))))):] is non empty set
id (product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))) is Relation-like product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #)) -defined product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #)) -valued Function-like one-to-one total quasi_total onto bijective V128() V130() V131() V135() Function-yielding V153() Element of bool [:(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))):]
[0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #)))) is Relation-like [:NAT,NAT,NAT:] -defined {[0,0,0]} -defined bool [:(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[0,0,0]} --> (id (product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #)))) is Relation-like {[0,0,0]} -defined bool [:(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))):] -valued {(id (product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))))} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[0,0,0]},{(id (product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))))}:]
{(id (product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))))} is non empty trivial functional finite 1 -element with_common_domain countable set
[:{[0,0,0]},{(id (product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))))}:] is Relation-like non empty finite countable set
bool [:{[0,0,0]},{(id (product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))))}:] is non empty finite V30() countable set
t is Relation-like product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #)) -defined product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #)) -valued Function-like total quasi_total Function-yielding V153() Element of bool [:(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))):]
[1,0,0] .--> t is Relation-like [:NAT,NAT,NAT:] -defined {[1,0,0]} -defined bool [:(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[1,0,0]} --> t is Relation-like {[1,0,0]} -defined bool [:(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))):] -valued {t} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[1,0,0]},{t}:]
{t} is non empty trivial functional finite 1 -element with_common_domain countable set
[:{[1,0,0]},{t}:] is Relation-like non empty finite countable set
bool [:{[1,0,0]},{t}:] is non empty finite V30() countable set
([1,0,0] .--> t) +* ([0,0,0] .--> (id (product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))))) is Relation-like [:NAT,NAT,NAT:] -defined bool [:(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))),(product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))):] -valued non empty Function-like finite countable V139() Function-yielding V153() set
c₁₄ is Relation-like Function-like Element of product (the_Values_of AMI-Struct(# {0},P,{[1,0,0],[0,0,0]},s,(N --> NAT),P #))
t . c₁₄ is Relation-like Function-like set
c₁₄ . 0 is set
succ (c₁₄ . 0) is non empty set
0 .--> (succ (c₁₄ . 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 (c₁₄ . 0)) is Relation-like non-empty non empty-yielding {0} -defined {(succ (c₁₄ . 0))} -valued non empty Function-like constant finite total quasi_total countable V139() Element of bool [:{0},{(succ (c₁₄ . 0))}:]
{(succ (c₁₄ . 0))} is non empty trivial finite 1 -element with_non-empty_elements non empty-membered countable set
[:{0},{(succ (c₁₄ . 0))}:] is Relation-like non empty finite countable set
bool [:{0},{(succ (c₁₄ . 0))}:] is non empty finite V30() countable set
c₁₄ +* (0 .--> (succ (c₁₄ . 0))) is Relation-like non empty Function-like set
S is strict AMI-Struct over N
the carrier of S is set
the ZeroF of S is Element of the carrier of S
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued Function-like total quasi_total Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like set
bool [: the carrier of S,N:] is non empty set
the ValuesF of S is Relation-like N -defined non empty Function-like total set
the_Values_of S is Relation-like the carrier of S -defined Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined Function-like total set
product (the_Values_of S) is functional with_common_domain product-like set
[:(product (the_Values_of S)),(product (the_Values_of S)):] is Relation-like set
bool [:(product (the_Values_of S)),(product (the_Values_of S)):] is non empty set
the Execution of S is Relation-like the InstructionsF of S -defined Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):]
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
[: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is Relation-like non empty set
bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is non empty set
id (product (the_Values_of S)) is Relation-like product (the_Values_of S) -defined product (the_Values_of S) -valued Function-like one-to-one total quasi_total onto bijective V128() V130() V131() V135() Function-yielding V153() Element of bool [:(product (the_Values_of S)),(product (the_Values_of S)):]
[0,0,0] .--> (id (product (the_Values_of S))) is Relation-like [:NAT,NAT,NAT:] -defined {[0,0,0]} -defined bool [:(product (the_Values_of S)),(product (the_Values_of S)):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[0,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins homogeneous J/A-independent V71() countable set
{[0,0,0]} --> (id (product (the_Values_of S))) is Relation-like {[0,0,0]} -defined bool [:(product (the_Values_of S)),(product (the_Values_of S)):] -valued {(id (product (the_Values_of S)))} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[0,0,0]},{(id (product (the_Values_of S)))}:]
{(id (product (the_Values_of S)))} is non empty trivial functional finite 1 -element with_common_domain countable set
[:{[0,0,0]},{(id (product (the_Values_of S)))}:] is Relation-like non empty finite countable set
bool [:{[0,0,0]},{(id (product (the_Values_of S)))}:] is non empty finite V30() countable set
s is strict AMI-Struct over N
the carrier of s is set
the ZeroF of s is Element of the carrier of s
the InstructionsF of s is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the Object-Kind of s is Relation-like the carrier of s -defined N -valued Function-like total quasi_total Element of bool [: the carrier of s,N:]
[: the carrier of s,N:] is Relation-like set
bool [: the carrier of s,N:] is non empty set
the ValuesF of s is Relation-like N -defined non empty Function-like total set
the_Values_of s is Relation-like the carrier of s -defined Function-like total set
the Object-Kind of s * the ValuesF of s is Relation-like the carrier of s -defined Function-like total set
product (the_Values_of s) is functional with_common_domain product-like set
[:(product (the_Values_of s)),(product (the_Values_of s)):] is Relation-like set
bool [:(product (the_Values_of s)),(product (the_Values_of s)):] is non empty set
the Execution of s is Relation-like the InstructionsF of s -defined Funcs ((product ( the Object-Kind of s * the ValuesF of s)),(product ( the Object-Kind of s * the ValuesF of s))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of s,(Funcs ((product ( the Object-Kind of s * the ValuesF of s)),(product ( the Object-Kind of s * the ValuesF of s)))):]
product ( the Object-Kind of s * the ValuesF of s) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of s * the ValuesF of s)),(product ( the Object-Kind of s * the ValuesF of s))) is non empty functional set
[: the InstructionsF of s,(Funcs ((product ( the Object-Kind of s * the ValuesF of s)),(product ( the Object-Kind of s * the ValuesF of s)))):] is Relation-like non empty set
bool [: the InstructionsF of s,(Funcs ((product ( the Object-Kind of s * the ValuesF of s)),(product ( the Object-Kind of s * the ValuesF of s)))):] is non empty set
id (product (the_Values_of s)) is Relation-like product (the_Values_of s) -defined product (the_Values_of s) -valued Function-like one-to-one total quasi_total onto bijective V128() V130() V131() V135() Function-yielding V153() Element of bool [:(product (the_Values_of s)),(product (the_Values_of s)):]
[0,0,0] .--> (id (product (the_Values_of s))) is Relation-like [:NAT,NAT,NAT:] -defined {[0,0,0]} -defined bool [:(product (the_Values_of s)),(product (the_Values_of s)):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[0,0,0]} --> (id (product (the_Values_of s))) is Relation-like {[0,0,0]} -defined bool [:(product (the_Values_of s)),(product (the_Values_of s)):] -valued {(id (product (the_Values_of s)))} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[0,0,0]},{(id (product (the_Values_of s)))}:]
{(id (product (the_Values_of s)))} is non empty trivial functional finite 1 -element with_common_domain countable set
[:{[0,0,0]},{(id (product (the_Values_of s)))}:] is Relation-like non empty finite countable set
bool [:{[0,0,0]},{(id (product (the_Values_of s)))}:] is non empty finite V30() countable set
P is Relation-like product (the_Values_of S) -defined product (the_Values_of S) -valued Function-like total quasi_total Function-yielding V153() Element of bool [:(product (the_Values_of S)),(product (the_Values_of S)):]
[1,0,0] .--> P is Relation-like [:NAT,NAT,NAT:] -defined {[1,0,0]} -defined bool [:(product (the_Values_of S)),(product (the_Values_of S)):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[1,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins countable set
{[1,0,0]} --> P is Relation-like {[1,0,0]} -defined bool [:(product (the_Values_of S)),(product (the_Values_of S)):] -valued {P} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[1,0,0]},{P}:]
{P} is non empty trivial functional finite 1 -element with_common_domain countable set
[:{[1,0,0]},{P}:] is Relation-like non empty finite countable set
bool [:{[1,0,0]},{P}:] is non empty finite V30() countable set
([1,0,0] .--> P) +* ([0,0,0] .--> (id (product (the_Values_of S)))) is Relation-like [:NAT,NAT,NAT:] -defined bool [:(product (the_Values_of S)),(product (the_Values_of S)):] -valued non empty Function-like finite countable V139() Function-yielding V153() set
c₆ is Relation-like product (the_Values_of s) -defined product (the_Values_of s) -valued Function-like total quasi_total Function-yielding V153() Element of bool [:(product (the_Values_of s)),(product (the_Values_of s)):]
[1,0,0] .--> c₆ is Relation-like [:NAT,NAT,NAT:] -defined {[1,0,0]} -defined bool [:(product (the_Values_of s)),(product (the_Values_of s)):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[1,0,0]} --> c₆ is Relation-like {[1,0,0]} -defined bool [:(product (the_Values_of s)),(product (the_Values_of s)):] -valued {c₆} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[1,0,0]},{c₆}:]
{c₆} is non empty trivial functional finite 1 -element with_common_domain countable set
[:{[1,0,0]},{c₆}:] is Relation-like non empty finite countable set
bool [:{[1,0,0]},{c₆}:] is non empty finite V30() countable set
([1,0,0] .--> c₆) +* ([0,0,0] .--> (id (product (the_Values_of s)))) is Relation-like [:NAT,NAT,NAT:] -defined bool [:(product (the_Values_of s)),(product (the_Values_of s)):] -valued non empty Function-like finite countable V139() Function-yielding V153() set
s is Relation-like Function-like Element of product (the_Values_of S)
P . s is Relation-like Function-like set
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
c₆ . s is Relation-like Function-like set
N is non empty non with_non-empty_elements set
(N) is strict AMI-Struct over N
N is non empty non with_non-empty_elements set
(N) is non empty finite strict AMI-Struct over N
S is set
the_Values_of (N) is Relation-like the carrier of (N) -defined non empty Function-like total V139() set
the carrier of (N) is non empty finite countable set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() set
dom (the_Values_of (N)) is non empty set
(the_Values_of (N)) . S is set
dom (the_Values_of (N)) is non empty finite countable Element of bool the carrier of (N)
bool the carrier of (N) is non empty finite V30() countable set
the Object-Kind of (N) . S is set
dom the ValuesF of (N) is non empty Element of bool N
bool N is non empty set
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
[:N,{NAT}:] is Relation-like non empty set
the ValuesF of (N) . ( the Object-Kind of (N) . S) is set
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values strict AMI-Struct over N
the_Values_of (N) is Relation-like non-empty non empty-yielding the carrier of (N) -defined non empty Function-like total V139() set
the carrier of (N) is non empty finite countable set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() set
(0 .--> 0) * the ValuesF of (N) is Relation-like NAT -defined Function-like finite countable V139() set
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
[: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
(the_Values_of (N)) . 0 is 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
(0 .--> NAT) . 0 is set
IC is V85((N)) Element of the carrier of (N)
the ZeroF of (N) is Element of the carrier of (N)
Values (IC ) is non empty set
(the_Values_of (N)) . (IC ) is non empty set
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict AMI-Struct over N
the InstructionsF of (N) is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the carrier of (N) is non empty finite countable set
the_Values_of (N) is Relation-like non-empty non empty-yielding the carrier of (N) -defined non empty Function-like total V139() set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() set
IC is V85((N)) Element of the carrier of (N)
the ZeroF of (N) is Element of the carrier of (N)
S is Element of the InstructionsF of (N)
InsCode S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68(S) is set
K68(K68(S)) is set
s is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set
Exec (S,s) is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() 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) . s is Relation-like Function-like set
(Exec (S,s)) . (IC ) is 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
s . (IC ) is set
succ (IC s) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative countable set
(IC 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
{[0,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins homogeneous J/A-independent V71() countable Element of bool [:NAT,NAT,NAT:]
{[1,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins countable Element of bool [:NAT,NAT,NAT:]
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
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}
bool {0} is non empty finite V30() countable 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
id (product (the_Values_of (N))) is Relation-like product (the_Values_of (N)) -defined product (the_Values_of (N)) -valued non empty Function-like one-to-one total quasi_total onto bijective V128() V130() V131() V135() Function-yielding V153() Element of bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):]
[0,0,0] .--> (id (product (the_Values_of (N)))) is Relation-like [:NAT,NAT,NAT:] -defined {[0,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[0,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins homogeneous J/A-independent V71() countable set
{[0,0,0]} --> (id (product (the_Values_of (N)))) is Relation-like non-empty non empty-yielding {[0,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued {(id (product (the_Values_of (N))))} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[0,0,0]},{(id (product (the_Values_of (N))))}:]
{(id (product (the_Values_of (N))))} is non empty trivial functional finite 1 -element with_non-empty_elements non empty-membered with_common_domain countable set
[:{[0,0,0]},{(id (product (the_Values_of (N))))}:] is Relation-like non empty finite countable set
bool [:{[0,0,0]},{(id (product (the_Values_of (N))))}:] is non empty finite V30() countable set
c₆ 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))):]
[1,0,0] .--> c₆ is Relation-like [:NAT,NAT,NAT:] -defined {[1,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[1,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins countable set
{[1,0,0]} --> c₆ is Relation-like non-empty non empty-yielding {[1,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued {c₆} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[1,0,0]},{c₆}:]
{c₆} is non empty trivial functional finite 1 -element with_non-empty_elements non empty-membered with_common_domain countable set
[:{[1,0,0]},{c₆}:] is Relation-like non empty finite countable set
bool [:{[1,0,0]},{c₆}:] is non empty finite V30() countable set
([1,0,0] .--> c₆) +* ([0,0,0] .--> (id (product (the_Values_of (N))))) is Relation-like [:NAT,NAT,NAT:] -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued non empty Function-like finite countable V139() Function-yielding V153() set
s is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set
c₆ . s is Relation-like Function-like set
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
s is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() Element of product (the_Values_of (N))
c₆ . s is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() Element of product (the_Values_of (N))
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 ([0,0,0] .--> (id (product (the_Values_of (N))))) is Relation-like non empty trivial finite 1 -element countable Element of bool {[0,0,0]}
bool {[0,0,0]} is non empty finite V30() countable set
([1,0,0] .--> c₆) . S is Relation-like Function-like set
s +* (0 .--> (succ (s . 0))) is Relation-like non empty Function-like set
(s +* (0 .--> (succ (s . 0)))) . 0 is set
(0 .--> (succ (s . 0))) . 0 is set
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict AMI-Struct over N
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)
InsCode S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68(S) is set
K68(K68(S)) is set
{[0,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins homogeneous J/A-independent V71() countable Element of bool [:NAT,NAT,NAT:]
the carrier of (N) is non empty finite countable set
the_Values_of (N) is Relation-like non-empty non empty-yielding the carrier of (N) -defined non empty Function-like total V139() set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() set
P is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set
Exec (S,P) is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() 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) . P is Relation-like Function-like 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
id (product (the_Values_of (N))) is Relation-like product (the_Values_of (N)) -defined product (the_Values_of (N)) -valued non empty Function-like one-to-one total quasi_total onto bijective V128() V130() V131() V135() Function-yielding V153() Element of bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):]
[0,0,0] .--> (id (product (the_Values_of (N)))) is Relation-like [:NAT,NAT,NAT:] -defined {[0,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[0,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins homogeneous J/A-independent V71() countable set
{[0,0,0]} --> (id (product (the_Values_of (N)))) is Relation-like non-empty non empty-yielding {[0,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued {(id (product (the_Values_of (N))))} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[0,0,0]},{(id (product (the_Values_of (N))))}:]
{(id (product (the_Values_of (N))))} is non empty trivial functional finite 1 -element with_non-empty_elements non empty-membered with_common_domain countable set
[:{[0,0,0]},{(id (product (the_Values_of (N))))}:] is Relation-like non empty finite countable set
bool [:{[0,0,0]},{(id (product (the_Values_of (N))))}:] is non empty finite V30() countable set
dom ([0,0,0] .--> (id (product (the_Values_of (N))))) is Relation-like non empty trivial finite 1 -element countable Element of bool {[0,0,0]}
bool {[0,0,0]} is non empty finite V30() countable set
{[0,0,0]} --> (id (product (the_Values_of (N)))) is Relation-like non-empty non empty-yielding {[0,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[0,0,0]},(bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):]):]
[:{[0,0,0]},(bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):]):] is Relation-like non empty set
bool [:{[0,0,0]},(bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):]):] is non empty set
[:{[0,0,0]},{(id (product (the_Values_of (N))))}:] is Relation-like non empty finite countable set
({[0,0,0]} --> (id (product (the_Values_of (N))))) . S is Relation-like Function-like set
s 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))):]
[1,0,0] .--> s is Relation-like [:NAT,NAT,NAT:] -defined {[1,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[1,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins countable set
{[1,0,0]} --> s is Relation-like non-empty non empty-yielding {[1,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued {s} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[1,0,0]},{s}:]
{s} is non empty trivial functional finite 1 -element with_non-empty_elements non empty-membered with_common_domain countable set
[:{[1,0,0]},{s}:] is Relation-like non empty finite countable set
bool [:{[1,0,0]},{s}:] is non empty finite V30() countable set
([1,0,0] .--> s) +* ([0,0,0] .--> (id (product (the_Values_of (N))))) is Relation-like [:NAT,NAT,NAT:] -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued non empty Function-like finite countable V139() Function-yielding V153() set
c₆ is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() Element of product (the_Values_of (N))
( the Execution of (N) . S) . c₆ is Relation-like Function-like set
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict AMI-Struct over N
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)
InsCode S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68(S) is set
K68(K68(S)) is set
the carrier of (N) is non empty finite countable set
the_Values_of (N) is Relation-like non-empty non empty-yielding the carrier of (N) -defined non empty Function-like total V139() set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() set
the Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set
Exec (S, the Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set ) is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() 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) . the Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set is Relation-like Function-like set
IC is V85((N)) Element of the carrier of (N)
the ZeroF of (N) is Element of the carrier of (N)
(Exec (S, the Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set )) . (IC ) is set
IC the Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set 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 V139() set . (IC ) is set
succ (IC the Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set ) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative countable set
(IC the Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() 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
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict AMI-Struct over N
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)
InsCode S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68(S) is set
K68(K68(S)) is set
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict AMI-Struct over N
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)
the carrier of (N) is non empty finite countable set
the_Values_of (N) is Relation-like non-empty non empty-yielding the carrier of (N) -defined non empty Function-like total V139() set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() set
InsCode S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68(S) is set
K68(K68(S)) is set
NonZero (N) is finite countable Element of bool the carrier of (N)
bool the carrier of (N) is non empty finite V30() countable set
[#] (N) is non empty non proper finite countable Element of bool the carrier of (N)
IC is V85((N)) Element of the carrier of (N)
the ZeroF of (N) is Element of the carrier of (N)
{(IC )} is non empty trivial finite 1 -element countable set
([#] (N)) \ {(IC )} is finite countable Element of bool the carrier of (N)
P is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set
c₆ is Element of the carrier of (N)
P . c₆ is set
s is Element of the InstructionsF of (N)
InsCode s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
K68(s) is set
K68(K68(s)) is set
Exec (s,P) is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() 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) . P is Relation-like Function-like set
(Exec (s,P)) . c₆ is set
{0} \ {0} is finite V46() V47() V48() V49() V50() V51() V55() V56() V57() countable Element of bool NAT
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict AMI-Struct over N
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)
JumpPart S is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable V117() V139() set
K68(S) is set
AddressPart K68(S) is set
N is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable set
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
{(N + 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
S is non empty non with_non-empty_elements set
(S) is non empty finite with_non-empty_values IC-Ins-separated strict AMI-Struct over S
the InstructionsF of (S) 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
P is ins-loc-free Element of the InstructionsF of (S)
InsCode P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (S)
InsCodes the InstructionsF of (S) is non empty set
K78( the InstructionsF of (S)) is set
dom the InstructionsF of (S) is non empty set
dom (dom the InstructionsF of (S)) is set
K68(P) is set
K68(K68(P)) is set
(S,(S),s,P) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
the carrier of (S) is non empty finite countable set
the_Values_of (S) is Relation-like non-empty non empty-yielding the carrier of (S) -defined non empty Function-like total V139() set
the Object-Kind of (S) is Relation-like the carrier of (S) -defined S -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (S),S:]
[: the carrier of (S),S:] is Relation-like non empty set
bool [: the carrier of (S),S:] is non empty set
the ValuesF of (S) is Relation-like S -defined non empty Function-like total set
the Object-Kind of (S) * the ValuesF of (S) is Relation-like the carrier of (S) -defined non empty Function-like finite total countable V139() set
product (the_Values_of (S)) is non empty functional with_common_domain product-like set
{ (IC (Exec (P,b₁))) where b₁ is Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total Element of product (the_Values_of (S)) : IC b₁ = s } is set
NAT --> P is Relation-like NAT -defined the InstructionsF of (S) -valued T-Sequence-like non empty non trivial Function-like constant non finite total quasi_total non empty-membered Element of bool [:NAT, the InstructionsF of (S):]
[:NAT, the InstructionsF of (S):] is Relation-like non empty non trivial non finite non empty-membered set
bool [:NAT, the InstructionsF of (S):] is non empty non trivial non finite non empty-membered set
{P} is non empty trivial finite 1 -element countable set
[:NAT,{P}:] is Relation-like non empty non trivial non finite non empty-membered set
the Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total V139() set is Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total V139() set
IC is V85((S)) Element of the carrier of (S)
the ZeroF of (S) is Element of the carrier of (S)
Values (IC ) is non empty set
(the_Values_of (S)) . (IC ) is non empty set
P is Element of Values (IC )
(IC ) .--> P is Relation-like the carrier of (S) -defined {(IC )} -defined the carrier of (S) -defined Values (IC ) -valued Values (IC ) -valued non empty trivial Function-like one-to-one constant the_Values_of (S) -compatible finite 1 -element countable V139() set
{(IC )} is non empty trivial finite 1 -element countable set
{(IC )} --> P is Relation-like {(IC )} -defined Values (IC ) -valued {P} -valued non empty Function-like constant finite total quasi_total countable V139() Element of bool [:{(IC )},{P}:]
{P} is non empty trivial finite 1 -element countable set
[:{(IC )},{P}:] is Relation-like non empty finite countable set
bool [:{(IC )},{P}:] is non empty finite V30() countable set
dom ((IC ) .--> P) is non empty trivial finite 1 -element countable Element of bool {(IC )}
bool {(IC )} is non empty finite V30() countable set
{(IC )} is non empty trivial finite 1 -element countable Element of bool the carrier of (S)
bool the carrier of (S) is non empty finite V30() countable set
the Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total V139() set +* ((IC ) .--> P) is Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total V139() set
(NAT --> P) /. s is ins-loc-free Element of the InstructionsF of (S)
(NAT --> P) . s is ins-loc-free Element of the InstructionsF of (S)
y is set
succ N is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative countable set
c₁₄ is Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total V139() Element of product (the_Values_of (S))
Exec (P,c₁₄) is Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total V139() set
product ( the Object-Kind of (S) * the ValuesF of (S)) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S)))) is non empty functional set
the Execution of (S) is Relation-like the InstructionsF of (S) -defined Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S)))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of (S),(Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S))))):]
[: the InstructionsF of (S),(Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S))))):] is Relation-like non empty set
bool [: the InstructionsF of (S),(Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S))))):] is non empty set
the Execution of (S) . P is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S))))
( the Execution of (S) . P) . c₁₄ is Relation-like Function-like set
IC (Exec (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
(Exec (P,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
t is Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total V139() Element of product (the_Values_of (S))
IC 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
t . (IC ) is set
((IC ) .--> P) . (IC ) is set
Following ((NAT --> P),t) is Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total V139() set
CurInstr ((NAT --> P),t) is ins-loc-free Element of the InstructionsF of (S)
(NAT --> P) /. (IC t) is ins-loc-free Element of the InstructionsF of (S)
(NAT --> P) . (IC t) is ins-loc-free Element of the InstructionsF of (S)
Exec ((CurInstr ((NAT --> P),t)),t) is Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total V139() set
product ( the Object-Kind of (S) * the ValuesF of (S)) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S)))) is non empty functional set
the Execution of (S) is Relation-like the InstructionsF of (S) -defined Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S)))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of (S),(Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S))))):]
[: the InstructionsF of (S),(Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S))))):] is Relation-like non empty set
bool [: the InstructionsF of (S),(Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S))))):] is non empty set
the Execution of (S) . (CurInstr ((NAT --> P),t)) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of (S) * the ValuesF of (S))),(product ( the Object-Kind of (S) * the ValuesF of (S))))
( the Execution of (S) . (CurInstr ((NAT --> P),t))) . t is Relation-like Function-like set
IC (Following ((NAT --> P),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
(Following ((NAT --> P),t)) . (IC ) is set
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict AMI-Struct over N
the InstructionsF of (N) is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
S is ins-loc-free Element of the InstructionsF of (N)
(N,(N),S) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ (N,(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 { (N,(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
InsCode S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68(S) is set
K68(K68(S)) is set
s 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
(N,(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 finite countable set
the_Values_of (N) is Relation-like non-empty non empty-yielding the carrier of (N) -defined non empty Function-like total V139() set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() 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
0 + 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
{(0 + 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
{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
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
(N,(N),P,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₁ = P } is set
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
{(1 + 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
{2} 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
InsCode S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68(S) is set
K68(K68(S)) is set
s is ins-loc-free Element of the InstructionsF of (N)
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
(N,(N),P,s) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
the carrier of (N) is non empty finite countable set
the_Values_of (N) is Relation-like non-empty non empty-yielding the carrier of (N) -defined non empty Function-like total V139() set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() 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₁ = P } is set
{P} is non empty trivial finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
InsCode S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68(S) is set
K68(K68(S)) is set
N is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable set
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
{N,(N + 1)} is non empty finite V30() V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable set
S is non empty non with_non-empty_elements set
(S) is non empty finite with_non-empty_values IC-Ins-separated strict AMI-Struct over 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) 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
{ ((S,(S),s,b₁) \ (S,(S),b₁)) where b₁ is Element of the InstructionsF of (S) : verum } is set
union { ((S,(S),s,b₁) \ (S,(S),b₁)) where b₁ is Element of the InstructionsF of (S) : verum } is set
s is set
s is ins-loc-free Element of the InstructionsF of (S)
(S,(S),s,s) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
the carrier of (S) is non empty finite countable set
the_Values_of (S) is Relation-like non-empty non empty-yielding the carrier of (S) -defined non empty Function-like total V139() set
the Object-Kind of (S) is Relation-like the carrier of (S) -defined S -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (S),S:]
[: the carrier of (S),S:] is Relation-like non empty set
bool [: the carrier of (S),S:] is non empty set
the ValuesF of (S) is Relation-like S -defined non empty Function-like total set
the Object-Kind of (S) * the ValuesF of (S) is Relation-like the carrier of (S) -defined non empty Function-like finite total countable V139() set
product (the_Values_of (S)) is non empty functional with_common_domain product-like set
{ (IC (Exec (s,b₁))) where b₁ is Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total Element of product (the_Values_of (S)) : IC b₁ = s } is set
(S,(S),s) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ (S,(S),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 { (S,(S),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
(S,(S),s,s) \ (S,(S),s) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
kk is ins-loc-free Element of the InstructionsF of (S)
InsCode kk is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (S)
InsCodes the InstructionsF of (S) is non empty set
K78( the InstructionsF of (S)) is set
dom the InstructionsF of (S) is non empty set
dom (dom the InstructionsF of (S)) is set
K68(kk) is set
K68(K68(kk)) is set
(S,(S),kk) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ (S,(S),b₁,kk) 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 { (S,(S),b₁,kk) 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
{(N + 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
{N} is non empty trivial finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable set
{{N},{(N + 1)}} is non empty finite V30() with_non-empty_elements non empty-membered countable set
kk is ins-loc-free Element of the InstructionsF of (S)
InsCode kk is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (S)
InsCodes the InstructionsF of (S) is non empty set
K78( the InstructionsF of (S)) is set
dom the InstructionsF of (S) is non empty set
dom (dom the InstructionsF of (S)) is set
K68(kk) is set
K68(K68(kk)) is set
(S,(S),kk) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ (S,(S),b₁,kk) 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 { (S,(S),b₁,kk) 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
{N} is non empty trivial finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable set
{(N + 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
{{N},{(N + 1)}} is non empty finite V30() with_non-empty_elements non empty-membered countable set
kk is ins-loc-free Element of the InstructionsF of (S)
InsCode kk is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (S)
InsCodes the InstructionsF of (S) is non empty set
K78( the InstructionsF of (S)) is set
dom the InstructionsF of (S) is non empty set
dom (dom the InstructionsF of (S)) is set
K68(kk) is set
K68(K68(kk)) is set
{N} is non empty trivial finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable set
{(N + 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
{{N},{(N + 1)}} is non empty finite V30() with_non-empty_elements non empty-membered countable set
{N} is non empty trivial finite V30() 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable set
{(N + 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
{{N},{(N + 1)}} is non empty finite V30() with_non-empty_elements non empty-membered countable set
halt (S) is ins-loc-free Element of the InstructionsF of (S)
halt the InstructionsF of (S) is ins-loc-free Element of the InstructionsF of (S)
s is ins-loc-free Element of the InstructionsF of (S)
(S,(S),s) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ (S,(S),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 { (S,(S),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
InsCode s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (S)
InsCodes the InstructionsF of (S) is non empty set
K78( the InstructionsF of (S)) is set
dom the InstructionsF of (S) is non empty set
dom (dom the InstructionsF of (S)) is set
K68(s) is set
K68(K68(s)) is set
(S,(S),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 (S) -defined non empty Function-like the_Values_of (S) -compatible total Element of product (the_Values_of (S)) : IC b₁ = s } is set
(S,(S),s,s) \ (S,(S),s) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ ((S,(S),s,b₂) \ (S,(S),b₂)) where b₁ is ins-loc-free Element of the InstructionsF of (S) : verum } is set
kk is ins-loc-free Element of the InstructionsF of (S)
(S,(S),kk) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ (S,(S),b₁,kk) 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 { (S,(S),b₁,kk) 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
InsCode kk is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (S)
InsCodes the InstructionsF of (S) is non empty set
K78( the InstructionsF of (S)) is set
dom the InstructionsF of (S) is non empty set
dom (dom the InstructionsF of (S)) is set
K68(kk) is set
K68(K68(kk)) is set
(S,(S),s,kk) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
{ (IC (Exec (kk,b₁))) where b₁ is Relation-like the carrier of (S) -defined non empty Function-like the_Values_of (S) -compatible total Element of product (the_Values_of (S)) : IC b₁ = s } is set
(S,(S),s,kk) \ (S,(S),kk) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ ((S,(S),s,b₂) \ (S,(S),b₂)) where b₁ is ins-loc-free Element of the InstructionsF of (S) : verum } is set
{ ((S,(S),s,b₂) \ (S,(S),b₂)) where b₁ is ins-loc-free Element of the InstructionsF of (S) : verum } is set
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict 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
(N,(N),s) 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
{ ((N,(N),s,b₁) \ (N,(N),b₁)) where b₁ is Element of the InstructionsF of (N) : verum } is set
union { ((N,(N),s,b₁) \ (N,(N),b₁)) where b₁ is Element of the InstructionsF of (N) : verum } 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,(s + 1)} is non empty finite V30() V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
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
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict (N) AMI-Struct over N
halt (N) is ins-loc-free Element of the InstructionsF of (N)
the InstructionsF of (N) is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
halt the InstructionsF of (N) is ins-loc-free Element of the InstructionsF of (N)
InsCode (halt (N)) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68((halt (N))) is set
K68(K68((halt (N)))) is set
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict halting (N) AMI-Struct over N
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict halting (N) AMI-Struct over N
the InstructionsF of (N) is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the carrier of (N) is non empty finite countable set
the_Values_of (N) is Relation-like non-empty non empty-yielding the carrier of (N) -defined non empty Function-like total V139() set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() set
S is ins-loc-free Element of the InstructionsF of (N)
InsCode S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68(S) is set
K68(K68(S)) is set
s is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set
Exec (S,s) is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() 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) . s is Relation-like Function-like set
IC is V85((N)) Element of the carrier of (N)
the ZeroF of (N) is Element of the carrier of (N)
(Exec (S,s)) . (IC ) is 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
s . (IC ) is set
succ (IC s) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative countable set
(IC 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
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict halting (N) AMI-Struct over N
the InstructionsF of (N) is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
s is ins-loc-free Element of the InstructionsF of (N)
InsCode s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68(s) is set
K68(K68(s)) 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
(N,(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 finite countable set
the_Values_of (N) is Relation-like non-empty non empty-yielding the carrier of (N) -defined non empty Function-like total V139() set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() 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
succ S is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative countable 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
{(succ S)} 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
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict halting (N) 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
(N,(N),S) 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
{ ((N,(N),S,b₁) \ (N,(N),b₁)) where b₁ is Element of the InstructionsF of (N) : verum } is set
union { ((N,(N),S,b₁) \ (N,(N),b₁)) where b₁ is Element of the InstructionsF of (N) : verum } is set
succ S is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative countable 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,(succ S)} is non empty finite V30() V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable set
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
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
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
the InstructionsF of S 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
succ s is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative countable 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
{(succ s)} 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
P is Element of the InstructionsF of S
(N,S,s,P) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued non empty Function-like total quasi_total Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like non empty set
bool [: the carrier of S,N:] is non empty set
the ValuesF of S is Relation-like N -defined non empty Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined non empty Function-like total set
product (the_Values_of S) is non empty functional with_common_domain product-like set
{ (IC (Exec (P,b₁))) where b₁ is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S) : IC b₁ = s } is set
IC is V85(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
Values (IC ) is non empty set
(the_Values_of S) . (IC ) is non empty set
the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set is Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set
c₆ is set
s is Element of Values (IC )
the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set +* ((IC ),s) is Relation-like the carrier of S -defined non empty Function-like total set
dom the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set +* (s,P) is Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set
( the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set +* (s,P)) /. s is Element of the InstructionsF of S
( the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set +* (s,P)) . s is Element of the InstructionsF of S
dom the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
u is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
IC 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 . (IC ) is set
Following (( the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set +* (s,P)),u) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
CurInstr (( the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set +* (s,P)),u) is Element of the InstructionsF of S
( the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set +* (s,P)) /. (IC u) is Element of the InstructionsF of S
Exec ((CurInstr (( the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set +* (s,P)),u)),u) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the Execution of S is Relation-like the InstructionsF of S -defined Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):]
[: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is Relation-like non empty set
bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is non empty set
the Execution of S . (CurInstr (( the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set +* (s,P)),u)) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the Execution of S . (CurInstr (( the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set +* (s,P)),u))) . u is Relation-like Function-like set
IC (Following (( the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set +* (s,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
(Following (( the Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set +* (s,P)),u)) . (IC ) is set
s is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
Exec (P,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
the Execution of S . P is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the Execution of S . P) . s is Relation-like Function-like set
IC (Exec (P,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
(Exec (P,s)) . (IC ) is 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
s . (IC ) is set
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
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
s is Element of the InstructionsF of S
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued non empty Function-like total quasi_total Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like non empty set
bool [: the carrier of S,N:] is non empty set
the ValuesF of S is Relation-like N -defined non empty Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined non empty Function-like total set
the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set 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(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set . (IC ) is set
(N,S,(IC the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set ),s) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
product (the_Values_of S) is non empty functional with_common_domain product-like set
{ (IC (Exec (s,b₁))) where b₁ is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S) : IC b₁ = IC the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set } is set
succ (IC the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set ) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative countable set
(IC the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total 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
{(succ (IC the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set ))} 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
{(IC the Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set )} 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 S
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
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
s is Element of the InstructionsF of S
(N,S,s) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ (N,S,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 { (N,S,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
c₆ 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
(N,S,s,s) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued non empty Function-like total quasi_total Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like non empty set
bool [: the carrier of S,N:] is non empty set
the ValuesF of S is Relation-like N -defined non empty Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined non empty Function-like total set
product (the_Values_of S) is non empty functional with_common_domain product-like set
{ (IC (Exec (s,b₁))) where b₁ is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S) : IC b₁ = s } is set
s is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
Exec (s,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the Execution of S is Relation-like the InstructionsF of S -defined Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):]
[: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is Relation-like non empty set
bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is non empty set
the Execution of S . s is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the Execution of S . s) . s is Relation-like Function-like set
IC (Exec (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
IC is V85(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(Exec (s,s)) . (IC ) is 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
s . (IC ) is set
succ (IC s) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative countable set
(IC 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
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
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
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
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
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
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued non empty Function-like total quasi_total Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like non empty set
bool [: the carrier of S,N:] is non empty set
the ValuesF of S is Relation-like N -defined non empty Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined non empty Function-like total set
s is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable V139() set
dom s is finite V46() V47() V48() V49() V50() V51() V55() V56() V57() countable Element of bool NAT
P is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC 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
IC is V85(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
P . (IC ) 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
Comput (s,P,c₆) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (s,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
(Comput (s,P,c₆)) . (IC ) is set
product (the_Values_of S) is non empty functional with_common_domain product-like set
s is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
Following (s,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
CurInstr (s,s) is Element of the InstructionsF of S
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 /. (IC s) is Element of the InstructionsF of S
Exec ((CurInstr (s,s)),s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the Execution of S is Relation-like the InstructionsF of S -defined Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):]
[: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is Relation-like non empty set
bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is non empty set
the Execution of S . (CurInstr (s,s)) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the Execution of S . (CurInstr (s,s))) . s is Relation-like Function-like set
IC (Following (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
(Following (s,s)) . (IC ) is set
s /. (IC (Comput (s,P,c₆))) is Element of the InstructionsF of S
(N,S,(IC (Comput (s,P,c₆))),(s /. (IC (Comput (s,P,c₆))))) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
{ (IC (Exec ((s /. (IC (Comput (s,P,c₆)))),b₁))) where b₁ is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S) : IC b₁ = IC (Comput (s,P,c₆)) } is set
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
Comput (s,P,(c₆ + 1)) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (s,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
(Comput (s,P,(c₆ + 1))) . (IC ) is set
Comput (s,P,0) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (s,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
(Comput (s,P,0)) . (IC ) 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
s /. P is Element of the InstructionsF of S
(N,S,P,(s /. P)) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
product (the_Values_of S) is non empty functional with_common_domain product-like set
{ (IC (Exec ((s /. P),b₁))) where b₁ is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S) : IC b₁ = P } is set
c₆ is set
s is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
Exec ((s /. P),s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the Execution of S is Relation-like the InstructionsF of S -defined Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):]
[: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is Relation-like non empty set
bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is non empty set
the Execution of S . (s /. P) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the Execution of S . (s /. P)) . s is Relation-like Function-like set
IC (Exec ((s /. P),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
IC is V85(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(Exec ((s /. P),s)) . (IC ) is 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
s . (IC ) is set
s is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
0 + 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
Comput (s,s,(0 + 1)) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (s,s,(0 + 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
(Comput (s,s,(0 + 1))) . (IC ) is set
Comput (s,s,0) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
Following (s,(Comput (s,s,0))) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
CurInstr (s,(Comput (s,s,0))) is Element of the InstructionsF of S
IC (Comput (s,s,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
(Comput (s,s,0)) . (IC ) is set
s /. (IC (Comput (s,s,0))) is Element of the InstructionsF of S
Exec ((CurInstr (s,(Comput (s,s,0)))),(Comput (s,s,0))) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
the Execution of S . (CurInstr (s,(Comput (s,s,0)))) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the Execution of S . (CurInstr (s,(Comput (s,s,0))))) . (Comput (s,s,0)) is Relation-like Function-like set
IC (Following (s,(Comput (s,s,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
(Following (s,(Comput (s,s,0)))) . (IC ) is set
Following (s,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
CurInstr (s,s) is Element of the InstructionsF of S
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 /. (IC s) is Element of the InstructionsF of S
Exec ((CurInstr (s,s)),s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
the Execution of S . (CurInstr (s,s)) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the Execution of S . (CurInstr (s,s))) . s is Relation-like Function-like set
IC (Following (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
(Following (s,s)) . (IC ) is set
Exec ((s /. (IC s)),s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
the Execution of S . (s /. (IC s)) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the Execution of S . (s /. (IC s))) . s is Relation-like Function-like set
IC (Exec ((s /. (IC 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
(Exec ((s /. (IC s)),s)) . (IC ) is set
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
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued non empty Function-like total quasi_total Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like non empty set
bool [: the carrier of S,N:] is non empty set
the ValuesF of S is Relation-like N -defined non empty Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined non empty Function-like total set
s is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable V139() set
dom s is finite V46() V47() V48() V49() V50() V51() V55() V56() V57() countable Element of bool NAT
P is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC 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
IC is V85(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
P . (IC ) is set
c₆ is Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total 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
Comput (c₆,P,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (c₆,P,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
(Comput (c₆,P,s)) . (IC ) is set
product (the_Values_of S) is non empty functional with_common_domain product-like set
s is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S)
Following (c₆,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
CurInstr (c₆,s) is Element of the InstructionsF of S
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
c₆ /. (IC s) is Element of the InstructionsF of S
Exec ((CurInstr (c₆,s)),s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the Execution of S is Relation-like the InstructionsF of S -defined Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):]
[: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is Relation-like non empty set
bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is non empty set
the Execution of S . (CurInstr (c₆,s)) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the Execution of S . (CurInstr (c₆,s))) . s is Relation-like Function-like set
IC (Following (c₆,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)) . (IC ) is set
c₆ /. (IC (Comput (c₆,P,s))) is Element of the InstructionsF of S
(N,S,(IC (Comput (c₆,P,s))),(c₆ /. (IC (Comput (c₆,P,s))))) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
{ (IC (Exec ((c₆ /. (IC (Comput (c₆,P,s)))),b₁))) where b₁ is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S) : IC b₁ = IC (Comput (c₆,P,s)) } 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
Comput (c₆,P,(s + 1)) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
s /. (IC (Comput (c₆,P,s))) is Element of the InstructionsF of S
IC (Comput (c₆,P,(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
(Comput (c₆,P,(s + 1))) . (IC ) is set
Comput (c₆,P,0) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (c₆,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
(Comput (c₆,P,0)) . (IC ) is set
P is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC 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
IC is V85(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
P . (IC ) is set
c₆ is Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total 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
Comput (s,P,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (s,P,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
(Comput (s,P,s)) . (IC ) is set
Comput (c₆,P,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (c₆,P,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
(Comput (c₆,P,s)) . (IC ) is set
Comput (c₆,P,0) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
Comput (s,P,0) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
s is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable set
Comput (c₆,P,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
Comput (s,P,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total 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
Comput (c₆,P,(s + 1)) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
Comput (s,P,(s + 1)) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total 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
Comput (c₆,P,kk) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (c₆,P,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
(Comput (c₆,P,kk)) . (IC ) is set
Following (c₆,(Comput (s,P,s))) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
CurInstr (c₆,(Comput (s,P,s))) is Element of the InstructionsF of S
IC (Comput (s,P,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
(Comput (s,P,s)) . (IC ) is set
c₆ /. (IC (Comput (s,P,s))) is Element of the InstructionsF of S
Exec ((CurInstr (c₆,(Comput (s,P,s)))),(Comput (s,P,s))) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
product ( the Object-Kind of S * the ValuesF of S) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) is non empty functional set
the Execution of S is Relation-like the InstructionsF of S -defined Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):]
[: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is Relation-like non empty set
bool [: the InstructionsF of S,(Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))):] is non empty set
the Execution of S . (CurInstr (c₆,(Comput (s,P,s)))) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the Execution of S . (CurInstr (c₆,(Comput (s,P,s))))) . (Comput (s,P,s)) is Relation-like Function-like set
Following (s,(Comput (s,P,s))) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
CurInstr (s,(Comput (s,P,s))) is Element of the InstructionsF of S
s /. (IC (Comput (s,P,s))) is Element of the InstructionsF of S
Exec ((CurInstr (s,(Comput (s,P,s)))),(Comput (s,P,s))) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
the Execution of S . (CurInstr (s,(Comput (s,P,s)))) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of S * the ValuesF of S)),(product ( the Object-Kind of S * the ValuesF of S)))
( the Execution of S . (CurInstr (s,(Comput (s,P,s))))) . (Comput (s,P,s)) is Relation-like Function-like set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
s is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable V139() set
dom s is finite V46() V47() V48() V49() V50() V51() V55() V56() V57() countable Element of bool NAT
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued non empty Function-like total quasi_total Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like non empty set
bool [: the carrier of S,N:] is non empty set
the ValuesF of S is Relation-like N -defined non empty Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined non empty Function-like total set
P is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total 0 -started set
IC 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
IC is V85(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
P . (IC ) is set
c₆ is Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total 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
Comput (c₆,P,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (c₆,P,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
(Comput (c₆,P,s)) . (IC ) is set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting (N) AMI-Struct over N
halt S is halting (N,S) Element of the InstructionsF of S
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
0 .--> (halt S) is Relation-like NAT -defined {0} -defined the InstructionsF of S -valued the InstructionsF of S -valued non empty trivial Function-like one-to-one constant finite 1 -element unique-halt countable V139() set
{0} --> (halt S) is Relation-like {0} -defined the InstructionsF of S -valued {(halt S)} -valued non empty Function-like constant finite total quasi_total countable V139() Element of bool [:{0},{(halt S)}:]
{(halt S)} is non empty trivial finite 1 -element countable set
[:{0},{(halt S)}:] is Relation-like non empty finite countable set
bool [:{0},{(halt S)}:] is non empty finite V30() countable 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
dom (0 .--> (halt S)) is non empty trivial finite 1 -element V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
(0 .--> (halt S)) /. P is Element of the InstructionsF of S
(N,S,P,((0 .--> (halt S)) /. P)) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued non empty Function-like total quasi_total Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like non empty set
bool [: the carrier of S,N:] is non empty set
the ValuesF of S is Relation-like N -defined non empty Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined non empty Function-like total set
product (the_Values_of S) is non empty functional with_common_domain product-like set
{ (IC (Exec (((0 .--> (halt S)) /. P),b₁))) where b₁ is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S) : IC b₁ = P } is set
dom (0 .--> (halt 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
s is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable V139() set
dom s is finite V46() V47() V48() V49() V50() V51() V55() V56() V57() countable Element of bool NAT
s /. P is Element of the InstructionsF of S
s . P is set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
s is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable V139() set
dom s is finite V46() V47() V48() V49() V50() V51() V55() V56() V57() countable Element of bool NAT
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting (N) AMI-Struct over N
halt S is halting (N,S) Element of the InstructionsF of S
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
<%(halt S)%> is Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued T-Sequence-like non empty trivial Function-like constant finite 1 -element initial unique-halt countable V139() set
0 .--> (halt S) is Relation-like NAT -defined {0} -defined the InstructionsF of S -valued the InstructionsF of S -valued non empty trivial Function-like one-to-one constant finite 1 -element unique-halt countable V139() set
{0} --> (halt S) is Relation-like {0} -defined the InstructionsF of S -valued {(halt S)} -valued non empty Function-like constant finite total quasi_total countable V139() Element of bool [:{0},{(halt S)}:]
{(halt S)} is non empty trivial finite 1 -element countable set
[:{0},{(halt S)}:] is Relation-like non empty finite countable set
bool [:{0},{(halt S)}:] is non empty finite V30() countable set
dom <%(halt S)%> is epsilon-transitive epsilon-connected ordinal natural non empty trivial V16() V17() finite cardinal 1 -element ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
card (dom <%(halt 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 omega
LastLoc <%(halt 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 <%(halt S)%> is epsilon-transitive epsilon-connected ordinal natural non empty trivial V16() V17() finite cardinal 1 -element ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
max (dom <%(halt S)%>) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V113() set
card <%(halt 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 omega
dom <%(halt S)%> is epsilon-transitive epsilon-connected ordinal natural non empty trivial V16() V17() finite cardinal 1 -element ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable set
(card <%(halt 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
<%(halt S)%> . (LastLoc <%(halt S)%>) is set
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable set
<%(halt S)%> . P is set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
halt S is halting (N,S) Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
<%(halt S)%> is Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued T-Sequence-like non empty trivial Function-like constant finite 1 -element initial unique-halt countable V139() set
0 .--> (halt S) is Relation-like NAT -defined {0} -defined the InstructionsF of S -valued the InstructionsF of S -valued non empty trivial Function-like one-to-one constant finite 1 -element unique-halt countable V139() set
{0} --> (halt S) is Relation-like {0} -defined the InstructionsF of S -valued {(halt S)} -valued non empty Function-like constant finite total quasi_total countable V139() Element of bool [:{0},{(halt S)}:]
{(halt S)} is non empty trivial finite 1 -element countable set
[:{0},{(halt S)}:] is Relation-like non empty finite countable set
bool [:{0},{(halt S)}:] is non empty finite V30() countable set
s is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like non empty Function-like finite initial countable V139() set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
halt S is halting (N,S) Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
<%(halt S)%> is Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued T-Sequence-like non empty trivial Function-like constant finite 1 -element initial unique-halt countable V139() set
0 .--> (halt S) is Relation-like NAT -defined {0} -defined the InstructionsF of S -valued the InstructionsF of S -valued non empty trivial Function-like one-to-one constant finite 1 -element unique-halt countable V139() set
{0} --> (halt S) is Relation-like {0} -defined the InstructionsF of S -valued {(halt S)} -valued non empty Function-like constant finite total quasi_total countable V139() Element of bool [:{0},{(halt S)}:]
{(halt S)} is non empty trivial finite 1 -element countable set
[:{0},{(halt S)}:] is Relation-like non empty finite countable set
bool [:{0},{(halt S)}:] is non empty finite V30() countable set
s is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like non empty Function-like finite initial countable V139() set
LastLoc 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 epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
max (dom s) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V113() set
s . (LastLoc s) is set
dom s is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable set
s . P is set
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting (N) AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
halt S is halting (N,S) Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
<%(halt S)%> is Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued T-Sequence-like non empty trivial Function-like constant finite 1 -element initial unique-halt countable V139() set
0 .--> (halt S) is Relation-like NAT -defined {0} -defined the InstructionsF of S -valued the InstructionsF of S -valued non empty trivial Function-like one-to-one constant finite 1 -element unique-halt countable V139() set
{0} --> (halt S) is Relation-like {0} -defined the InstructionsF of S -valued {(halt S)} -valued non empty Function-like constant finite total quasi_total countable V139() Element of bool [:{0},{(halt S)}:]
{(halt S)} is non empty trivial finite 1 -element countable set
[:{0},{(halt S)}:] is Relation-like non empty finite countable set
bool [:{0},{(halt S)}:] is non empty finite V30() countable set
s is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like non empty Function-like finite initial countable V139() set
LastLoc 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 epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
max (dom s) is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal V41() ext-real non negative countable V113() set
s . (LastLoc s) is set
dom s is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
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
s . P is set
P is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like non empty Function-like finite initial halt-ending unique-halt countable V139() set
N is non empty non with_non-empty_elements set
Trivial-AMI N is non empty trivial finite 1 -element with_non-empty_values IC-Ins-separated strict halting AMI-Struct over N
the InstructionsF of (Trivial-AMI N) is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
S is Element of the InstructionsF of (Trivial-AMI N)
the carrier of (Trivial-AMI N) is non empty trivial finite 1 -element countable set
the_Values_of (Trivial-AMI N) is Relation-like non-empty non empty-yielding the carrier of (Trivial-AMI N) -defined non empty Function-like total V139() set
the Object-Kind of (Trivial-AMI N) is Relation-like the carrier of (Trivial-AMI N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (Trivial-AMI N),N:]
[: the carrier of (Trivial-AMI N),N:] is Relation-like non empty set
bool [: the carrier of (Trivial-AMI N),N:] is non empty set
the ValuesF of (Trivial-AMI N) is Relation-like N -defined non empty Function-like total set
the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N) is Relation-like the carrier of (Trivial-AMI N) -defined non empty Function-like finite total countable V139() set
P is Relation-like the carrier of (Trivial-AMI N) -defined non empty Function-like the_Values_of (Trivial-AMI N) -compatible total V139() set
Exec (S,P) is Relation-like the carrier of (Trivial-AMI N) -defined non empty Function-like the_Values_of (Trivial-AMI N) -compatible total V139() set
product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N)) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N))),(product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N)))) is non empty functional set
the Execution of (Trivial-AMI N) is Relation-like the InstructionsF of (Trivial-AMI N) -defined Funcs ((product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N))),(product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N)))) -valued non empty Function-like total quasi_total Function-yielding V153() Element of bool [: the InstructionsF of (Trivial-AMI N),(Funcs ((product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N))),(product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N))))):]
[: the InstructionsF of (Trivial-AMI N),(Funcs ((product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N))),(product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N))))):] is Relation-like non empty set
bool [: the InstructionsF of (Trivial-AMI N),(Funcs ((product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N))),(product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N))))):] is non empty set
the Execution of (Trivial-AMI N) . S is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N))),(product ( the Object-Kind of (Trivial-AMI N) * the ValuesF of (Trivial-AMI N))))
( the Execution of (Trivial-AMI N) . S) . P is Relation-like Function-like set
product (the_Values_of (Trivial-AMI N)) is non empty functional with_common_domain product-like set
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
[:N,{NAT}:] is Relation-like non empty set
id (product (the_Values_of (Trivial-AMI N))) is Relation-like product (the_Values_of (Trivial-AMI N)) -defined product (the_Values_of (Trivial-AMI N)) -valued non empty Function-like one-to-one total quasi_total onto bijective V128() V130() V131() V135() Function-yielding V153() Element of bool [:(product (the_Values_of (Trivial-AMI N))),(product (the_Values_of (Trivial-AMI N))):]
[:(product (the_Values_of (Trivial-AMI N))),(product (the_Values_of (Trivial-AMI N))):] is Relation-like non empty set
bool [:(product (the_Values_of (Trivial-AMI N))),(product (the_Values_of (Trivial-AMI N))):] is non empty set
[0,{},{}] .--> (id (product (the_Values_of (Trivial-AMI N)))) is Relation-like {[0,{},{}]} -defined bool [:(product (the_Values_of (Trivial-AMI N))),(product (the_Values_of (Trivial-AMI N))):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[0,{},{}]} --> (id (product (the_Values_of (Trivial-AMI N)))) is Relation-like non-empty non empty-yielding {[0,{},{}]} -defined bool [:(product (the_Values_of (Trivial-AMI N))),(product (the_Values_of (Trivial-AMI N))):] -valued {(id (product (the_Values_of (Trivial-AMI N))))} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[0,{},{}]},{(id (product (the_Values_of (Trivial-AMI N))))}:]
{(id (product (the_Values_of (Trivial-AMI N))))} is non empty trivial functional finite 1 -element with_non-empty_elements non empty-membered with_common_domain countable set
[:{[0,{},{}]},{(id (product (the_Values_of (Trivial-AMI N))))}:] is Relation-like non empty finite countable set
bool [:{[0,{},{}]},{(id (product (the_Values_of (Trivial-AMI N))))}:] is non empty finite V30() countable set
([0,{},{}] .--> (id (product (the_Values_of (Trivial-AMI N))))) . S is Relation-like Function-like set
c₆ is Relation-like the carrier of (Trivial-AMI N) -defined non empty Function-like the_Values_of (Trivial-AMI N) -compatible total V139() Element of product (the_Values_of (Trivial-AMI N))
( the Execution of (Trivial-AMI N) . S) . c₆ is Relation-like Function-like set
N is non empty non with_non-empty_elements set
Trivial-AMI N is non empty trivial finite 1 -element with_non-empty_values IC-Ins-separated strict halting AMI-Struct over N
the InstructionsF of (Trivial-AMI N) is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
S is Element of the InstructionsF of (Trivial-AMI N)
InsCode S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (Trivial-AMI N)
InsCodes the InstructionsF of (Trivial-AMI N) is non empty set
K78( the InstructionsF of (Trivial-AMI N)) is set
dom the InstructionsF of (Trivial-AMI N) is non empty set
dom (dom the InstructionsF of (Trivial-AMI N)) is set
K68(S) is set
K68(K68(S)) is set
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
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
s is Element of the InstructionsF of S
(N,S,s) is V46() V47() V48() V49() V50() V51() V55() countable Element of bool NAT
{ (N,S,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 { (N,S,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
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
(N,S,P,s) is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued non empty Function-like total quasi_total Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like non empty set
bool [: the carrier of S,N:] is non empty set
the ValuesF of S is Relation-like N -defined non empty Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined non empty Function-like total set
product (the_Values_of S) is non empty functional with_common_domain product-like set
{ (IC (Exec (s,b₁))) where b₁ is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total Element of product (the_Values_of S) : IC b₁ = P } is set
s is set
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict halting (N) AMI-Struct over N
the InstructionsF of (N) is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the carrier of (N) is non empty finite countable set
the_Values_of (N) is Relation-like non-empty non empty-yielding the carrier of (N) -defined non empty Function-like total V139() set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() set
S is ins-loc-free Element of the InstructionsF of (N)
InsCode S is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative countable Element of InsCodes the InstructionsF of (N)
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
K68(S) is set
K68(K68(S)) is set
s is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set
Exec (S,s) is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() 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) . s is Relation-like Function-like set
IncIC (s,1) is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() 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
IC is V85((N)) Element of the carrier of (N)
the ZeroF of (N) is Element of the carrier of (N)
s . (IC ) is set
(IC 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
Start-At (((IC s) + 1),(N)) is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible finite countable (IC s) + 1 -started V139() set
(IC ) .--> ((IC s) + 1) is Relation-like the carrier of (N) -defined {(IC )} -defined NAT -valued non empty trivial Function-like one-to-one constant finite 1 -element Cardinal-yielding countable V139() set
{(IC )} is non empty trivial finite 1 -element countable set
{(IC )} --> ((IC s) + 1) is Relation-like non-empty non empty-yielding {(IC )} -defined NAT -valued {((IC s) + 1)} -valued non empty Function-like constant finite total quasi_total Cardinal-yielding countable V139() Element of bool [:{(IC )},{((IC s) + 1)}:]
{((IC 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 set
[:{(IC )},{((IC s) + 1)}:] is Relation-like non empty finite countable set
bool [:{(IC )},{((IC s) + 1)}:] is non empty finite V30() countable set
s +* (Start-At (((IC s) + 1),(N))) is Relation-like the carrier of (N) -defined the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible the_Values_of (N) -compatible total (IC s) + 1 -started V139() set
{[0,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins homogeneous J/A-independent V71() countable Element of bool [:NAT,NAT,NAT:]
{[1,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins countable Element of bool [:NAT,NAT,NAT:]
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
id (product (the_Values_of (N))) is Relation-like product (the_Values_of (N)) -defined product (the_Values_of (N)) -valued non empty Function-like one-to-one total quasi_total onto bijective V128() V130() V131() V135() Function-yielding V153() Element of bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):]
[0,0,0] .--> (id (product (the_Values_of (N)))) is Relation-like [:NAT,NAT,NAT:] -defined {[0,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[0,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins homogeneous J/A-independent V71() countable set
{[0,0,0]} --> (id (product (the_Values_of (N)))) is Relation-like non-empty non empty-yielding {[0,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued {(id (product (the_Values_of (N))))} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[0,0,0]},{(id (product (the_Values_of (N))))}:]
{(id (product (the_Values_of (N))))} is non empty trivial functional finite 1 -element with_non-empty_elements non empty-membered with_common_domain countable set
[:{[0,0,0]},{(id (product (the_Values_of (N))))}:] is Relation-like non empty finite countable set
bool [:{[0,0,0]},{(id (product (the_Values_of (N))))}:] is non empty finite V30() countable set
c₆ 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))):]
[1,0,0] .--> c₆ is Relation-like [:NAT,NAT,NAT:] -defined {[1,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued non empty trivial Function-like one-to-one constant finite 1 -element countable V139() Function-yielding V153() set
{[1,0,0]} is Relation-like non empty trivial finite 1 -element standard-ins countable set
{[1,0,0]} --> c₆ is Relation-like non-empty non empty-yielding {[1,0,0]} -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued {c₆} -valued non empty Function-like constant finite total quasi_total countable V139() Function-yielding V153() Element of bool [:{[1,0,0]},{c₆}:]
{c₆} is non empty trivial functional finite 1 -element with_non-empty_elements non empty-membered with_common_domain countable set
[:{[1,0,0]},{c₆}:] is Relation-like non empty finite countable set
bool [:{[1,0,0]},{c₆}:] is non empty finite V30() countable set
([1,0,0] .--> c₆) +* ([0,0,0] .--> (id (product (the_Values_of (N))))) is Relation-like [:NAT,NAT,NAT:] -defined bool [:(product (the_Values_of (N))),(product (the_Values_of (N))):] -valued non empty Function-like finite countable V139() Function-yielding V153() set
s is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() set
c₆ . s is Relation-like Function-like set
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
s is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() Element of product (the_Values_of (N))
c₆ . s is Relation-like the carrier of (N) -defined non empty Function-like the_Values_of (N) -compatible total V139() Element of product (the_Values_of (N))
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
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
dom ([0,0,0] .--> (id (product (the_Values_of (N))))) is Relation-like non empty trivial finite 1 -element countable Element of bool {[0,0,0]}
bool {[0,0,0]} is non empty finite V30() countable set
([1,0,0] .--> c₆) . S is Relation-like Function-like set
N is non empty non with_non-empty_elements set
(N) is non empty finite with_non-empty_values IC-Ins-separated strict halting (N) AMI-Struct over N
the carrier of (N) is non empty finite countable set
the_Values_of (N) is Relation-like non-empty non empty-yielding the carrier of (N) -defined non empty Function-like total V139() set
the Object-Kind of (N) is Relation-like the carrier of (N) -defined N -valued non empty Function-like finite total quasi_total countable V139() Element of bool [: the carrier of (N),N:]
[: the carrier of (N),N:] is Relation-like non empty set
bool [: the carrier of (N),N:] is non empty set
the ValuesF of (N) is Relation-like N -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 finite total countable V139() set
S is Relation-like the carrier of (N) -defined Function-like the_Values_of (N) -compatible set
DataPart S is Relation-like the carrier of (N) -defined Function-like the_Values_of (N) -compatible data-only set
NonZero (N) is finite countable Element of bool the carrier of (N)
bool the carrier of (N) is non empty finite V30() countable set
[#] (N) is non empty non proper finite countable Element of bool the carrier of (N)
IC is V85((N)) Element of the carrier of (N)
the ZeroF of (N) is Element of the carrier of (N)
{(IC )} is non empty trivial finite 1 -element countable set
([#] (N)) \ {(IC )} is finite countable Element of bool the carrier of (N)
S | (NonZero (N)) is Relation-like NonZero (N) -defined the carrier of (N) -defined Function-like the_Values_of (N) -compatible finite countable V139() set
the carrier of (N) \ {0} is finite countable Element of bool the carrier of (N)
{0} \ {0} is finite V46() V47() V48() V49() V50() V51() V55() V56() V57() countable Element of bool 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
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued non empty Function-like total quasi_total Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like non empty set
bool [: the carrier of S,N:] is non empty set
the ValuesF of S is Relation-like N -defined non empty Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined non empty Function-like total set
s is non empty non with_non-empty_elements set
kk is non empty with_non-empty_values IC-Ins-separated AMI-Struct over s
the InstructionsF of kk is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
s is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable V139() set
P is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC 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
IC is V85(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
P . (IC ) is set
dom s is finite V46() V47() V48() V49() V50() V51() V55() V56() V57() countable Element of bool NAT
c₆ is Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total 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
Comput (c₆,P,s) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (c₆,P,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
(Comput (c₆,P,s)) . (IC ) is set
the carrier of kk is non empty set
the_Values_of kk is Relation-like non-empty non empty-yielding the carrier of kk -defined non empty Function-like total set
the Object-Kind of kk is Relation-like the carrier of kk -defined s -valued non empty Function-like total quasi_total Element of bool [: the carrier of kk,s:]
[: the carrier of kk,s:] is Relation-like non empty set
bool [: the carrier of kk,s:] is non empty set
the ValuesF of kk is Relation-like s -defined non empty Function-like total set
the Object-Kind of kk * the ValuesF of kk is Relation-like the carrier of kk -defined non empty Function-like total set
P is Relation-like NAT -defined the InstructionsF of kk -valued Function-like finite countable V139() set
dom P is finite V46() V47() V48() V49() V50() V51() V55() V56() V57() countable Element of bool NAT
N is non empty non with_non-empty_elements set
S is non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
the InstructionsF of S is Relation-like non empty standard-ins homogeneous J/A-independent V71() set
Stop S is Relation-like NAT -defined the InstructionsF of S -valued T-Sequence-like non empty trivial Function-like constant finite 1 -element initial non halt-free halt-ending unique-halt countable V139() set
halt S is halting (N,S) Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
<%(halt S)%> is Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued T-Sequence-like non empty trivial Function-like constant finite 1 -element initial unique-halt countable V139() set
0 .--> (halt S) is Relation-like NAT -defined {0} -defined the InstructionsF of S -valued the InstructionsF of S -valued non empty trivial Function-like one-to-one constant finite 1 -element unique-halt countable V139() set
{0} --> (halt S) is Relation-like {0} -defined the InstructionsF of S -valued {(halt S)} -valued non empty Function-like constant finite total quasi_total countable V139() Element of bool [:{0},{(halt S)}:]
{(halt S)} is non empty trivial finite 1 -element countable set
[:{0},{(halt S)}:] is Relation-like non empty finite countable set
bool [:{0},{(halt S)}:] is non empty finite V30() countable set
the carrier of S is non empty set
the_Values_of S is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
the Object-Kind of S is Relation-like the carrier of S -defined N -valued non empty Function-like total quasi_total Element of bool [: the carrier of S,N:]
[: the carrier of S,N:] is Relation-like non empty set
bool [: the carrier of S,N:] is non empty set
the ValuesF of S is Relation-like N -defined non empty Function-like total set
the Object-Kind of S * the ValuesF of S is Relation-like the carrier of S -defined non empty Function-like total set
s is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total 0 -started set
P is Relation-like NAT -defined the InstructionsF of S -valued non empty Function-like total set
Comput (P,s,0) is Relation-like the carrier of S -defined non empty Function-like the_Values_of S -compatible total set
IC (Comput (P,s,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
IC is V85(S) Element of the carrier of S
the ZeroF of S is Element of the carrier of S
(Comput (P,s,0)) . (IC ) is set
dom P is non empty V46() V47() V48() V49() V50() V51() V53() V55() set
CurInstr (P,(Comput (P,s,0))) is Element of the InstructionsF of S
P /. (IC (Comput (P,s,0))) is Element of the InstructionsF of S
dom (Stop S) is epsilon-transitive epsilon-connected ordinal natural non empty trivial V16() V17() finite cardinal 1 -element ext-real non negative V46() V47() V48() V49() V50() V51() V53() V54() V55() V56() V57() countable Element of bool NAT
dom P is non empty V46() V47() V48() V49() V50() V51() V53() V55() countable Element of bool NAT
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
P /. 0 is Element of the InstructionsF of S
P . 0 is Element of the InstructionsF of S
(Stop S) . 0 is set