:: SCMFSA10 semantic presentation

REAL is non empty V28() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V28() cardinal limit_cardinal countable denumerable Element of K6(REAL)

K6(REAL) is V28() set

SCM+FSA is V44() with_non-empty_values IC-Ins-separated strict V91(3) AMI-Struct over 3

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

SCM+FSA-Memory is set

K514(NAT,SCM+FSA-Memory) is Element of SCM+FSA-Memory

K376() is non empty set

SCM+FSA-OK is Relation-like SCM+FSA-Memory -defined 3 -valued Function-like V40( SCM+FSA-Memory ,3) Element of K6(K7(SCM+FSA-Memory,3))

K7(SCM+FSA-Memory,3) is Relation-like set

K6(K7(SCM+FSA-Memory,3)) is set

SCM*-VAL is Relation-like 3 -defined Function-like total V147() set

SCM+FSA-Exec is Relation-like K376() -defined K162((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))) -valued Function-like V40(K376(),K162((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL)))) Element of K6(K7(K376(),K162((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL)))))

SCM+FSA-OK * SCM*-VAL is Relation-like SCM+FSA-Memory -defined Function-like set

product (SCM+FSA-OK * SCM*-VAL) is functional with_common_domain product-like set

K162((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))) is set

K7(K376(),K162((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL)))) is Relation-like set

K6(K7(K376(),K162((product (SCM+FSA-OK * SCM*-VAL)),(product (SCM+FSA-OK * SCM*-VAL))))) is set

