REAL is set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite countable denumerable V64() Element of bool REAL
bool REAL is set
omega is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite countable denumerable V64() set
bool omega is set
bool NAT is set
9 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
Segm 9 is countable Element of bool omega
SCM-Data-Loc is non empty set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
K86(NAT,1) is finite countable V63() Element of bool NAT
[:K86(NAT,1),NAT:] is Relation-like NAT -defined REAL -valued Element of bool [:NAT,REAL:]
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is set
SCM-Memory is set
{NAT} is finite countable V63() set
{NAT} \/ SCM-Data-Loc is set
bool SCM-Memory is set
2 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
[:SCM-Memory,2:] is Relation-like set
bool [:SCM-Memory,2:] is set
SCM-OK is Relation-like SCM-Memory -defined 2 -valued Function-like V38( SCM-Memory ,2) Element of bool [:SCM-Memory,2:]
SCM-VAL is Relation-like 2 -defined Function-like total set
INT is set
K276(NAT,INT) is set
SCM-OK * SCM-VAL is Relation-like SCM-Memory -defined Function-like set
product (SCM-OK * SCM-VAL) is functional with_common_domain product-like set
SCM-Instr is Relation-like non empty standard-ins V72() V73() V75() set
SCM-Halt is Element of Segm 9
the Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V24() V25() finite finite-yielding V30() Cardinal-yielding countable integer Function-yielding V94() ext-real non negative set is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V24() V25() finite finite-yielding V30() Cardinal-yielding countable integer Function-yielding V94() ext-real non negative set
{} is set
[SCM-Halt,{},{}] is V13() V14() set
[SCM-Halt,{}] is non natural V13() set
{SCM-Halt,{}} is finite countable set
{SCM-Halt} is finite countable set
{{SCM-Halt,{}},{SCM-Halt}} is finite V30() countable set
[[SCM-Halt,{}],{}] is non natural V13() set
{[SCM-Halt,{}],{}} is finite countable set
{[SCM-Halt,{}]} is Relation-like Function-like finite countable set
{{[SCM-Halt,{}],{}},{[SCM-Halt,{}]}} is finite V30() countable set
{[SCM-Halt,{},{}]} is Relation-like non empty finite countable standard-ins V72() V73() V75() set
6 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
{ [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b1 = 6 } is set
{[SCM-Halt,{},{}]} \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b1 = 6 } is set
7 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
8 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
K87(NAT,7,8) is finite countable V63() Element of bool NAT
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT , b3 is Element of SCM-Data-Loc : b1 in K87(NAT,7,8) } is set
({[SCM-Halt,{},{}]} \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT , b3 is Element of SCM-Data-Loc : b1 in K87(NAT,7,8) } is set
3 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
4 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
5 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
K90(NAT,1,2,3,4,5) is finite countable V63() Element of bool NAT
{ [b1,{},K149(SCM-Data-Loc,b2,b3)] where b1 is Element of Segm 9, b2, b3 is Element of SCM-Data-Loc : b1 in K90(NAT,1,2,3,4,5) } is set
(({[SCM-Halt,{},{}]} \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT , b3 is Element of SCM-Data-Loc : b1 in K87(NAT,7,8) } ) \/ { [b1,{},K149(SCM-Data-Loc,b2,b3)] where b1 is Element of Segm 9, b2, b3 is Element of SCM-Data-Loc : b1 in K90(NAT,1,2,3,4,5) } is set
K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))) is set
[:SCM-Instr,K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))):] is Relation-like set
bool [:SCM-Instr,K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))):] is set
SCM is non empty with_non-empty_values IC-Ins-separated strict strict halting AMI-Struct over 2
In (NAT,SCM-Memory) is Element of SCM-Memory
SCM-Exec is Relation-like SCM-Instr -defined K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))) -valued Function-like V38( SCM-Instr ,K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL)))) Element of bool [:SCM-Instr,K165((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))):]
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2
the InstructionsF of SCM is Relation-like non empty standard-ins V72() V73() V75() set
the carrier of SCM is non empty set
the_Values_of SCM is Relation-like non-empty the carrier of SCM -defined Function-like total set
the Object-Kind of SCM is Relation-like the carrier of SCM -defined 2 -valued Function-like V38( the carrier of SCM,2) Element of bool [: the carrier of SCM,2:]
[: the carrier of SCM,2:] is Relation-like set
bool [: the carrier of SCM,2:] is set
the ValuesF of SCM is Relation-like 2 -defined Function-like total set
the Object-Kind of SCM * the ValuesF of SCM is Relation-like the carrier of SCM -defined Function-like set
SCM+FSA-Data*-Loc is non empty set
INT \ NAT is Element of bool INT
bool INT is set
SCM+FSA-Memory is non empty set
SCM-Memory \/ SCM+FSA-Data*-Loc is set
bool SCM+FSA-Memory is set
[:SCM+FSA-Memory,3:] is Relation-like set
bool [:SCM+FSA-Memory,3:] is set
SCM+FSA-OK is Relation-like SCM+FSA-Memory -defined 3 -valued Function-like V38( SCM+FSA-Memory ,3) Element of bool [:SCM+FSA-Memory,3:]
SCM+FSA-Memory --> 2 is Relation-like non-empty SCM+FSA-Memory -defined NAT -valued non empty Function-like constant total V38( SCM+FSA-Memory , NAT ) Element of bool [:SCM+FSA-Memory,NAT:]
[:SCM+FSA-Memory,NAT:] is Relation-like set
bool [:SCM+FSA-Memory,NAT:] is set
{2} is finite countable V63() set
[:SCM+FSA-Memory,{2}:] is Relation-like set
(SCM+FSA-Memory --> 2) +* SCM-OK is Relation-like Function-like set
SCM*-VAL is Relation-like 3 -defined Function-like total set
INT * is FinSequenceSet of INT
K277(NAT,INT,(INT *)) is set
SCM+FSA-OK * SCM*-VAL is Relation-like non-empty SCM+FSA-Memory -defined SCM+FSA-Memory -defined Function-like set
product (SCM+FSA-OK * SCM*-VAL) is non empty functional with_common_domain product-like set
SCM+FSA-Instr is Relation-like non empty standard-ins V72() V73() V75() set
13 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
Segm 13 is countable Element of bool omega
10 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
{9,10} is finite countable V63() set
{ [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
11 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
12 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
{11,12} is finite countable V63() set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM-Data-Loc , b3 is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } is set
(SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } ) \/ { [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM-Data-Loc , b3 is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } is set
K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))) is set
[:SCM+FSA-Instr,K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))):] is Relation-like set
bool [:SCM+FSA-Instr,K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))):] is set
COMPLEX is set
RAT is set
0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(SCM+FSA-OK * SCM*-VAL) . NAT is set
SCM+FSA-Data-Loc is non empty Element of bool SCM+FSA-Memory
SCM+FSA-Data*-Loc is non empty Element of bool SCM+FSA-Memory
SCM+FSA-Exec is Relation-like SCM+FSA-Instr -defined K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))) -valued Function-like V38( SCM+FSA-Instr ,K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL)))) Element of bool [:SCM+FSA-Instr,K165((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))):]
proj1 (SCM+FSA-OK * SCM*-VAL) is set
IC is V49( SCM ) Element of the carrier of SCM
the ZeroF of SCM is Element of the carrier of SCM
halt SCM is halting Element of the InstructionsF of SCM
halt the InstructionsF of SCM is V74( the InstructionsF of SCM) Element of the InstructionsF of SCM
[0,{},{}] is V13() V14() set
[0,{}] is non natural V13() set
{0,{}} is finite countable set
{0} is finite countable set
{{0,{}},{0}} is finite V30() countable set
[[0,{}],{}] is non natural V13() set
SCM-Data-Loc is non empty Element of bool SCM-Memory
{{}} is finite countable set
[:{{}},omega:] is Relation-like set
omega \/ [:{{}},omega:] is set
[{},{}] is non natural V13() set
{{},{}} is finite countable set
{{{},{}},{{}}} is finite V30() countable set
{[{},{}]} is Relation-like Function-like finite countable set
(omega \/ [:{{}},omega:]) \ {[{},{}]} is Element of bool (omega \/ [:{{}},omega:])
bool (omega \/ [:{{}},omega:]) is set
In (NAT,SCM+FSA-Memory) is Element of SCM+FSA-Memory
AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #) is strict AMI-Struct over 3
() is strict AMI-Struct over 3
the carrier of () is set
the_Values_of () is Relation-like the carrier of () -defined Function-like total set
the Object-Kind of () is Relation-like the carrier of () -defined 3 -valued Function-like V38( the carrier of (),3) Element of bool [: the carrier of (),3:]
[: the carrier of (),3:] is Relation-like set
bool [: the carrier of (),3:] is set
the ValuesF of () is Relation-like 3 -defined Function-like total set
the Object-Kind of () * the ValuesF of () is Relation-like the carrier of () -defined Function-like set
<*0*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like FinSequence of NAT
[6,<*0*>,{}] is V13() V14() set
[6,<*0*>] is non natural V13() set
{6,<*0*>} is finite countable set
{6} is finite countable V63() set
{{6,<*0*>},{6}} is finite V30() countable set
[[6,<*0*>],{}] is non natural V13() set
{[6,<*0*>],{}} is finite countable set
{[6,<*0*>]} is Relation-like Function-like finite countable set
{{[6,<*0*>],{}},{[6,<*0*>]}} is finite V30() countable set
the InstructionsF of () is Relation-like non empty standard-ins V72() V73() V75() set
IC is V49(()) Element of the carrier of ()
the carrier of () is non empty set
the ZeroF of () is Element of the carrier of ()
bool the carrier of () is set
() is Element of bool the carrier of ()
the Element of SCM+FSA-Data-Loc is Element of SCM+FSA-Data-Loc
fa is Element of the carrier of ()
the Element of SCM+FSA-Data*-Loc is Element of SCM+FSA-Data*-Loc
a is Element of the carrier of ()
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
dl. fa is Int-like Element of the carrier of SCM
[1,fa] is non natural V13() set
{1,fa} is finite countable set
{1} is finite countable V63() set
{{1,fa},{1}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
fa + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (fa + 1) is V24() V25() integer ext-real non positive set
- 0 is V24() V25() integer ext-real non positive set
a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (a + 1) is V24() V25() integer ext-real non positive set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
(fa) is ()
fa + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (fa + 1) is V24() V25() integer ext-real non positive set
(a) is ()
a + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (a + 1) is V24() V25() integer ext-real non positive set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of SCM
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
dl. c is Int-like Element of the carrier of SCM
[1,c] is non natural V13() set
{1,c} is finite countable set
{{1,c},{1}} is finite V30() countable set
(c) is Int-like Element of the carrier of ()
fa is ()
a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
- a is V24() V25() integer ext-real non positive set
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
c + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(s) is ()
s + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (s + 1) is V24() V25() integer ext-real non positive set
[:NAT, the carrier of ():] is Relation-like set
bool [:NAT, the carrier of ():] is set
fa is Relation-like NAT -defined the carrier of () -valued Function-like V38( NAT , the carrier of ()) Element of bool [:NAT, the carrier of ():]
proj1 fa is set
proj2 fa is set
a is set
c is set
fa . a is set
fa . c is set
dom fa is countable Element of bool NAT
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(s) is ()
s + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (s + 1) is V24() V25() integer ext-real non positive set
fa . s is Element of the carrier of ()
a3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(a3) is ()
a3 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (a3 + 1) is V24() V25() integer ext-real non positive set
dom fa is countable Element of bool NAT
rng fa is Element of bool the carrier of ()
a is set
c is set
fa . c is set
s is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(s) is ()
s + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (s + 1) is V24() V25() integer ext-real non positive set
a is set
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(c) is ()
c + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V25() integer V63() ext-real positive non negative Element of NAT
- (c + 1) is V24() V25() integer ext-real non positive set
fa . c is Element of the carrier of ()
fa is Int-like Element of the carrier of ()
fa is Int-like Element of the carrier of ()
Values fa is non empty set
the_Values_of () is Relation-like non-empty the carrier of () -defined Function-like total set
the Object-Kind of () is Relation-like the carrier of () -defined 3 -valued Function-like V38( the carrier of (),3) Element of bool [: the carrier of (),3:]
[: the carrier of (),3:] is Relation-like set
bool [: the carrier of (),3:] is set
the ValuesF of () is Relation-like 3 -defined Function-like total set
the Object-Kind of () * the ValuesF of () is Relation-like the carrier of () -defined Function-like set
(the_Values_of ()) . fa is set
fa is ()
Values fa is non empty set
the_Values_of () is Relation-like non-empty the carrier of () -defined Function-like total set
the Object-Kind of () is Relation-like the carrier of () -defined 3 -valued Function-like V38( the carrier of (),3) Element of bool [: the carrier of (),3:]
[: the carrier of (),3:] is Relation-like set
bool [: the carrier of (),3:] is set
the ValuesF of () is Relation-like 3 -defined Function-like total set
the Object-Kind of () * the ValuesF of () is Relation-like the carrier of () -defined Function-like set
(the_Values_of ()) . fa is set
the InstructionsF of () is Relation-like non empty standard-ins V72() V73() V75() set
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM+FSA-Data-Loc , b3 is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
s is Element of SCM+FSA-Data*-Loc
<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set
fa `1_3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
{ [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
s is Element of SCM+FSA-Data-Loc
<*c,a3,s*> is set
[a,{},<*c,a3,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,a3,s*>] is non natural V13() set
{[a,{}],<*c,a3,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,a3,s*>},{[a,{}]}} is finite V30() countable set
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
{ [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 13, b2 is Element of SCM+FSA-Data-Loc , b3 is Element of SCM+FSA-Data*-Loc : b1 in {11,12} } is set
a is Element of the InstructionsF of SCM
InsCode a is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K39( the InstructionsF of SCM) is set
proj1 the InstructionsF of SCM is non empty set
proj1 (proj1 the InstructionsF of SCM) is set
K29(a) is set
K29(K29(a)) is set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
a3 is Element of SCM+FSA-Data*-Loc
s is Element of SCM+FSA-Data-Loc
<*c,a3,s*> is set
[a,{},<*c,a3,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,a3,s*>] is non natural V13() set
{[a,{}],<*c,a3,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,a3,s*>},{[a,{}]}} is finite V30() countable set
fa `1_3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
a is Element of Segm 13
c is Element of SCM+FSA-Data-Loc
s is Element of SCM+FSA-Data*-Loc
<*c,s*> is set
[a,{},<*c,s*>] is V13() V14() set
[a,{}] is non natural V13() set
{a,{}} is finite countable set
{a} is finite countable set
{{a,{}},{a}} is finite V30() countable set
[[a,{}],<*c,s*>] is non natural V13() set
{[a,{}],<*c,s*>} is finite countable set
{[a,{}]} is Relation-like Function-like finite countable set
{{[a,{}],<*c,s*>},{[a,{}]}} is finite V30() countable set
fa `1_3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative set
fa is Element of the InstructionsF of SCM
{ [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
SCM-Instr \/ { [b1,{},<*b2,b4,b3*>] where b1 is Element of Segm 13, b2, b3 is Element of SCM+FSA-Data-Loc , b4 is Element of SCM+FSA-Data*-Loc : b1 in {9,10} } is set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
c := s is Element of the InstructionsF of SCM
<*c,s*> is set
[1,{},<*c,s*>] is V13() V14() set
[1,{}] is non natural V13() set
{1,{}} is finite countable set
{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*c,s*>] is non natural V13() set
{[1,{}],<*c,s*>} is finite countable set
{[1,{}]} is Relation-like Function-like finite countable set
{{[1,{}],<*c,s*>},{[1,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
a3 := t is Element of the InstructionsF of SCM
<*a3,t*> is set
[1,{},<*a3,t*>] is V13() V14() set
[1,{}] is non natural V13() set
{1,{}} is finite countable set
{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*a3,t*>] is non natural V13() set
{[1,{}],<*a3,t*>} is finite countable set
{[1,{}]} is Relation-like Function-like finite countable set
{{[1,{}],<*a3,t*>},{[1,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
t := w is Element of the InstructionsF of SCM
<*t,w*> is set
[1,{},<*t,w*>] is V13() V14() set
[[1,{}],<*t,w*>] is non natural V13() set
{[1,{}],<*t,w*>} is finite countable set
{{[1,{}],<*t,w*>},{[1,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
AddTo (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[2,{},<*c,s*>] is V13() V14() set
[2,{}] is non natural V13() set
{2,{}} is finite countable set
{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*c,s*>] is non natural V13() set
{[2,{}],<*c,s*>} is finite countable set
{[2,{}]} is Relation-like Function-like finite countable set
{{[2,{}],<*c,s*>},{[2,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
AddTo (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[2,{},<*a3,t*>] is V13() V14() set
[2,{}] is non natural V13() set
{2,{}} is finite countable set
{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*a3,t*>] is non natural V13() set
{[2,{}],<*a3,t*>} is finite countable set
{[2,{}]} is Relation-like Function-like finite countable set
{{[2,{}],<*a3,t*>},{[2,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
AddTo (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[2,{},<*t,w*>] is V13() V14() set
[[2,{}],<*t,w*>] is non natural V13() set
{[2,{}],<*t,w*>} is finite countable set
{{[2,{}],<*t,w*>},{[2,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
SubFrom (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[3,{},<*c,s*>] is V13() V14() set
[3,{}] is non natural V13() set
{3,{}} is finite countable set
{3} is finite countable V63() set
{{3,{}},{3}} is finite V30() countable set
[[3,{}],<*c,s*>] is non natural V13() set
{[3,{}],<*c,s*>} is finite countable set
{[3,{}]} is Relation-like Function-like finite countable set
{{[3,{}],<*c,s*>},{[3,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
SubFrom (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[3,{},<*a3,t*>] is V13() V14() set
[3,{}] is non natural V13() set
{3,{}} is finite countable set
{3} is finite countable V63() set
{{3,{}},{3}} is finite V30() countable set
[[3,{}],<*a3,t*>] is non natural V13() set
{[3,{}],<*a3,t*>} is finite countable set
{[3,{}]} is Relation-like Function-like finite countable set
{{[3,{}],<*a3,t*>},{[3,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
SubFrom (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[3,{},<*t,w*>] is V13() V14() set
[[3,{}],<*t,w*>] is non natural V13() set
{[3,{}],<*t,w*>} is finite countable set
{{[3,{}],<*t,w*>},{[3,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
MultBy (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[4,{},<*c,s*>] is V13() V14() set
[4,{}] is non natural V13() set
{4,{}} is finite countable set
{4} is finite countable V63() set
{{4,{}},{4}} is finite V30() countable set
[[4,{}],<*c,s*>] is non natural V13() set
{[4,{}],<*c,s*>} is finite countable set
{[4,{}]} is Relation-like Function-like finite countable set
{{[4,{}],<*c,s*>},{[4,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
MultBy (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[4,{},<*a3,t*>] is V13() V14() set
[4,{}] is non natural V13() set
{4,{}} is finite countable set
{4} is finite countable V63() set
{{4,{}},{4}} is finite V30() countable set
[[4,{}],<*a3,t*>] is non natural V13() set
{[4,{}],<*a3,t*>} is finite countable set
{[4,{}]} is Relation-like Function-like finite countable set
{{[4,{}],<*a3,t*>},{[4,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
MultBy (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[4,{},<*t,w*>] is V13() V14() set
[[4,{}],<*t,w*>] is non natural V13() set
{[4,{}],<*t,w*>} is finite countable set
{{[4,{}],<*t,w*>},{[4,{}]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
Divide (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[5,{},<*c,s*>] is V13() V14() set
[5,{}] is non natural V13() set
{5,{}} is finite countable set
{5} is finite countable V63() set
{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*c,s*>] is non natural V13() set
{[5,{}],<*c,s*>} is finite countable set
{[5,{}]} is Relation-like Function-like finite countable set
{{[5,{}],<*c,s*>},{[5,{}]}} is finite V30() countable set
a3 is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
t is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
Divide (a3,t) is Element of the InstructionsF of SCM
<*a3,t*> is set
[5,{},<*a3,t*>] is V13() V14() set
[5,{}] is non natural V13() set
{5,{}} is finite countable set
{5} is finite countable V63() set
{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*a3,t*>] is non natural V13() set
{[5,{}],<*a3,t*>} is finite countable set
{[5,{}]} is Relation-like Function-like finite countable set
{{[5,{}],<*a3,t*>},{[5,{}]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
w is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
Divide (t,w) is Element of the InstructionsF of SCM
<*t,w*> is set
[5,{},<*t,w*>] is V13() V14() set
[[5,{}],<*t,w*>] is non natural V13() set
{[5,{}],<*t,w*>} is finite countable set
{{[5,{}],<*t,w*>},{[5,{}]}} is finite V30() countable set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
SCM-goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
[6,<*fa*>,{}] is V13() V14() set
[6,<*fa*>] is non natural V13() set
{6,<*fa*>} is finite countable set
{6} is finite countable V63() set
{{6,<*fa*>},{6}} is finite V30() countable set
[[6,<*fa*>],{}] is non natural V13() set
{[6,<*fa*>],{}} is finite countable set
{[6,<*fa*>]} is Relation-like Function-like finite countable set
{{[6,<*fa*>],{}},{[6,<*fa*>]}} is finite V30() countable set
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of SCM
c =0_goto fa is Element of the InstructionsF of SCM
<*c*> is Relation-like Function-like set
[7,<*fa*>,<*c*>] is V13() V14() set
[7,<*fa*>] is non natural V13() set
{7,<*fa*>} is finite countable set
{7} is finite countable V63() set
{{7,<*fa*>},{7}} is finite V30() countable set
[[7,<*fa*>],<*c*>] is non natural V13() set
{[7,<*fa*>],<*c*>} is finite countable set
{[7,<*fa*>]} is Relation-like Function-like finite countable set
{{[7,<*fa*>],<*c*>},{[7,<*fa*>]}} is finite V30() countable set
s is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
a3 =0_goto fa is Element of the InstructionsF of SCM
<*a3*> is Relation-like Function-like set
[7,<*fa*>,<*a3*>] is V13() V14() set
[7,<*fa*>] is non natural V13() set
{7,<*fa*>} is finite countable set
{7} is finite countable V63() set
{{7,<*fa*>},{7}} is finite V30() countable set
[[7,<*fa*>],<*a3*>] is non natural V13() set
{[7,<*fa*>],<*a3*>} is finite countable set
{[7,<*fa*>]} is Relation-like Function-like finite countable set
{{[7,<*fa*>],<*a3*>},{[7,<*fa*>]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
t =0_goto fa is Element of the InstructionsF of SCM
<*t*> is Relation-like Function-like set
[7,<*fa*>,<*t*>] is V13() V14() set
[[7,<*fa*>],<*t*>] is non natural V13() set
{[7,<*fa*>],<*t*>} is finite countable set
{{[7,<*fa*>],<*t*>},{[7,<*fa*>]}} is finite V30() countable set
c is Int-like Element of the carrier of SCM
c >0_goto fa is Element of the InstructionsF of SCM
<*c*> is Relation-like Function-like set
[8,<*fa*>,<*c*>] is V13() V14() set
[8,<*fa*>] is non natural V13() set
{8,<*fa*>} is finite countable set
{8} is finite countable V63() set
{{8,<*fa*>},{8}} is finite V30() countable set
[[8,<*fa*>],<*c*>] is non natural V13() set
{[8,<*fa*>],<*c*>} is finite countable set
{[8,<*fa*>]} is Relation-like Function-like finite countable set
{{[8,<*fa*>],<*c*>},{[8,<*fa*>]}} is finite V30() countable set
s is Element of the InstructionsF of ()
a3 is Int-like Element of the carrier of SCM
c is Element of the InstructionsF of ()
a3 >0_goto fa is Element of the InstructionsF of SCM
<*a3*> is Relation-like Function-like set
[8,<*fa*>,<*a3*>] is V13() V14() set
[8,<*fa*>] is non natural V13() set
{8,<*fa*>} is finite countable set
{8} is finite countable V63() set
{{8,<*fa*>},{8}} is finite V30() countable set
[[8,<*fa*>],<*a3*>] is non natural V13() set
{[8,<*fa*>],<*a3*>} is finite countable set
{[8,<*fa*>]} is Relation-like Function-like finite countable set
{{[8,<*fa*>],<*a3*>},{[8,<*fa*>]}} is finite V30() countable set
t is Int-like Element of the carrier of SCM
s is Element of the InstructionsF of ()
t >0_goto fa is Element of the InstructionsF of SCM
<*t*> is Relation-like Function-like set
[8,<*fa*>,<*t*>] is V13() V14() set
[[8,<*fa*>],<*t*>] is non natural V13() set
{[8,<*fa*>],<*t*>} is finite countable set
{{[8,<*fa*>],<*t*>},{[8,<*fa*>]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
c is ()
a is Int-like Element of the carrier of ()
<*fa,c,a*> is set
[9,{},<*fa,c,a*>] is V13() V14() set
[9,{}] is non natural V13() set
{9,{}} is finite countable set
{9} is finite countable V63() set
{{9,{}},{9}} is finite V30() countable set
[[9,{}],<*fa,c,a*>] is non natural V13() set
{[9,{}],<*fa,c,a*>} is finite countable set
{[9,{}]} is Relation-like Function-like finite countable set
{{[9,{}],<*fa,c,a*>},{[9,{}]}} is finite V30() countable set
a3 is Element of SCM-Data-Loc
s is Element of SCM+FSA-Data*-Loc
t is Element of SCM-Data-Loc
<*a3,s,t*> is set
[9,{},<*a3,s,t*>] is V13() V14() set
[[9,{}],<*a3,s,t*>] is non natural V13() set
{[9,{}],<*a3,s,t*>} is finite countable set
{{[9,{}],<*a3,s,t*>},{[9,{}]}} is finite V30() countable set
[10,{},<*fa,c,a*>] is V13() V14() set
[10,{}] is non natural V13() set
{10,{}} is finite countable set
{10} is finite countable V63() set
{{10,{}},{10}} is finite V30() countable set
[[10,{}],<*fa,c,a*>] is non natural V13() set
{[10,{}],<*fa,c,a*>} is finite countable set
{[10,{}]} is Relation-like Function-like finite countable set
{{[10,{}],<*fa,c,a*>},{[10,{}]}} is finite V30() countable set
a3 is Element of SCM-Data-Loc
s is Element of SCM+FSA-Data*-Loc
t is Element of SCM-Data-Loc
<*a3,s,t*> is set
[10,{},<*a3,s,t*>] is V13() V14() set
[[10,{}],<*a3,s,t*>] is non natural V13() set
{[10,{}],<*a3,s,t*>} is finite countable set
{{[10,{}],<*a3,s,t*>},{[10,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is ()
<*fa,a*> is set
[11,{},<*fa,a*>] is V13() V14() set
[11,{}] is non natural V13() set
{11,{}} is finite countable set
{11} is finite countable V63() set
{{11,{}},{11}} is finite V30() countable set
[[11,{}],<*fa,a*>] is non natural V13() set
{[11,{}],<*fa,a*>} is finite countable set
{[11,{}]} is Relation-like Function-like finite countable set
{{[11,{}],<*fa,a*>},{[11,{}]}} is finite V30() countable set
s is Element of SCM-Data-Loc
c is Element of SCM+FSA-Data*-Loc
<*s,c*> is set
[11,{},<*s,c*>] is V13() V14() set
[[11,{}],<*s,c*>] is non natural V13() set
{[11,{}],<*s,c*>} is finite countable set
{{[11,{}],<*s,c*>},{[11,{}]}} is finite V30() countable set
[12,{},<*fa,a*>] is V13() V14() set
[12,{}] is non natural V13() set
{12,{}} is finite countable set
{12} is finite countable V63() set
{{12,{}},{12}} is finite V30() countable set
[[12,{}],<*fa,a*>] is non natural V13() set
{[12,{}],<*fa,a*>} is finite countable set
{[12,{}]} is Relation-like Function-like finite countable set
{{[12,{}],<*fa,a*>},{[12,{}]}} is finite V30() countable set
s is Element of SCM-Data-Loc
c is Element of SCM+FSA-Data*-Loc
<*s,c*> is set
[12,{},<*s,c*>] is V13() V14() set
[[12,{}],<*s,c*>] is non natural V13() set
{[12,{}],<*s,c*>} is finite countable set
{{[12,{}],<*s,c*>},{[12,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
c := s is Element of the InstructionsF of SCM
<*c,s*> is set
[1,{},<*c,s*>] is V13() V14() set
[1,{}] is non natural V13() set
{1,{}} is finite countable set
{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*c,s*>] is non natural V13() set
{[1,{}],<*c,s*>} is finite countable set
{[1,{}]} is Relation-like Function-like finite countable set
{{[1,{}],<*c,s*>},{[1,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
AddTo (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[2,{},<*c,s*>] is V13() V14() set
[2,{}] is non natural V13() set
{2,{}} is finite countable set
{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*c,s*>] is non natural V13() set
{[2,{}],<*c,s*>} is finite countable set
{[2,{}]} is Relation-like Function-like finite countable set
{{[2,{}],<*c,s*>},{[2,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
SubFrom (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[3,{},<*c,s*>] is V13() V14() set
[3,{}] is non natural V13() set
{3,{}} is finite countable set
{3} is finite countable V63() set
{{3,{}},{3}} is finite V30() countable set
[[3,{}],<*c,s*>] is non natural V13() set
{[3,{}],<*c,s*>} is finite countable set
{[3,{}]} is Relation-like Function-like finite countable set
{{[3,{}],<*c,s*>},{[3,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
MultBy (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[4,{},<*c,s*>] is V13() V14() set
[4,{}] is non natural V13() set
{4,{}} is finite countable set
{4} is finite countable V63() set
{{4,{}},{4}} is finite V30() countable set
[[4,{}],<*c,s*>] is non natural V13() set
{[4,{}],<*c,s*>} is finite countable set
{[4,{}]} is Relation-like Function-like finite countable set
{{[4,{}],<*c,s*>},{[4,{}]}} is finite V30() countable set
fa is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
Divide (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[5,{},<*c,s*>] is V13() V14() set
[5,{}] is non natural V13() set
{5,{}} is finite countable set
{5} is finite countable V63() set
{{5,{}},{5}} is finite V30() countable set
[[5,{}],<*c,s*>] is non natural V13() set
{[5,{}],<*c,s*>} is finite countable set
{[5,{}]} is Relation-like Function-like finite countable set
{{[5,{}],<*c,s*>},{[5,{}]}} is finite V30() countable set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
(fa) is Element of the InstructionsF of ()
SCM-goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
[6,<*fa*>,{}] is V13() V14() set
[6,<*fa*>] is non natural V13() set
{6,<*fa*>} is finite countable set
{{6,<*fa*>},{6}} is finite V30() countable set
[[6,<*fa*>],{}] is non natural V13() set
InsCode (fa) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa)) is set
K29(K29((fa))) is set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
c =0_goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
<*c*> is Relation-like Function-like set
[7,<*fa*>,<*c*>] is V13() V14() set
[7,<*fa*>] is non natural V13() set
{7,<*fa*>} is finite countable set
{7} is finite countable V63() set
{{7,<*fa*>},{7}} is finite V30() countable set
[[7,<*fa*>],<*c*>] is non natural V13() set
{[7,<*fa*>],<*c*>} is finite countable set
{[7,<*fa*>]} is Relation-like Function-like finite countable set
{{[7,<*fa*>],<*c*>},{[7,<*fa*>]}} is finite V30() countable set
fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of NAT
a is Int-like Element of the carrier of ()
(fa,a) is Element of the InstructionsF of ()
InsCode (fa,a) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((fa,a)) is set
K29(K29((fa,a))) is set
c is Int-like Element of the carrier of SCM
c >0_goto fa is Element of the InstructionsF of SCM
<*fa*> is Relation-like Function-like set
<*c*> is Relation-like Function-like set
[8,<*fa*>,<*c*>] is V13() V14() set
[8,<*fa*>] is non natural V13() set
{8,<*fa*>} is finite countable set
{8} is finite countable V63() set
{{8,<*fa*>},{8}} is finite V30() countable set
[[8,<*fa*>],<*c*>] is non natural V13() set
{[8,<*fa*>],<*c*>} is finite countable set
{[8,<*fa*>]} is Relation-like Function-like finite countable set
{{[8,<*fa*>],<*c*>},{[8,<*fa*>]}} is finite V30() countable set
a is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of ()
fa is ()
(a,c,fa) is Element of the InstructionsF of ()
<*a,fa,c*> is set
[9,{},<*a,fa,c*>] is V13() V14() set
[[9,{}],<*a,fa,c*>] is non natural V13() set
{[9,{}],<*a,fa,c*>} is finite countable set
{{[9,{}],<*a,fa,c*>},{[9,{}]}} is finite V30() countable set
InsCode (a,c,fa) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((a,c,fa)) is set
K29(K29((a,c,fa))) is set
c is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
fa is ()
(c,a,fa) is Element of the InstructionsF of ()
<*c,fa,a*> is set
[10,{},<*c,fa,a*>] is V13() V14() set
[[10,{}],<*c,fa,a*>] is non natural V13() set
{[10,{}],<*c,fa,a*>} is finite countable set
{{[10,{}],<*c,fa,a*>},{[10,{}]}} is finite V30() countable set
InsCode (c,a,fa) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((c,a,fa)) is set
K29(K29((c,a,fa))) is set
a is Int-like Element of the carrier of ()
fa is ()
(a,fa) is Element of the InstructionsF of ()
<*a,fa*> is set
[11,{},<*a,fa*>] is V13() V14() set
[[11,{}],<*a,fa*>] is non natural V13() set
{[11,{}],<*a,fa*>} is finite countable set
{{[11,{}],<*a,fa*>},{[11,{}]}} is finite V30() countable set
InsCode (a,fa) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((a,fa)) is set
K29(K29((a,fa))) is set
a is Int-like Element of the carrier of ()
fa is ()
(a,fa) is Element of the InstructionsF of ()
<*a,fa*> is set
[12,{},<*a,fa*>] is V13() V14() set
[[12,{}],<*a,fa*>] is non natural V13() set
{[12,{}],<*a,fa*>} is finite countable set
{{[12,{}],<*a,fa*>},{[12,{}]}} is finite V30() countable set
InsCode (a,fa) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29((a,fa)) is set
K29(K29((a,fa))) is set
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
c := s is Element of the InstructionsF of SCM
<*c,s*> is set
[1,{},<*c,s*>] is V13() V14() set
[1,{}] is non natural V13() set
{1,{}} is finite countable set
{{1,{}},{1}} is finite V30() countable set
[[1,{}],<*c,s*>] is non natural V13() set
{[1,{}],<*c,s*>} is finite countable set
{[1,{}]} is Relation-like Function-like finite countable set
{{[1,{}],<*c,s*>},{[1,{}]}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
a3 is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(a3,t) is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
AddTo (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[2,{},<*c,s*>] is V13() V14() set
[2,{}] is non natural V13() set
{2,{}} is finite countable set
{{2,{}},{2}} is finite V30() countable set
[[2,{}],<*c,s*>] is non natural V13() set
{[2,{}],<*c,s*>} is finite countable set
{[2,{}]} is Relation-like Function-like finite countable set
{{[2,{}],<*c,s*>},{[2,{}]}} is finite V30() countable set
() is non empty Element of bool the carrier of ()
a3 is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(a3,t) is Element of the InstructionsF of ()
fa is Element of the InstructionsF of ()
InsCode fa is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real non negative Element of InsCodes the InstructionsF of ()
InsCodes the InstructionsF of () is non empty set
K39( the InstructionsF of ()) is set
proj1 the InstructionsF of () is non empty set
proj1 (proj1 the InstructionsF of ()) is set
K29(fa) is set
K29(K29(fa)) is set
a is Element of the InstructionsF of SCM
c is Int-like Element of the carrier of SCM
s is Int-like Element of the carrier of SCM
SubFrom (c,s) is Element of the InstructionsF of SCM
<*c,s*> is set
[3,{},<*c,s*>] is V13() V14() set
[3,{}] is non natural V13() set
{3,{}} is finite countable set
{3} is finite countable V63() set
{{3,{}