:: SCMFSA_2 semantic presentation

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

{ [b

{[SCM-Halt,{},{}]} \/ { [b

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

{ [b

({[SCM-Halt,{},{}]} \/ { [b

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

{ [b

(({[SCM-Halt,{},{}]} \/ { [b

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

{ [b

SCM-Instr \/ { [b

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

{ [b

(SCM-Instr \/ { [b

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

{ [b

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

{ [b

SCM-Instr \/ { [b

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

{ [b

SCM-Instr \/ { [b

{ [b

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

{ [b

SCM-Instr \/ { [b

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,{}