AMI-Struct(# SCM+FSA-Memory,K514(NAT,SCM+FSA-Memory),K376(),SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #) is strict AMI-Struct over 3

the U1 of SCM+FSA is set

COMPLEX is non empty V28() set

omega is non empty epsilon-transitive epsilon-connected ordinal V28() cardinal limit_cardinal countable denumerable set

K6(omega) is V28() set

K6(NAT) is V28() set

9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

Segm 9 is countable Element of K6(omega)

SCM-Data-Loc is set

K208() is set

K6(K208()) is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

K7(K208(),2) is Relation-like set

K6(K7(K208(),2)) is set

K210() is Relation-like K208() -defined 2 -valued Function-like V40(K208(),2) Element of K6(K7(K208(),2))

K211() is Relation-like 2 -defined Function-like total V147() set

K210() * K211() is Relation-like K208() -defined Function-like set

product (K210() * K211()) is functional with_common_domain product-like set

SCM-Instr is non empty set

K162((product (K210() * K211())),(product (K210() * K211()))) is set

K7(SCM-Instr,K162((product (K210() * K211())),(product (K210() * K211())))) is Relation-like set

K6(K7(SCM-Instr,K162((product (K210() * K211())),(product (K210() * K211()))))) is set

SCM is V44() with_non-empty_values IC-Ins-separated strict strict V91(2) AMI-Struct over 2

K514(NAT,K208()) is Element of K208()

K216() is Relation-like SCM-Instr -defined K162((product (K210() * K211())),(product (K210() * K211()))) -valued Function-like V40( SCM-Instr ,K162((product (K210() * K211())),(product (K210() * K211())))) Element of K6(K7(SCM-Instr,K162((product (K210() * K211())),(product (K210() * K211())))))

AMI-Struct(# K208(),K514(NAT,K208()),SCM-Instr,K210(),K211(),K216() #) is strict AMI-Struct over 2

the InstructionsF of SCM is non empty Relation-like standard-ins V73() J/A-independent V76() set

the U1 of SCM is set

the_Values_of SCM is Relation-like non-empty the U1 of SCM -defined Function-like total set

the Object-Kind of SCM is Relation-like the U1 of SCM -defined 2 -valued Function-like V40( the U1 of SCM,2) Element of K6(K7( the U1 of SCM,2))

K7( the U1 of SCM,2) is Relation-like set

K6(K7( the U1 of SCM,2)) is set

the ValuesF of SCM is Relation-like 2 -defined Function-like total V147() set

the Object-Kind of SCM * the ValuesF of SCM is Relation-like the U1 of SCM -defined Function-like set

K6( the U1 of SCM+FSA) is set

the InstructionsF of SCM+FSA is non empty Relation-like standard-ins V73() J/A-independent V76() set

INT is non empty V28() set

the_Values_of SCM+FSA is Relation-like non-empty the U1 of SCM+FSA -defined Function-like total set

the Object-Kind of SCM+FSA is Relation-like the U1 of SCM+FSA -defined 3 -valued Function-like V40( the U1 of SCM+FSA,3) Element of K6(K7( the U1 of SCM+FSA,3))

K7( the U1 of SCM+FSA,3) is Relation-like set

K6(K7( the U1 of SCM+FSA,3)) is set

the ValuesF of SCM+FSA is Relation-like 3 -defined Function-like total V147() set

the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA is Relation-like the U1 of SCM+FSA -defined Function-like set

K375() is set

K6(SCM+FSA-Memory) is set

RAT is non empty V28() set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V28() cardinal {} -element Cardinal-yielding countable Function-yielding V95() ext-real non negative V115() V116() V117() V118() V146() V147() set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V28() cardinal {} -element Cardinal-yielding countable Function-yielding V95() ext-real non negative V115() V116() V117() V118() V146() V147() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V28() cardinal {} -element Cardinal-yielding countable Function-yielding V95() ext-real non negative V115() V116() V117() V118() V146() V147() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V28() cardinal {} -element Cardinal-yielding countable Function-yielding V95() ext-real non negative V115() V116() V117() V118() V146() V147() Element of NAT

Seg 1 is countable Element of K6(NAT)

{1} is non empty V2() 1 -element set

Seg 2 is countable Element of K6(NAT)

{1,2} is non empty set

SCM+FSA-Data*-Loc is Element of K6(SCM+FSA-Memory)

INT * is FinSequenceSet of INT

4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

6 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

7 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

10 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

11 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

12 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

IC is Element of the U1 of SCM+FSA

[0,{},{}] is V15() V16() set

[0,{}] is V15() set

{0,{}} is non empty functional set

{0} is non empty V2() functional 1 -element with_common_domain set

{{0,{}},{0}} is non empty set

[[0,{}],{}] is V15() set

{[0,{}],{}} is non empty set

{[0,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[0,{}],{}},{[0,{}]}} is non empty set

halt SCM+FSA is V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

halt the InstructionsF of SCM+FSA is ins-loc-free Element of the InstructionsF of SCM+FSA

halt SCM is V90(2, SCM ) Element of the InstructionsF of SCM

halt the InstructionsF of SCM is ins-loc-free Element of the InstructionsF of SCM

Data-Locations is Element of K6( the U1 of SCM+FSA)

Int-Locations is Element of K6( the U1 of SCM+FSA)

FinSeq-Locations is V28() Element of K6( the U1 of SCM+FSA)

Int-Locations \/ FinSeq-Locations is Element of K6( the U1 of SCM+FSA)

K209() is Element of K6(K208())

InsCodes the InstructionsF of SCM+FSA is non empty set

K97( the InstructionsF of SCM+FSA) is set

proj1 the InstructionsF of SCM+FSA is non empty set

proj1 (proj1 the InstructionsF of SCM+FSA) is set

I is V63() Element of the U1 of SCM+FSA

i1 is V63() Element of the U1 of SCM+FSA

a is V11() V12() integer ext-real set

j is V11() V12() integer ext-real set

(I,i1) --> (a,j) is non empty Relation-like Function-like set

Values i1 is non empty set

(the_Values_of SCM+FSA) . i1 is set

Values I is non empty set

(the_Values_of SCM+FSA) . I is set

s1 is Element of Values I

k is Element of Values i1

(I,i1) --> (s1,k) is non empty Relation-like the U1 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set

I is Element of the U1 of SCM+FSA

I is V63() Element of the U1 of SCM+FSA

i1 is V63() Element of the U1 of SCM+FSA

I := i1 is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*I,i1*> is set

[1,{},<*I,i1*>] is V15() V16() set

[1,{}] is V15() set

{1,{}} is non empty set

{{1,{}},{1}} is non empty set

[[1,{}],<*I,i1*>] is V15() set

{[1,{}],<*I,i1*>} is non empty set

{[1,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[1,{}],<*I,i1*>},{[1,{}]}} is non empty set

a is V63() Element of the U1 of SCM

j is V63() Element of the U1 of SCM

a := j is Element of the InstructionsF of SCM

<*a,j*> is set

[1,{},<*a,j*>] is V15() V16() set

[[1,{}],<*a,j*>] is V15() set

{[1,{}],<*a,j*>} is non empty set

{{[1,{}],<*a,j*>},{[1,{}]}} is non empty set

I is V63() Element of the U1 of SCM+FSA

i1 is V63() Element of the U1 of SCM+FSA

AddTo (I,i1) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*I,i1*> is set

[2,{},<*I,i1*>] is V15() V16() set

[2,{}] is V15() set

{2,{}} is non empty set

{2} is non empty V2() 1 -element set

{{2,{}},{2}} is non empty set

[[2,{}],<*I,i1*>] is V15() set

{[2,{}],<*I,i1*>} is non empty set

{[2,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[2,{}],<*I,i1*>},{[2,{}]}} is non empty set

a is V63() Element of the U1 of SCM

j is V63() Element of the U1 of SCM

AddTo (a,j) is Element of the InstructionsF of SCM

<*a,j*> is set

[2,{},<*a,j*>] is V15() V16() set

[[2,{}],<*a,j*>] is V15() set

{[2,{}],<*a,j*>} is non empty set

{{[2,{}],<*a,j*>},{[2,{}]}} is non empty set

I is V63() Element of the U1 of SCM+FSA

i1 is V63() Element of the U1 of SCM+FSA

SubFrom (I,i1) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*I,i1*> is set

[3,{},<*I,i1*>] is V15() V16() set

[3,{}] is V15() set

{3,{}} is non empty set

{3} is non empty V2() 1 -element set

{{3,{}},{3}} is non empty set

[[3,{}],<*I,i1*>] is V15() set

{[3,{}],<*I,i1*>} is non empty set

{[3,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[3,{}],<*I,i1*>},{[3,{}]}} is non empty set

a is V63() Element of the U1 of SCM

j is V63() Element of the U1 of SCM

SubFrom (a,j) is Element of the InstructionsF of SCM

<*a,j*> is set

[3,{},<*a,j*>] is V15() V16() set

[[3,{}],<*a,j*>] is V15() set

{[3,{}],<*a,j*>} is non empty set

{{[3,{}],<*a,j*>},{[3,{}]}} is non empty set

I is V63() Element of the U1 of SCM+FSA

i1 is V63() Element of the U1 of SCM+FSA

MultBy (I,i1) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*I,i1*> is set

[4,{},<*I,i1*>] is V15() V16() set

[4,{}] is V15() set

{4,{}} is non empty set

{4} is non empty V2() 1 -element set

{{4,{}},{4}} is non empty set

[[4,{}],<*I,i1*>] is V15() set

{[4,{}],<*I,i1*>} is non empty set

{[4,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[4,{}],<*I,i1*>},{[4,{}]}} is non empty set

a is V63() Element of the U1 of SCM

j is V63() Element of the U1 of SCM

MultBy (a,j) is Element of the InstructionsF of SCM

<*a,j*> is set

[4,{},<*a,j*>] is V15() V16() set

[[4,{}],<*a,j*>] is V15() set

{[4,{}],<*a,j*>} is non empty set

{{[4,{}],<*a,j*>},{[4,{}]}} is non empty set

I is V63() Element of the U1 of SCM+FSA

i1 is V63() Element of the U1 of SCM+FSA

Divide (I,i1) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*I,i1*> is set

[5,{},<*I,i1*>] is V15() V16() set

[5,{}] is V15() set

{5,{}} is non empty set

{5} is non empty V2() 1 -element set

{{5,{}},{5}} is non empty set

[[5,{}],<*I,i1*>] is V15() set

{[5,{}],<*I,i1*>} is non empty set

{[5,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[5,{}],<*I,i1*>},{[5,{}]}} is non empty set

a is V63() Element of the U1 of SCM

j is V63() Element of the U1 of SCM

Divide (a,j) is Element of the InstructionsF of SCM

<*a,j*> is set

[5,{},<*a,j*>] is V15() V16() set

[[5,{}],<*a,j*>] is V15() set

{[5,{}],<*a,j*>} is non empty set

{{[5,{}],<*a,j*>},{[5,{}]}} is non empty set

I is V63() Element of the U1 of SCM+FSA

<*I*> is Relation-like Function-like set

i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

I =0_goto i1 is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*i1*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

[7,<*i1*>,<*I*>] is V15() V16() set

[7,<*i1*>] is V15() set

{7,<*i1*>} is non empty set

{7} is non empty V2() 1 -element set

{{7,<*i1*>},{7}} is non empty set

[[7,<*i1*>],<*I*>] is V15() set

{[7,<*i1*>],<*I*>} is non empty set

{[7,<*i1*>]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[7,<*i1*>],<*I*>},{[7,<*i1*>]}} is non empty set

a is V63() Element of the U1 of SCM

a =0_goto i1 is Element of the InstructionsF of SCM

<*i1*> is Relation-like Function-like set

<*a*> is Relation-like Function-like set

[7,<*i1*>,<*a*>] is V15() V16() set

[7,<*i1*>] is V15() set

{7,<*i1*>} is non empty set

{{7,<*i1*>},{7}} is non empty set

[[7,<*i1*>],<*a*>] is V15() set

{[7,<*i1*>],<*a*>} is non empty set

{[7,<*i1*>]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[7,<*i1*>],<*a*>},{[7,<*i1*>]}} is non empty set

