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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = I } is set
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
{ (b1 `2_3) where b1 is Element of the InstructionsF of SCM+FSA : InsCode b1 = InsCode (goto I) } is set
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