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 b1) where b1 is Element of the InstructionsF of SCM : InsCode b1 = I } is set
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 b1) where b1 is Element of the InstructionsF of SCM : InsCode b1 = I } is set
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 b1) where b1 is Element of the InstructionsF of SCM : InsCode b1 = I } is set
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 b1) where b1 is Element of the InstructionsF of SCM : InsCode b1 = I } is set
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 b1) where b1 is Element of the InstructionsF of SCM : InsCode b1 = I } is set
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 b1) where b1 is Element of the InstructionsF of SCM : InsCode b1 = I } is set
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 b1) where b1 is Element of the InstructionsF of SCM : 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
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 b1) where b1 is Element of the InstructionsF of SCM : 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 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 b1) where b1 is Element of the InstructionsF of SCM : 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 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 b1) where b1 is Element of the InstructionsF of SCM : InsCode b1 = InsCode (SCM-goto I) } is set
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 b1) where b1 is Element of the InstructionsF of SCM : InsCode b1 = InsCode (I =0_goto a) } is set
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 b1) where b1 is Element of the InstructionsF of SCM : InsCode b1 = InsCode (I >0_goto a) } is set
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,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT : verum } is set
meet { (NIC (k1,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT : verum } is set
{ (NIC (k1,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT : verum } is set
meet { (NIC (k1,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT : verum } is set
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,b1))) where b1 is Relation-like the U1 of SCM -defined Function-like the_Values_of SCM -compatible total Element of product (the_Values_of SCM) : IC b1 = j } is set
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,b1))) where b1 is Relation-like the U1 of SCM -defined Function-like the_Values_of SCM -compatible total Element of product (the_Values_of SCM) : IC b1 = k } is set
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),b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT : verum } is set
meet { (NIC ((halt SCM),b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V28() cardinal countable ext-real non negative Element of NAT : verum } is set
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