I is V63() Element of the U1 of SCM+FSA

<*I*> is Relation-like Function-like set

i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

I >0_goto i1 is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*i1*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

[8,<*i1*>,<*I*>] is V15() V16() set

[8,<*i1*>] is V15() set

{8,<*i1*>} is non empty set

{8} is non empty V2() 1 -element set

{{8,<*i1*>},{8}} is non empty set

[[8,<*i1*>],<*I*>] is V15() set

{[8,<*i1*>],<*I*>} is non empty set

{[8,<*i1*>]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[8,<*i1*>],<*I*>},{[8,<*i1*>]}} is non empty set

a is V63() Element of the U1 of SCM

a >0_goto i1 is Element of the InstructionsF of SCM

<*i1*> is Relation-like Function-like set

<*a*> is Relation-like Function-like set

[8,<*i1*>,<*a*>] is V15() V16() set

[8,<*i1*>] is V15() set

{8,<*i1*>} is non empty set

{{8,<*i1*>},{8}} is non empty set

[[8,<*i1*>],<*a*>] is V15() set

{[8,<*i1*>],<*a*>} is non empty set

{[8,<*i1*>]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[8,<*i1*>],<*a*>},{[8,<*i1*>]}} is non empty set

13 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real positive non negative Element of NAT

Segm 13 is countable Element of K6(omega)

