:: AMI_6 semantic presentation

REAL is set

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

K6(REAL) is set

COMPLEX is 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)

K191() is set

K198() is set

K6(K198()) 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(K198(),2) is Relation-like set

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

K200() is Relation-like Function-like V40(K198(),2) Element of K6(K7(K198(),2))

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

K200() * K201() is Relation-like Function-like set

product (K200() * K201()) is functional with_common_domain product-like set

K192() is non empty set

K152((product (K200() * K201())),(product (K200() * K201()))) is set

K7(K192(),K152((product (K200() * K201())),(product (K200() * K201())))) is Relation-like set

K6(K7(K192(),K152((product (K200() * K201())),(product (K200() * K201()))))) is set

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

K465(NAT,K198()) is Element of K198()

K206() is Relation-like Function-like V40(K192(),K152((product (K200() * K201())),(product (K200() * K201())))) Element of K6(K7(K192(),K152((product (K200() * K201())),(product (K200() * K201())))))

AMI-Struct(# K198(),K465(NAT,K198()),K192(),K200(),K201(),K206() #) 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 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 Function-like set

RAT is set

INT is set

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

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Function-yielding V95() ext-real non negative V115() V116() V117() V118() V146() V147() V148() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Function-yielding V95() ext-real non negative V115() V116() V117() V118() V146() V147() V148() 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

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

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable Function-yielding V95() ext-real non negative V115() V116() V117() V118() V146() V147() V148() 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

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

IC is Element of the U1 of SCM

[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 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)

K6( the U1 of SCM) is set

K199() is Element of K6(K198())

Seg 1 is non empty V2() V28() 1 -element countable Element of K6(NAT)

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

Seg 2 is non empty V28() 2 -element countable Element of K6(NAT)

{1,2} is non empty set

InsCodes the InstructionsF of SCM is non empty set

K87( the InstructionsF of SCM) is set

proj1 the InstructionsF of SCM is non empty set

proj1 (proj1 the InstructionsF of SCM) is set

I is Element of InsCodes the InstructionsF of SCM

a is set

[I,a] is V15() set

{I,a} is non empty set

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

{{I,a},{I}} is non empty set

k1 is set

[[I,a],k1] is V15() set

{[I,a],k1} is non empty set

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

{{[I,a],k1},{[I,a]}} is non empty set

[I,a,k1] is V15() V16() set

i1 is Element of the InstructionsF of SCM

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

K77(i1) is set

K77(K77(i1)) is set

JumpPart (halt SCM) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77((halt SCM)) is set

AddressPart K77((halt SCM)) is set

I is Element of InsCodes the InstructionsF of SCM

JumpParts I is non empty functional with_common_domain product-like set

{ (JumpPart b

a is set

k1 is Element of the InstructionsF of SCM

JumpPart k1 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(k1) is set

AddressPart K77(k1) is set

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

K77(K77(k1)) is set

a is set

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

K77(K77((halt SCM))) is set

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

I is Element of InsCodes the InstructionsF of SCM

JumpParts I is non empty functional with_common_domain product-like set

{ (JumpPart b

a is set

k1 is Element of the InstructionsF of SCM

JumpPart k1 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(k1) is set

AddressPart K77(k1) is set

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

K77(K77(k1)) is set

i1 is V63() Element of the U1 of SCM

j is V63() Element of the U1 of SCM

i1 := j is Element of the InstructionsF of SCM

<*i1,j*> is non empty Relation-like NAT -defined Function-like V28() 2 -element FinSequence-like FinSubsequence-like countable V147() set

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

[1,{}] is V15() set

{1,{}} is non empty set

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

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

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

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

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

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

k1 is set

the V63() Element of the U1 of SCM := the V63() Element of the U1 of SCM is Element of the InstructionsF of SCM

<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*> is non empty Relation-like NAT -defined Function-like V28() 2 -element FinSequence-like FinSubsequence-like countable V147() set

[1,{},<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>] is V15() V16() set

[[1,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>] is V15() set

{[1,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>} is non empty set

{{[1,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>},{[1,{}]}} is non empty set

JumpPart ( the V63() Element of the U1 of SCM := the V63() Element of the U1 of SCM) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(( the V63() Element of the U1 of SCM := the V63() Element of the U1 of SCM)) is set

AddressPart K77(( the V63() Element of the U1 of SCM := the V63() Element of the U1 of SCM)) is set

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

K77(K77(( the V63() Element of the U1 of SCM := the V63() Element of the U1 of SCM))) is set

I is Element of InsCodes the InstructionsF of SCM

JumpParts I is non empty functional with_common_domain product-like set

{ (JumpPart b

a is set

k1 is Element of the InstructionsF of SCM

JumpPart k1 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(k1) is set

AddressPart K77(k1) is set

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

K77(K77(k1)) is set

i1 is V63() Element of the U1 of SCM

j is V63() Element of the U1 of SCM

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

<*i1,j*> is non empty Relation-like NAT -defined Function-like V28() 2 -element FinSequence-like FinSubsequence-like countable V147() set

[2,{},<*i1,j*>] 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,{}],<*i1,j*>] is V15() set

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

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

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

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

k1 is set

AddTo ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM) is Element of the InstructionsF of SCM

<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*> is non empty Relation-like NAT -defined Function-like V28() 2 -element FinSequence-like FinSubsequence-like countable V147() set

[2,{},<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>] is V15() V16() set

[[2,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>] is V15() set

{[2,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>} is non empty set

{{[2,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>},{[2,{}]}} is non empty set

JumpPart (AddTo ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77((AddTo ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM))) is set

AddressPart K77((AddTo ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM))) is set

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

K77(K77((AddTo ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM)))) is set

I is Element of InsCodes the InstructionsF of SCM

JumpParts I is non empty functional with_common_domain product-like set

{ (JumpPart b

a is set

k1 is Element of the InstructionsF of SCM

JumpPart k1 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(k1) is set

AddressPart K77(k1) is set

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

K77(K77(k1)) is set

i1 is V63() Element of the U1 of SCM

j is V63() Element of the U1 of SCM

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

<*i1,j*> is non empty Relation-like NAT -defined Function-like V28() 2 -element FinSequence-like FinSubsequence-like countable V147() set

[3,{},<*i1,j*>] 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,{}],<*i1,j*>] is V15() set

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

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

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

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

k1 is set

SubFrom ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM) is Element of the InstructionsF of SCM

<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*> is non empty Relation-like NAT -defined Function-like V28() 2 -element FinSequence-like FinSubsequence-like countable V147() set

[3,{},<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>] is V15() V16() set

[[3,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>] is V15() set

{[3,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>} is non empty set

{{[3,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>},{[3,{}]}} is non empty set

JumpPart (SubFrom ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77((SubFrom ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM))) is set

AddressPart K77((SubFrom ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM))) is set

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

K77(K77((SubFrom ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM)))) is set

I is Element of InsCodes the InstructionsF of SCM

JumpParts I is non empty functional with_common_domain product-like set

{ (JumpPart b

a is set

k1 is Element of the InstructionsF of SCM

JumpPart k1 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(k1) is set

AddressPart K77(k1) is set

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

K77(K77(k1)) is set

i1 is V63() Element of the U1 of SCM

j is V63() Element of the U1 of SCM

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

<*i1,j*> is non empty Relation-like NAT -defined Function-like V28() 2 -element FinSequence-like FinSubsequence-like countable V147() set

[4,{},<*i1,j*>] 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,{}],<*i1,j*>] is V15() set

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

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

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

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

k1 is set

MultBy ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM) is Element of the InstructionsF of SCM

<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*> is non empty Relation-like NAT -defined Function-like V28() 2 -element FinSequence-like FinSubsequence-like countable V147() set

[4,{},<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>] is V15() V16() set

[[4,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>] is V15() set

{[4,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>} is non empty set

{{[4,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>},{[4,{}]}} is non empty set

JumpPart (MultBy ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77((MultBy ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM))) is set

AddressPart K77((MultBy ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM))) is set

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

K77(K77((MultBy ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM)))) is set

I is Element of InsCodes the InstructionsF of SCM

JumpParts I is non empty functional with_common_domain product-like set

{ (JumpPart b

a is set

k1 is Element of the InstructionsF of SCM

JumpPart k1 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(k1) is set

AddressPart K77(k1) is set

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

K77(K77(k1)) is set

i1 is V63() Element of the U1 of SCM

j is V63() Element of the U1 of SCM

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

<*i1,j*> is non empty Relation-like NAT -defined Function-like V28() 2 -element FinSequence-like FinSubsequence-like countable V147() set

[5,{},<*i1,j*>] 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,{}],<*i1,j*>] is V15() set

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

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

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

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

k1 is set

Divide ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM) is Element of the InstructionsF of SCM

<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*> is non empty Relation-like NAT -defined Function-like V28() 2 -element FinSequence-like FinSubsequence-like countable V147() set

[5,{},<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>] is V15() V16() set

[[5,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>] is V15() set

{[5,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>} is non empty set

{{[5,{}],<* the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM*>},{[5,{}]}} is non empty set

JumpPart (Divide ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM)) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77((Divide ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM))) is set

AddressPart K77((Divide ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM))) is set

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

K77(K77((Divide ( the V63() Element of the U1 of SCM, the V63() Element of the U1 of SCM)))) is set

I is Element of InsCodes the InstructionsF of SCM

JumpParts I is non empty functional with_common_domain product-like set

{ (JumpPart 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

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 non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() 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

{[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,<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *>]} is non empty V2() Relation-like Function-like constant 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,<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *>]}} is non empty set

JumpPart (SCM-goto 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 RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

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

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

<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

InsCode (SCM-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

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

k1 is set

DOM (JumpParts I) is set

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

k1 is set

i1 is Relation-like Function-like set

proj1 i1 is set

j is Element of the InstructionsF of SCM

JumpPart j is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(j) is set

AddressPart K77(j) 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

K77(K77(j)) is set

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

SCM-goto k is Element of the InstructionsF of SCM

<*k*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() 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

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

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

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

<*k*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

I is Element of InsCodes the InstructionsF of SCM

JumpParts I is non empty functional with_common_domain product-like set

{ (JumpPart 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 is V63() Element of the U1 of SCM

the V63() Element of the U1 of SCM =0_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 non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

<* the V63() Element of the U1 of SCM*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

[7,<* the 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*>] is V15() V16() set

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

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

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

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

[[7,<* the 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*>] is V15() set

{[7,<* the 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*>} is non empty set

{[7,<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *>]} is non empty V2() Relation-like Function-like constant 1 -element set

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

JumpPart ( the V63() Element of the U1 of SCM =0_goto 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 RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

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

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

<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

InsCode ( the V63() Element of the U1 of SCM =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

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

i1 is set

DOM (JumpParts I) is set

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

i1 is set

j is Relation-like Function-like set

proj1 j is set

k is Element of the InstructionsF of SCM

JumpPart k is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(k) is set

AddressPart K77(k) 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

K77(K77(k)) is set

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

s2 is V63() Element of the U1 of SCM

s2 =0_goto s1 is Element of the InstructionsF of SCM

<*s1*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

<*s2*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

[7,<*s1*>,<*s2*>] is V15() V16() set

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

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

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

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

{[7,<*s1*>],<*s2*>} is non empty set

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

{{[7,<*s1*>],<*s2*>},{[7,<*s1*>]}} is non empty set

<*s1*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

I is Element of InsCodes the InstructionsF of SCM

JumpParts I is non empty functional with_common_domain product-like set

{ (JumpPart 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 is V63() Element of the U1 of SCM

the V63() Element of the U1 of SCM >0_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 non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

<* the V63() Element of the U1 of SCM*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

[8,<* the 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*>] is V15() V16() set

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

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

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

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

[[8,<* the 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*>] is V15() set

{[8,<* the 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*>} is non empty set

{[8,<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *>]} is non empty V2() Relation-like Function-like constant 1 -element set

{{[8,<* the 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*>},{[8,<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *>]}} is non empty set

JumpPart ( the V63() Element of the U1 of SCM >0_goto 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 RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

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

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

<* the epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT *> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

InsCode ( the V63() Element of the U1 of SCM >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

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

i1 is set

DOM (JumpParts I) is set

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

i1 is set

j is Relation-like Function-like set

proj1 j is set

k is Element of the InstructionsF of SCM

JumpPart k is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(k) is set

AddressPart K77(k) 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

K77(K77(k)) is set

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

s2 is V63() Element of the U1 of SCM

s2 >0_goto s1 is Element of the InstructionsF of SCM

<*s1*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

<*s2*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

[8,<*s1*>,<*s2*>] is V15() V16() set

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

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

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

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

{[8,<*s1*>],<*s2*>} is non empty set

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

{{[8,<*s1*>],<*s2*>},{[8,<*s1*>]}} is non empty set

<*s1*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

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

SCM-goto I is Element of the InstructionsF of SCM

<*I*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() 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

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

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

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

InsCode (SCM-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

K77((SCM-goto I)) is set

K77(K77((SCM-goto I))) is set

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

{ (JumpPart b

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

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

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

a is set

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

k1 is Relation-like Function-like set

k1 . 1 is set

i1 is Element of the InstructionsF of SCM

JumpPart i1 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(i1) is set

AddressPart K77(i1) is set

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

K77(K77(i1)) is set

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

SCM-goto j is Element of the InstructionsF of SCM

<*j*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

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

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

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

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

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

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

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

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

<*j*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

a is set

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

SCM-goto k1 is Element of the InstructionsF of SCM

<*k1*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

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

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

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

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

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

{[6,<*k1*>],{}} is non empty set

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

{{[6,<*k1*>],{}},{[6,<*k1*>]}} is non empty set

JumpPart (SCM-goto k1) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77((SCM-goto k1)) is set

AddressPart K77((SCM-goto k1)) is set

<*k1*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

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

K77(K77((SCM-goto k1))) is set

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

I is V63() Element of the U1 of SCM

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

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

<*a*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

<*I*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

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

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

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

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

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

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

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

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

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

InsCode (I =0_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

K77((I =0_goto a)) is set

K77(K77((I =0_goto a))) is set

JumpParts (InsCode (I =0_goto a)) is non empty functional with_common_domain product-like set

{ (JumpPart b

product" (JumpParts (InsCode (I =0_goto a))) is Relation-like Function-like set

(product" (JumpParts (InsCode (I =0_goto a)))) . 1 is set

proj1 (product" (JumpParts (InsCode (I =0_goto a)))) is set

k1 is set

pi ((JumpParts (InsCode (I =0_goto a))),1) is set

i1 is Relation-like Function-like set

i1 . 1 is set

j is Element of the InstructionsF of SCM

JumpPart j is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(j) is set

AddressPart K77(j) 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

K77(K77(j)) is set

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

s1 is V63() Element of the U1 of SCM

s1 =0_goto k is Element of the InstructionsF of SCM

<*k*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

<*s1*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

[7,<*k*>,<*s1*>] is V15() V16() set

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

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

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

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

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

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

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

<*k*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

k1 is 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 Element of the InstructionsF of SCM

<*i1*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

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

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

{7,<*i1*>} is non empty 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

JumpPart (I =0_goto i1) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

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

AddressPart K77((I =0_goto i1)) is set

<*i1*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

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

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

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

I is V63() Element of the U1 of SCM

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

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

<*a*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

<*I*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

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

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

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

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

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

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

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

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

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

InsCode (I >0_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

K77((I >0_goto a)) is set

K77(K77((I >0_goto a))) is set

JumpParts (InsCode (I >0_goto a)) is non empty functional with_common_domain product-like set

{ (JumpPart b

product" (JumpParts (InsCode (I >0_goto a))) is Relation-like Function-like set

(product" (JumpParts (InsCode (I >0_goto a)))) . 1 is set

proj1 (product" (JumpParts (InsCode (I >0_goto a)))) is set

k1 is set

pi ((JumpParts (InsCode (I >0_goto a))),1) is set

i1 is Relation-like Function-like set

i1 . 1 is set

j is Element of the InstructionsF of SCM

JumpPart j is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

K77(j) is set

AddressPart K77(j) 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

K77(K77(j)) is set

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

s1 is V63() Element of the U1 of SCM

s1 >0_goto k is Element of the InstructionsF of SCM

<*k*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

<*s1*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

[8,<*k*>,<*s1*>] is V15() V16() set

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

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

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

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

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

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

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

<*k*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

k1 is 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 Element of the InstructionsF of SCM

<*i1*> is non empty V2() Relation-like NAT -defined Function-like constant V28() 1 -element FinSequence-like FinSubsequence-like countable V147() set

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

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

{8,<*i1*>} is non empty 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

JumpPart (I >0_goto i1) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V28() FinSequence-like FinSubsequence-like countable V115() V116() V117() V118() V147() set

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

AddressPart K77((I >0_goto i1)) is set

<*i1*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant V28() 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable V115() V116() V117() V118() V119() V120() V121() V122() V147() FinSequence of NAT

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

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

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

k1 is Element of the InstructionsF of SCM

JUMP k1 is countable Element of K6(NAT)

{ (NIC (k1,b

meet { (NIC (k1,b

{ (NIC (k1,b

meet { (NIC (k1,b

s1 is set

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

NIC (k1,j) is countable Element of K6(NAT)

product (the_Values_of SCM) is non empty functional with_common_domain product-like set

{ (IC (Exec (k1,b

succ j is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real non negative set

K356(j,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

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

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

NIC (k1,k) is countable Element of K6(NAT)

{ (IC (Exec (k1,b

succ k is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real non negative set

K356(k,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

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

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

{ (NIC ((halt SCM),b

meet { (NIC ((halt SCM),b

I is V63() Element of the U1 of SCM

a is V63() Element of the U1 of SCM

I := a is Element of the InstructionsF of SCM

<*I,a*> is non empty Relation-like NAT -defined Function-like V28() 2 -element FinSequence-like FinSubsequence-like countable V147() set

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

[1,{}] is V15() set

{1,{}} is non empty set

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

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

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

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

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

k1 is Relation-like the U1 of SCM -defined Function-like the_Values_of SCM -compatible total set

Exec ((I := a),k1) is Relation-like the U1 of SCM -defined Function-like the_Values_of SCM -compatible total set

product ( the Object-Kind of SCM * the ValuesF of SCM) is functional with_common_domain product-like set

K152((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))) is set

the Execution of SCM is Relation-like Function-like V40( the InstructionsF of SCM,K152((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) Element of K6(K7( the InstructionsF of SCM,K152((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))))

K7( the InstructionsF of SCM,K152((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))) is Relation-like set

K6(K7( the InstructionsF of SCM,K152((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))))) is set

K154( the InstructionsF of SCM,K152((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(I := a)) is Element of K152((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM)))

K154( the InstructionsF of SCM,K152((product ( the Object-Kind of SCM * the ValuesF of SCM)),(product ( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(I := a)) . k1 is set

(Exec ((I := a),k1)) . (IC ) is set

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

k1 . (IC ) is set

succ (IC k1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable non with_non-empty_elements ext-real non negative set

K356((IC k1),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

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

[2,{},<*I,a*>] 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,a*>] is V15() set

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

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

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

k1 is Relation-like the U1 of SCM -defined Function-like the_Values_of