(halt SCM+FSA) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((halt SCM+FSA)) is set

K87((halt SCM+FSA)) `3_3 is set

I is V63() Element of the U1 of SCM+FSA

i1 is V63() Element of the U1 of SCM+FSA

I := i1 is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(I := i1) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((I := i1)) is set

K87((I := i1)) `3_3 is set

<*I,i1*> is set

[1,{},<*I,i1*>] is V15() V16() set

[1,{}] is V15() set

{1,{}} is non empty set

{{1,{}},{1}} is non empty set

[[1,{}],<*I,i1*>] is V15() set

{[1,{}],<*I,i1*>} is non empty set

{[1,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[1,{}],<*I,i1*>},{[1,{}]}} is non empty set

[1,{},<*I,i1*>] `2_3 is set

K87([1,{},<*I,i1*>]) is set

K87([1,{},<*I,i1*>]) `3_3 is set

I is V63() Element of the U1 of SCM+FSA

i1 is V63() Element of the U1 of SCM+FSA

AddTo (I,i1) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(AddTo (I,i1)) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((AddTo (I,i1))) is set

K87((AddTo (I,i1))) `3_3 is set

<*I,i1*> is set

[2,{},<*I,i1*>] is V15() V16() set

[2,{}] is V15() set

{2,{}} is non empty set

{2} is non empty V2() 1 -element set

{{2,{}},{2}} is non empty set

[[2,{}],<*I,i1*>] is V15() set

{[2,{}],<*I,i1*>} is non empty set

{[2,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[2,{}],<*I,i1*>},{[2,{}]}} is non empty set

[2,{},<*I,i1*>] `2_3 is set

K87([2,{},<*I,i1*>]) is set

K87([2,{},<*I,i1*>]) `3_3 is set

I is V63() Element of the U1 of SCM+FSA

i1 is V63() Element of the U1 of SCM+FSA

SubFrom (I,i1) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(SubFrom (I,i1)) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((SubFrom (I,i1))) is set

K87((SubFrom (I,i1))) `3_3 is set

<*I,i1*> is set

[3,{},<*I,i1*>] is V15() V16() set

[3,{}] is V15() set

{3,{}} is non empty set

{3} is non empty V2() 1 -element set

{{3,{}},{3}} is non empty set

[[3,{}],<*I,i1*>] is V15() set

{[3,{}],<*I,i1*>} is non empty set

{[3,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[3,{}],<*I,i1*>},{[3,{}]}} is non empty set

[3,{},<*I,i1*>] `2_3 is set

K87([3,{},<*I,i1*>]) is set

K87([3,{},<*I,i1*>]) `3_3 is set

I is V63() Element of the U1 of SCM+FSA

i1 is V63() Element of the U1 of SCM+FSA

MultBy (I,i1) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(MultBy (I,i1)) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((MultBy (I,i1))) is set

K87((MultBy (I,i1))) `3_3 is set

<*I,i1*> is set

[4,{},<*I,i1*>] is V15() V16() set

[4,{}] is V15() set

{4,{}} is non empty set

{4} is non empty V2() 1 -element set

{{4,{}},{4}} is non empty set

[[4,{}],<*I,i1*>] is V15() set

{[4,{}],<*I,i1*>} is non empty set

{[4,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[4,{}],<*I,i1*>},{[4,{}]}} is non empty set

[4,{},<*I,i1*>] `2_3 is set

K87([4,{},<*I,i1*>]) is set

K87([4,{},<*I,i1*>]) `3_3 is set

I is V63() Element of the U1 of SCM+FSA

i1 is V63() Element of the U1 of SCM+FSA

Divide (I,i1) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Divide (I,i1)) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((Divide (I,i1))) is set

K87((Divide (I,i1))) `3_3 is set

<*I,i1*> is set

[5,{},<*I,i1*>] is V15() V16() set

[5,{}] is V15() set

{5,{}} is non empty set

{5} is non empty V2() 1 -element set

{{5,{}},{5}} is non empty set

[[5,{}],<*I,i1*>] is V15() set

{[5,{}],<*I,i1*>} is non empty set

{[5,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[5,{}],<*I,i1*>},{[5,{}]}} is non empty set

[5,{},<*I,i1*>] `2_3 is set

K87([5,{},<*I,i1*>]) is set

K87([5,{},<*I,i1*>]) `3_3 is set

I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

<*I*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

i1 is V63() Element of the U1 of SCM+FSA

i1 =0_goto I is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(i1 =0_goto I) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((i1 =0_goto I)) is set

K87((i1 =0_goto I)) `3_3 is set

<*i1*> is Relation-like Function-like set

[7,<*I*>,<*i1*>] is V15() V16() set

[7,<*I*>] is V15() set

{7,<*I*>} is non empty set

{7} is non empty V2() 1 -element set

{{7,<*I*>},{7}} is non empty set

[[7,<*I*>],<*i1*>] is V15() set

{[7,<*I*>],<*i1*>} is non empty set

{[7,<*I*>]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[7,<*I*>],<*i1*>},{[7,<*I*>]}} is non empty set

[7,<*I*>,<*i1*>] `2_3 is set

K87([7,<*I*>,<*i1*>]) is set

K87([7,<*I*>,<*i1*>]) `3_3 is set

I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

<*I*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

i1 is V63() Element of the U1 of SCM+FSA

i1 >0_goto I is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(i1 >0_goto I) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((i1 >0_goto I)) is set

K87((i1 >0_goto I)) `3_3 is set

<*i1*> is Relation-like Function-like set

[8,<*I*>,<*i1*>] is V15() V16() set

[8,<*I*>] is V15() set

{8,<*I*>} is non empty set

{8} is non empty V2() 1 -element set

{{8,<*I*>},{8}} is non empty set

[[8,<*I*>],<*i1*>] is V15() set

{[8,<*I*>],<*i1*>} is non empty set

{[8,<*I*>]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[8,<*I*>],<*i1*>},{[8,<*I*>]}} is non empty set

[8,<*I*>,<*i1*>] `2_3 is set

K87([8,<*I*>,<*i1*>]) is set

K87([8,<*I*>,<*i1*>]) `3_3 is set

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

i1 is set

a is Element of the InstructionsF of SCM+FSA

a `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(a) is set

K87(a) `3_3 is set

InsCode a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(a)) is set

i1 is set

InsCode (halt SCM+FSA) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87((halt SCM+FSA))) is set

{{}} is non empty V2() functional 1 -element with_common_domain set

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

i1 is set

a is Element of the InstructionsF of SCM+FSA

a `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(a) is set

K87(a) `3_3 is set

InsCode a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(a)) is set

j is V63() Element of the U1 of SCM+FSA

k is V63() Element of the U1 of SCM+FSA

j := k is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

the V63() Element of the U1 of SCM+FSA is V63() Element of the U1 of SCM+FSA

a is set

the V63() Element of the U1 of SCM+FSA := the V63() Element of the U1 of SCM+FSA is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

( the V63() Element of the U1 of SCM+FSA := the V63() Element of the U1 of SCM+FSA) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(( the V63() Element of the U1 of SCM+FSA := the V63() Element of the U1 of SCM+FSA)) is set

K87(( the V63() Element of the U1 of SCM+FSA := the V63() Element of the U1 of SCM+FSA)) `3_3 is set

InsCode ( the V63() Element of the U1 of SCM+FSA := the V63() Element of the U1 of SCM+FSA) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(( the V63() Element of the U1 of SCM+FSA := the V63() Element of the U1 of SCM+FSA))) is set

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

i1 is set

a is Element of the InstructionsF of SCM+FSA

a `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(a) is set

K87(a) `3_3 is set

InsCode a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(a)) is set

j is V63() Element of the U1 of SCM+FSA

k is V63() Element of the U1 of SCM+FSA

AddTo (j,k) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

the V63() Element of the U1 of SCM+FSA is V63() Element of the U1 of SCM+FSA

a is set

AddTo ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(AddTo ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((AddTo ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA))) is set

K87((AddTo ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA))) `3_3 is set

InsCode (AddTo ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87((AddTo ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)))) is set

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

i1 is set

a is Element of the InstructionsF of SCM+FSA

a `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(a) is set

K87(a) `3_3 is set

InsCode a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(a)) is set

j is V63() Element of the U1 of SCM+FSA

k is V63() Element of the U1 of SCM+FSA

SubFrom (j,k) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

the V63() Element of the U1 of SCM+FSA is V63() Element of the U1 of SCM+FSA

a is set

SubFrom ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(SubFrom ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((SubFrom ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA))) is set

K87((SubFrom ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA))) `3_3 is set

InsCode (SubFrom ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87((SubFrom ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)))) is set

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

i1 is set

a is Element of the InstructionsF of SCM+FSA

a `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(a) is set

K87(a) `3_3 is set

InsCode a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(a)) is set

j is V63() Element of the U1 of SCM+FSA

k is V63() Element of the U1 of SCM+FSA

MultBy (j,k) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

the V63() Element of the U1 of SCM+FSA is V63() Element of the U1 of SCM+FSA

a is set

MultBy ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(MultBy ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((MultBy ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA))) is set

K87((MultBy ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA))) `3_3 is set

InsCode (MultBy ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87((MultBy ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)))) is set

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

i1 is set

a is Element of the InstructionsF of SCM+FSA

a `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(a) is set

K87(a) `3_3 is set

InsCode a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(a)) is set

j is V63() Element of the U1 of SCM+FSA

k is V63() Element of the U1 of SCM+FSA

Divide (j,k) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

the V63() Element of the U1 of SCM+FSA is V63() Element of the U1 of SCM+FSA

a is set

Divide ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Divide ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((Divide ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA))) is set

K87((Divide ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA))) `3_3 is set

InsCode (Divide ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87((Divide ( the V63() Element of the U1 of SCM+FSA, the V63() Element of the U1 of SCM+FSA)))) is set

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

product" (JumpParts I) is Relation-like Function-like set

proj1 (product" (JumpParts I)) is set

the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SCM-goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT is Element of the InstructionsF of SCM

<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *> is Relation-like Function-like set

[6,<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *>,{}] is V15() V16() set

[6,<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *>] is V15() set

{6,<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *>} is non empty set

{6} is non empty V2() 1 -element set

{{6,<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *>},{6}} is non empty set

[[6,<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *>],{}] is V15() set

(goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT )) is set

K87((goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT )) `3_3 is set

<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

InsCode (goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87((goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ))) is set

a is set

DOM (JumpParts I) is set

dom ((goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ) `2_3) is countable Element of K6(NAT)

a is set

j is Relation-like Function-like set

proj1 j is set

k is Element of the InstructionsF of SCM+FSA

k `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(k) is set

K87(k) `3_3 is set

InsCode k is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(k)) is set

s1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

goto s1 is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SCM-goto s1 is Element of the InstructionsF of SCM

<*s1*> is Relation-like Function-like set

[6,<*s1*>,{}] is V15() V16() set

[6,<*s1*>] is V15() set

{6,<*s1*>} is non empty set

{{6,<*s1*>},{6}} is non empty set

[[6,<*s1*>],{}] is V15() set

<*s1*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

product" (JumpParts I) is Relation-like Function-like set

proj1 (product" (JumpParts I)) is set

the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

the V63() Element of the U1 of SCM+FSA is V63() Element of the U1 of SCM+FSA

the V63() Element of the U1 of SCM+FSA =0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

( the V63() Element of the U1 of SCM+FSA =0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(( the V63() Element of the U1 of SCM+FSA =0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT )) is set

K87(( the V63() Element of the U1 of SCM+FSA =0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT )) `3_3 is set

<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

InsCode ( the V63() Element of the U1 of SCM+FSA =0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(( the V63() Element of the U1 of SCM+FSA =0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ))) is set

j is set

DOM (JumpParts I) is set

dom (( the V63() Element of the U1 of SCM+FSA =0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ) `2_3) is countable Element of K6(NAT)

j is set

k is Relation-like Function-like set

proj1 k is set

s1 is Element of the InstructionsF of SCM+FSA

s1 `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(s1) is set

K87(s1) `3_3 is set

InsCode s1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(s1)) is set

s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

k is V63() Element of the U1 of SCM+FSA

k =0_goto s2 is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*s2*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

product" (JumpParts I) is Relation-like Function-like set

proj1 (product" (JumpParts I)) is set

the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

the V63() Element of the U1 of SCM+FSA is V63() Element of the U1 of SCM+FSA

the V63() Element of the U1 of SCM+FSA >0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

( the V63() Element of the U1 of SCM+FSA >0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(( the V63() Element of the U1 of SCM+FSA >0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT )) is set

K87(( the V63() Element of the U1 of SCM+FSA >0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT )) `3_3 is set

<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

InsCode ( the V63() Element of the U1 of SCM+FSA >0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(( the V63() Element of the U1 of SCM+FSA >0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ))) is set

j is set

DOM (JumpParts I) is set

dom (( the V63() Element of the U1 of SCM+FSA >0_goto the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT ) `2_3) is countable Element of K6(NAT)

j is set

k is Relation-like Function-like set

proj1 k is set

s1 is Element of the InstructionsF of SCM+FSA

s1 `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(s1) is set

K87(s1) `3_3 is set

InsCode s1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(s1)) is set

s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

k is V63() Element of the U1 of SCM+FSA

k >0_goto s2 is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*s2*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

i1 is set

a is Element of the InstructionsF of SCM+FSA

a `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(a) is set

K87(a) `3_3 is set

InsCode a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(a)) is set

k is V63() Element of the U1 of SCM+FSA

j is V63() Element of the U1 of SCM+FSA

s1 is FinSeq-Location

k := (s1,j) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*k,s1,j*> is set

[9,{},<*k,s1,j*>] is V15() V16() set

[9,{}] is V15() set

{9,{}} is non empty set

{9} is non empty V2() 1 -element set

{{9,{}},{9}} is non empty set

[[9,{}],<*k,s1,j*>] is V15() set

{[9,{}],<*k,s1,j*>} is non empty set

{[9,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[9,{}],<*k,s1,j*>},{[9,{}]}} is non empty set

the V63() Element of the U1 of SCM+FSA is V63() Element of the U1 of SCM+FSA

the FinSeq-Location is FinSeq-Location

j is set

the V63() Element of the U1 of SCM+FSA := ( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location , the V63() Element of the U1 of SCM+FSA*> is set

[9,{},<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location , the V63() Element of the U1 of SCM+FSA*>] is V15() V16() set

[[9,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location , the V63() Element of the U1 of SCM+FSA*>] is V15() set

{[9,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location , the V63() Element of the U1 of SCM+FSA*>} is non empty set

{{[9,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location , the V63() Element of the U1 of SCM+FSA*>},{[9,{}]}} is non empty set

( the V63() Element of the U1 of SCM+FSA := ( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA)) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(( the V63() Element of the U1 of SCM+FSA := ( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA))) is set

K87(( the V63() Element of the U1 of SCM+FSA := ( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA))) `3_3 is set

InsCode ( the V63() Element of the U1 of SCM+FSA := ( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(( the V63() Element of the U1 of SCM+FSA := ( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA)))) is set

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

i1 is set

a is Element of the InstructionsF of SCM+FSA

a `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(a) is set

K87(a) `3_3 is set

InsCode a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(a)) is set

k is V63() Element of the U1 of SCM+FSA

j is V63() Element of the U1 of SCM+FSA

s1 is FinSeq-Location

(s1,j) := k is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*k,s1,j*> is set

[10,{},<*k,s1,j*>] is V15() V16() set

[10,{}] is V15() set

{10,{}} is non empty set

{10} is non empty V2() 1 -element set

{{10,{}},{10}} is non empty set

[[10,{}],<*k,s1,j*>] is V15() set

{[10,{}],<*k,s1,j*>} is non empty set

{[10,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[10,{}],<*k,s1,j*>},{[10,{}]}} is non empty set

the V63() Element of the U1 of SCM+FSA is V63() Element of the U1 of SCM+FSA

the FinSeq-Location is FinSeq-Location

j is set

( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA) := the V63() Element of the U1 of SCM+FSA is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location , the V63() Element of the U1 of SCM+FSA*> is set

[10,{},<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location , the V63() Element of the U1 of SCM+FSA*>] is V15() V16() set

[[10,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location , the V63() Element of the U1 of SCM+FSA*>] is V15() set

{[10,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location , the V63() Element of the U1 of SCM+FSA*>} is non empty set

{{[10,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location , the V63() Element of the U1 of SCM+FSA*>},{[10,{}]}} is non empty set

(( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA) := the V63() Element of the U1 of SCM+FSA) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA) := the V63() Element of the U1 of SCM+FSA)) is set

K87((( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA) := the V63() Element of the U1 of SCM+FSA)) `3_3 is set

InsCode (( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA) := the V63() Element of the U1 of SCM+FSA) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87((( the FinSeq-Location , the V63() Element of the U1 of SCM+FSA) := the V63() Element of the U1 of SCM+FSA))) is set

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

i1 is set

a is Element of the InstructionsF of SCM+FSA

a `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(a) is set

K87(a) `3_3 is set

InsCode a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(a)) is set

j is V63() Element of the U1 of SCM+FSA

k is FinSeq-Location

j :=len k is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*j,k*> is set

[11,{},<*j,k*>] is V15() V16() set

[11,{}] is V15() set

{11,{}} is non empty set

{11} is non empty V2() 1 -element set

{{11,{}},{11}} is non empty set

[[11,{}],<*j,k*>] is V15() set

{[11,{}],<*j,k*>} is non empty set

{[11,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[11,{}],<*j,k*>},{[11,{}]}} is non empty set

the V63() Element of the U1 of SCM+FSA is V63() Element of the U1 of SCM+FSA

the FinSeq-Location is FinSeq-Location

j is set

the V63() Element of the U1 of SCM+FSA :=len the FinSeq-Location is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location *> is set

[11,{},<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location *>] is V15() V16() set

[[11,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location *>] is V15() set

{[11,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location *>} is non empty set

{{[11,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location *>},{[11,{}]}} is non empty set

( the V63() Element of the U1 of SCM+FSA :=len the FinSeq-Location ) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(( the V63() Element of the U1 of SCM+FSA :=len the FinSeq-Location )) is set

K87(( the V63() Element of the U1 of SCM+FSA :=len the FinSeq-Location )) `3_3 is set

InsCode ( the V63() Element of the U1 of SCM+FSA :=len the FinSeq-Location ) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(( the V63() Element of the U1 of SCM+FSA :=len the FinSeq-Location ))) is set

I is Element of InsCodes the InstructionsF of SCM+FSA

JumpParts I is non empty functional with_common_domain product-like set

{ (b

i1 is set

a is Element of the InstructionsF of SCM+FSA

a `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(a) is set

K87(a) `3_3 is set

InsCode a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(a)) is set

j is V63() Element of the U1 of SCM+FSA

k is FinSeq-Location

k :=<0,...,0> j is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*j,k*> is set

[12,{},<*j,k*>] is V15() V16() set

[12,{}] is V15() set

{12,{}} is non empty set

{12} is non empty V2() 1 -element set

{{12,{}},{12}} is non empty set

[[12,{}],<*j,k*>] is V15() set

{[12,{}],<*j,k*>} is non empty set

{[12,{}]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[12,{}],<*j,k*>},{[12,{}]}} is non empty set

the V63() Element of the U1 of SCM+FSA is V63() Element of the U1 of SCM+FSA

the FinSeq-Location is FinSeq-Location

j is set

the FinSeq-Location :=<0,...,0> the V63() Element of the U1 of SCM+FSA is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location *> is set

[12,{},<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location *>] is V15() V16() set

[[12,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location *>] is V15() set

{[12,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location *>} is non empty set

{{[12,{}],<* the V63() Element of the U1 of SCM+FSA, the FinSeq-Location *>},{[12,{}]}} is non empty set

( the FinSeq-Location :=<0,...,0> the V63() Element of the U1 of SCM+FSA) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(( the FinSeq-Location :=<0,...,0> the V63() Element of the U1 of SCM+FSA)) is set

K87(( the FinSeq-Location :=<0,...,0> the V63() Element of the U1 of SCM+FSA)) `3_3 is set

InsCode ( the FinSeq-Location :=<0,...,0> the V63() Element of the U1 of SCM+FSA) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(( the FinSeq-Location :=<0,...,0> the V63() Element of the U1 of SCM+FSA))) is set

I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

goto I is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SCM-goto I is Element of the InstructionsF of SCM

<*I*> is Relation-like Function-like set

[6,<*I*>,{}] is V15() V16() set

[6,<*I*>] is V15() set

{6,<*I*>} is non empty set

{6} is non empty V2() 1 -element set

{{6,<*I*>},{6}} is non empty set

[[6,<*I*>],{}] is V15() set

InsCode (goto I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87((goto I)) is set

K87(K87((goto I))) is set

JumpParts (InsCode (goto I)) is non empty functional with_common_domain product-like set

{ (b

product" (JumpParts (InsCode (goto I))) is Relation-like Function-like set

(product" (JumpParts (InsCode (goto I)))) . 1 is set

proj1 (product" (JumpParts (InsCode (goto I)))) is set

i1 is set

pi ((JumpParts (InsCode (goto I))),1) is set

a is Relation-like Function-like set

a . 1 is set

j is Element of the InstructionsF of SCM+FSA

j `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87(j) is set

K87(j) `3_3 is set

InsCode j is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87(K87(j)) is set

k is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

goto k is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SCM-goto k is Element of the InstructionsF of SCM

<*k*> is Relation-like Function-like set

[6,<*k*>,{}] is V15() V16() set

[6,<*k*>] is V15() set

{6,<*k*>} is non empty set

{{6,<*k*>},{6}} is non empty set

[[6,<*k*>],{}] is V15() set

<*k*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

i1 is set

a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

<*a*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like Cardinal-yielding V115() V116() V117() V118() FinSequence of NAT

<*a*> . 1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative set

goto a is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SCM-goto a is Element of the InstructionsF of SCM

<*a*> is Relation-like Function-like set

[6,<*a*>,{}] is V15() V16() set

[6,<*a*>] is V15() set

{6,<*a*>} is non empty set

{{6,<*a*>},{6}} is non empty set

[[6,<*a*>],{}] is V15() set

InsCode (goto a) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA

K87((goto a)) is set

K87(K87((goto a))) is set

(goto a) `2_3 is Relation-like NAT -valued RAT -valued Function-like FinSequence-like V115() V116() V117() V118() set

K87((goto a)) `3_3 is set

I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT

i1 is V63() Element of the U1 of SCM+FSA

i1 =0_goto I is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of