REAL is non empty with_zero set
NAT is non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero Element of K32(REAL)
K32(REAL) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V24() V84() V85() with_zero set
K32(omega) is set
K32(NAT) is set
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() FinSequence-like FinSubsequence-like FinSequence-membered V81() V84() V86() integer Function-yielding V120() complex ext-real non positive non negative set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real positive non negative Element of NAT
{{},1} is non empty set
9 is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real positive non negative Element of NAT
Segm 9 is V84() Element of K32(omega)
SCM-Data-Loc is non empty set
K80(NAT,1) is non empty V84() non with_zero V90() Element of K32(NAT)
K66(NAT,REAL,K80(NAT,1),NAT) is Relation-like Element of K32(K33(NAT,REAL))
K33(NAT,REAL) is Relation-like set
K32(K33(NAT,REAL)) is set
SCM-Memory is non empty set
{NAT} is non empty non with_zero V90() set
{NAT} \/ SCM-Data-Loc is non empty set
K32(SCM-Memory) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real positive non negative Element of NAT
K33(SCM-Memory,2) is Relation-like set
K32(K33(SCM-Memory,2)) is set
SCM-OK is Relation-like Function-like V36( SCM-Memory ,2) Element of K32(K33(SCM-Memory,2))
SCM-VAL is Relation-like 2 -defined Function-like V35(2) set
INT is set
K325(NAT,INT) is set
SCM-OK * SCM-VAL is Relation-like non-empty Function-like set
K233((SCM-OK * SCM-VAL)) is non empty functional V82() V83() set
SCM-Instr is non empty Relation-like standard-ins V98() V99() V101() set
SCM-Halt is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() FinSequence-like FinSubsequence-like FinSequence-membered V81() V84() V86() integer Function-yielding V120() complex ext-real non positive non negative Element of Segm 9
[SCM-Halt,{},{}] is V1() V2() set
[SCM-Halt,{}] is V1() set
{SCM-Halt,{}} is non empty functional set
{SCM-Halt} is non empty functional V82() set
{{SCM-Halt,{}},{SCM-Halt}} is non empty non with_zero V90() set
[[SCM-Halt,{}],{}] is V1() set
{[SCM-Halt,{}],{}} is non empty set
{[SCM-Halt,{}]} is non empty Relation-like Function-like set
{{[SCM-Halt,{}],{}},{[SCM-Halt,{}]}} is non empty non with_zero V90() set
{[SCM-Halt,{},{}]} is non empty Relation-like standard-ins V98() V99() V101() set
6 is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real positive non negative Element of NAT
{ [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT : b1 = 6 } is set
{[SCM-Halt,{},{}]} \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT : b1 = 6 } is non empty set
7 is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real positive non negative Element of NAT
8 is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real positive non negative Element of NAT
K81(NAT,7,8) is non empty V84() non with_zero V90() Element of K32(NAT)
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT , b3 is Element of SCM-Data-Loc : b1 in K81(NAT,7,8) } is set
({[SCM-Halt,{},{}]} \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT , b3 is Element of SCM-Data-Loc : b1 in K81(NAT,7,8) } is non empty set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real positive non negative Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real positive non negative Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real positive non negative Element of NAT
K84(NAT,1,2,3,4,5) is V84() non with_zero Element of K32(NAT)
{ [b1,{},K129(SCM-Data-Loc,b2,b3)] where b1 is Element of Segm 9, b2, b3 is Element of SCM-Data-Loc : b1 in K84(NAT,1,2,3,4,5) } is set
(({[SCM-Halt,{},{}]} \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT , b3 is Element of SCM-Data-Loc : b1 in K81(NAT,7,8) } ) \/ { [b1,{},K129(SCM-Data-Loc,b2,b3)] where b1 is Element of Segm 9, b2, b3 is Element of SCM-Data-Loc : b1 in K84(NAT,1,2,3,4,5) } is non empty set
K145(K233((SCM-OK * SCM-VAL)),K233((SCM-OK * SCM-VAL))) is set
K33(SCM-Instr,K145(K233((SCM-OK * SCM-VAL)),K233((SCM-OK * SCM-VAL)))) is Relation-like set
K32(K33(SCM-Instr,K145(K233((SCM-OK * SCM-VAL)),K233((SCM-OK * SCM-VAL))))) is set
ExtREAL is set
COMPLEX is set
RAT is set
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() FinSequence-like FinSubsequence-like FinSequence-membered V81() V84() V86() integer Function-yielding V120() complex ext-real non positive non negative Element of NAT
(SCM-OK * SCM-VAL) . NAT is set
SCM-Data-Loc is non empty Element of K32(SCM-Memory)
SCM-Exec is Relation-like Function-like V36( SCM-Instr ,K145(K233((SCM-OK * SCM-VAL)),K233((SCM-OK * SCM-VAL)))) Element of K32(K33(SCM-Instr,K145(K233((SCM-OK * SCM-VAL)),K233((SCM-OK * SCM-VAL)))))
proj1 (SCM-OK * SCM-VAL) is set
[0,{},{}] is V1() V2() set
[0,{}] is V1() set
{0,{}} is non empty functional set
{0} is non empty functional V82() set
{{0,{}},{0}} is non empty non with_zero V90() set
[[0,{}],{}] is V1() set
{[0,{}],{}} is non empty set
{[0,{}]} is non empty Relation-like Function-like set
{{[0,{}],{}},{[0,{}]}} is non empty non with_zero V90() set
i is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
InsCodes SCM-Instr is non empty set
K23(SCM-Instr) is set
proj1 SCM-Instr is non empty set
proj1 (proj1 SCM-Instr) is set
In (NAT,SCM-Memory) is Element of SCM-Memory
AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),SCM-Instr,SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2
() is strict AMI-Struct over 2
the_Values_of () is Relation-like the carrier of () -defined Function-like V35( the carrier of ()) set
the carrier of () is set
the Object-Kind of () is Relation-like Function-like V36( the carrier of (),2) Element of K32(K33( the carrier of (),2))
K33( the carrier of (),2) is Relation-like set
K32(K33( the carrier of (),2)) is set
the ValuesF of () is Relation-like 2 -defined Function-like V35(2) set
the Object-Kind of () * the ValuesF of () is Relation-like Function-like set
IC is Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
Values (IC ) is non empty set
(the_Values_of ()) . (IC ) is set
the Element of SCM-Data-Loc is Element of SCM-Data-Loc
i is Element of the carrier of ()
i is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
lb is Int-like Element of the carrier of ()
i . lb is set
b is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
a is Element of SCM-Data-Loc
b . a is V86() integer complex ext-real set
the InstructionsF of () is non empty Relation-like standard-ins V98() V99() V101() set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[1,{},<*i,lb*>] is V1() V2() set
[1,{}] is V1() set
{1,{}} is non empty set
{1} is non empty non with_zero V90() set
{{1,{}},{1}} is non empty non with_zero V90() set
[[1,{}],<*i,lb*>] is V1() set
{[1,{}],<*i,lb*>} is non empty set
{[1,{}]} is non empty Relation-like Function-like set
{{[1,{}],<*i,lb*>},{[1,{}]}} is non empty non with_zero V90() set
{1,2,3,4,5} is non with_zero set
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[1,{},<*a,b*>] is V1() V2() set
[[1,{}],<*a,b*>] is V1() set
{[1,{}],<*a,b*>} is non empty set
{{[1,{}],<*a,b*>},{[1,{}]}} is non empty non with_zero V90() set
[2,{},<*i,lb*>] is V1() V2() set
[2,{}] is V1() set
{2,{}} is non empty set
{2} is non empty non with_zero V90() set
{{2,{}},{2}} is non empty non with_zero V90() set
[[2,{}],<*i,lb*>] is V1() set
{[2,{}],<*i,lb*>} is non empty set
{[2,{}]} is non empty Relation-like Function-like set
{{[2,{}],<*i,lb*>},{[2,{}]}} is non empty non with_zero V90() set
{1,2,3,4,5} is non with_zero set
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[2,{},<*a,b*>] is V1() V2() set
[[2,{}],<*a,b*>] is V1() set
{[2,{}],<*a,b*>} is non empty set
{{[2,{}],<*a,b*>},{[2,{}]}} is non empty non with_zero V90() set
[3,{},<*i,lb*>] is V1() V2() set
[3,{}] is V1() set
{3,{}} is non empty set
{3} is non empty non with_zero V90() set
{{3,{}},{3}} is non empty non with_zero V90() set
[[3,{}],<*i,lb*>] is V1() set
{[3,{}],<*i,lb*>} is non empty set
{[3,{}]} is non empty Relation-like Function-like set
{{[3,{}],<*i,lb*>},{[3,{}]}} is non empty non with_zero V90() set
{1,2,3,4,5} is non with_zero set
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[3,{},<*a,b*>] is V1() V2() set
[[3,{}],<*a,b*>] is V1() set
{[3,{}],<*a,b*>} is non empty set
{{[3,{}],<*a,b*>},{[3,{}]}} is non empty non with_zero V90() set
[4,{},<*i,lb*>] is V1() V2() set
[4,{}] is V1() set
{4,{}} is non empty set
{4} is non empty non with_zero V90() set
{{4,{}},{4}} is non empty non with_zero V90() set
[[4,{}],<*i,lb*>] is V1() set
{[4,{}],<*i,lb*>} is non empty set
{[4,{}]} is non empty Relation-like Function-like set
{{[4,{}],<*i,lb*>},{[4,{}]}} is non empty non with_zero V90() set
{1,2,3,4,5} is non with_zero set
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[4,{},<*a,b*>] is V1() V2() set
[[4,{}],<*a,b*>] is V1() set
{[4,{}],<*a,b*>} is non empty set
{{[4,{}],<*a,b*>},{[4,{}]}} is non empty non with_zero V90() set
[5,{},<*i,lb*>] is V1() V2() set
[5,{}] is V1() set
{5,{}} is non empty set
{5} is non empty non with_zero V90() set
{{5,{}},{5}} is non empty non with_zero V90() set
[[5,{}],<*i,lb*>] is V1() set
{[5,{}],<*i,lb*>} is non empty set
{[5,{}]} is non empty Relation-like Function-like set
{{[5,{}],<*i,lb*>},{[5,{}]}} is non empty non with_zero V90() set
{1,2,3,4,5} is non with_zero set
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[5,{},<*a,b*>] is V1() V2() set
[[5,{}],<*a,b*>] is V1() set
{[5,{}],<*a,b*>} is non empty set
{{[5,{}],<*a,b*>},{[5,{}]}} is non empty non with_zero V90() set
i is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
<*i*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[6,<*i*>,{}] is V1() V2() set
[6,<*i*>] is V1() set
{6,<*i*>} is non empty non with_zero V90() set
{6} is non empty non with_zero V90() set
{{6,<*i*>},{6}} is non empty non with_zero V90() set
[[6,<*i*>],{}] is V1() set
{[6,<*i*>],{}} is non empty set
{[6,<*i*>]} is non empty Relation-like Function-like set
{{[6,<*i*>],{}},{[6,<*i*>]}} is non empty non with_zero V90() set
lb is Int-like Element of the carrier of ()
<*lb*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[7,<*i*>,<*lb*>] is V1() V2() set
[7,<*i*>] is V1() set
{7,<*i*>} is non empty non with_zero V90() set
{7} is non empty non with_zero V90() set
{{7,<*i*>},{7}} is non empty non with_zero V90() set
[[7,<*i*>],<*lb*>] is V1() set
{[7,<*i*>],<*lb*>} is non empty set
{[7,<*i*>]} is non empty Relation-like Function-like set
{{[7,<*i*>],<*lb*>},{[7,<*i*>]}} is non empty non with_zero V90() set
{7,8} is non empty non with_zero V90() set
b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
<*b*> is non empty Relation-like NAT -defined NAT -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of NAT
a is Element of SCM-Data-Loc
<*a*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of SCM-Data-Loc
[7,<*b*>,<*a*>] is V1() V2() set
[7,<*b*>] is V1() set
{7,<*b*>} is non empty non with_zero V90() set
{{7,<*b*>},{7}} is non empty non with_zero V90() set
[[7,<*b*>],<*a*>] is V1() set
{[7,<*b*>],<*a*>} is non empty set
{[7,<*b*>]} is non empty Relation-like Function-like set
{{[7,<*b*>],<*a*>},{[7,<*b*>]}} is non empty non with_zero V90() set
[8,<*i*>,<*lb*>] is V1() V2() set
[8,<*i*>] is V1() set
{8,<*i*>} is non empty non with_zero V90() set
{8} is non empty non with_zero V90() set
{{8,<*i*>},{8}} is non empty non with_zero V90() set
[[8,<*i*>],<*lb*>] is V1() set
{[8,<*i*>],<*lb*>} is non empty set
{[8,<*i*>]} is non empty Relation-like Function-like set
{{[8,<*i*>],<*lb*>},{[8,<*i*>]}} is non empty non with_zero V90() set
{7,8} is non empty non with_zero V90() set
b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
<*b*> is non empty Relation-like NAT -defined NAT -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of NAT
a is Element of SCM-Data-Loc
<*a*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of SCM-Data-Loc
[8,<*b*>,<*a*>] is V1() V2() set
[8,<*b*>] is V1() set
{8,<*b*>} is non empty non with_zero V90() set
{{8,<*b*>},{8}} is non empty non with_zero V90() set
[[8,<*b*>],<*a*>] is V1() set
{[8,<*b*>],<*a*>} is non empty set
{[8,<*b*>]} is non empty Relation-like Function-like set
{{[8,<*b*>],<*a*>},{[8,<*b*>]}} is non empty non with_zero V90() set
IC is Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[1,{},<*i,lb*>] is V1() V2() set
[[1,{}],<*i,lb*>] is V1() set
{[1,{}],<*i,lb*>} is non empty set
{{[1,{}],<*i,lb*>},{[1,{}]}} is non empty non with_zero V90() set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec ((i,lb),a) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) . a is set
(Exec ((i,lb),a)) . (IC ) is set
IC a is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
a . (IC ) is set
succ (IC a) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC a),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
(Exec ((i,lb),a)) . i is V86() integer complex ext-real set
a . lb is V86() integer complex ext-real set
b is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
t is Element of SCM-Instr
t address_1 is Element of SCM-Data-Loc
t address_2 is Element of SCM-Data-Loc
b . (t address_2) is V86() integer complex ext-real set
SCM-Chg (b,(t address_1),(b . (t address_2))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
(t address_1) .--> (b . (t address_2)) is V5() Relation-like SCM-Data-Loc -defined {(t address_1)} -defined Function-like one-to-one constant set
{(t address_1)} is non empty set
{(t address_1)} --> (b . (t address_2)) is non empty Relation-like {(t address_1)} -defined Function-like constant V35({(t address_1)}) V36({(t address_1)},{(b . (t address_2))}) Element of K32(K33({(t address_1)},{(b . (t address_2))}))
{(b . (t address_2))} is non empty set
K33({(t address_1)},{(b . (t address_2))}) is Relation-like set
K32(K33({(t address_1)},{(b . (t address_2))})) is set
b +* ((t address_1) .--> (b . (t address_2))) is Relation-like Function-like set
w is Element of Segm 9
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[w,{},<*a,b*>] is V1() V2() set
[w,{}] is V1() set
{w,{}} is non empty set
{w} is non empty set
{{w,{}},{w}} is non empty non with_zero V90() set
[[w,{}],<*a,b*>] is V1() set
{[w,{}],<*a,b*>} is non empty set
{[w,{}]} is non empty Relation-like Function-like set
{{[w,{}],<*a,b*>},{[w,{}]}} is non empty non with_zero V90() set
SCM-Exec-Res (t,b) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
IC b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
b . NAT is set
succ (IC b) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC b),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
SCM-Chg ((SCM-Chg (b,(t address_1),(b . (t address_2)))),(succ (IC b))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
NAT .--> (succ (IC b)) is V5() Relation-like {NAT} -defined omega -valued Function-like one-to-one constant set
{NAT} --> (succ (IC b)) is non empty Relation-like non-empty {NAT} -defined omega -valued Function-like constant V35({NAT}) V36({NAT},{(succ (IC b))}) Element of K32(K33({NAT},{(succ (IC b))}))
{(succ (IC b))} is non empty non with_zero V90() set
K33({NAT},{(succ (IC b))}) is Relation-like set
K32(K33({NAT},{(succ (IC b))})) is set
(SCM-Chg (b,(t address_1),(b . (t address_2)))) +* (NAT .--> (succ (IC b))) is Relation-like Function-like set
(SCM-Chg (b,(t address_1),(b . (t address_2)))) . a is V86() integer complex ext-real set
e is Int-like Element of the carrier of ()
(Exec ((i,lb),a)) . e is V86() integer complex ext-real set
a . e is V86() integer complex ext-real set
c is Element of SCM-Data-Loc
(SCM-Chg (b,(t address_1),(b . (t address_2)))) . c is V86() integer complex ext-real set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[2,{},<*i,lb*>] is V1() V2() set
[[2,{}],<*i,lb*>] is V1() set
{[2,{}],<*i,lb*>} is non empty set
{{[2,{}],<*i,lb*>},{[2,{}]}} is non empty non with_zero V90() set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec ((i,lb),a) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) . a is set
(Exec ((i,lb),a)) . (IC ) is set
IC a is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
a . (IC ) is set
succ (IC a) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC a),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
(Exec ((i,lb),a)) . i is V86() integer complex ext-real set
a . i is V86() integer complex ext-real set
a . lb is V86() integer complex ext-real set
(a . i) + (a . lb) is V86() integer complex ext-real set
b is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
t is Element of SCM-Instr
t address_1 is Element of SCM-Data-Loc
b . (t address_1) is V86() integer complex ext-real set
t address_2 is Element of SCM-Data-Loc
b . (t address_2) is V86() integer complex ext-real set
(b . (t address_1)) + (b . (t address_2)) is V86() integer complex ext-real set
SCM-Chg (b,(t address_1),((b . (t address_1)) + (b . (t address_2)))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
(t address_1) .--> ((b . (t address_1)) + (b . (t address_2))) is V5() Relation-like SCM-Data-Loc -defined {(t address_1)} -defined Function-like one-to-one constant set
{(t address_1)} is non empty set
{(t address_1)} --> ((b . (t address_1)) + (b . (t address_2))) is non empty Relation-like {(t address_1)} -defined Function-like constant V35({(t address_1)}) V36({(t address_1)},{((b . (t address_1)) + (b . (t address_2)))}) Element of K32(K33({(t address_1)},{((b . (t address_1)) + (b . (t address_2)))}))
{((b . (t address_1)) + (b . (t address_2)))} is non empty set
K33({(t address_1)},{((b . (t address_1)) + (b . (t address_2)))}) is Relation-like set
K32(K33({(t address_1)},{((b . (t address_1)) + (b . (t address_2)))})) is set
b +* ((t address_1) .--> ((b . (t address_1)) + (b . (t address_2)))) is Relation-like Function-like set
w is Element of Segm 9
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[w,{},<*a,b*>] is V1() V2() set
[w,{}] is V1() set
{w,{}} is non empty set
{w} is non empty set
{{w,{}},{w}} is non empty non with_zero V90() set
[[w,{}],<*a,b*>] is V1() set
{[w,{}],<*a,b*>} is non empty set
{[w,{}]} is non empty Relation-like Function-like set
{{[w,{}],<*a,b*>},{[w,{}]}} is non empty non with_zero V90() set
SCM-Exec-Res (t,b) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
IC b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
b . NAT is set
succ (IC b) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC b),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
SCM-Chg ((SCM-Chg (b,(t address_1),((b . (t address_1)) + (b . (t address_2))))),(succ (IC b))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
NAT .--> (succ (IC b)) is V5() Relation-like {NAT} -defined omega -valued Function-like one-to-one constant set
{NAT} --> (succ (IC b)) is non empty Relation-like non-empty {NAT} -defined omega -valued Function-like constant V35({NAT}) V36({NAT},{(succ (IC b))}) Element of K32(K33({NAT},{(succ (IC b))}))
{(succ (IC b))} is non empty non with_zero V90() set
K33({NAT},{(succ (IC b))}) is Relation-like set
K32(K33({NAT},{(succ (IC b))})) is set
(SCM-Chg (b,(t address_1),((b . (t address_1)) + (b . (t address_2))))) +* (NAT .--> (succ (IC b))) is Relation-like Function-like set
(SCM-Chg (b,(t address_1),((b . (t address_1)) + (b . (t address_2))))) . a is V86() integer complex ext-real set
e is Int-like Element of the carrier of ()
(Exec ((i,lb),a)) . e is V86() integer complex ext-real set
a . e is V86() integer complex ext-real set
c is Element of SCM-Data-Loc
(SCM-Chg (b,(t address_1),((b . (t address_1)) + (b . (t address_2))))) . c is V86() integer complex ext-real set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[3,{},<*i,lb*>] is V1() V2() set
[[3,{}],<*i,lb*>] is V1() set
{[3,{}],<*i,lb*>} is non empty set
{{[3,{}],<*i,lb*>},{[3,{}]}} is non empty non with_zero V90() set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec ((i,lb),a) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) . a is set
(Exec ((i,lb),a)) . (IC ) is set
IC a is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
a . (IC ) is set
succ (IC a) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC a),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
(Exec ((i,lb),a)) . i is V86() integer complex ext-real set
a . i is V86() integer complex ext-real set
a . lb is V86() integer complex ext-real set
(a . i) - (a . lb) is V86() integer complex ext-real set
b is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
t is Element of SCM-Instr
t address_1 is Element of SCM-Data-Loc
b . (t address_1) is V86() integer complex ext-real set
t address_2 is Element of SCM-Data-Loc
b . (t address_2) is V86() integer complex ext-real set
(b . (t address_1)) - (b . (t address_2)) is V86() integer complex ext-real set
SCM-Chg (b,(t address_1),((b . (t address_1)) - (b . (t address_2)))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
(t address_1) .--> ((b . (t address_1)) - (b . (t address_2))) is V5() Relation-like SCM-Data-Loc -defined {(t address_1)} -defined Function-like one-to-one constant set
{(t address_1)} is non empty set
{(t address_1)} --> ((b . (t address_1)) - (b . (t address_2))) is non empty Relation-like {(t address_1)} -defined Function-like constant V35({(t address_1)}) V36({(t address_1)},{((b . (t address_1)) - (b . (t address_2)))}) Element of K32(K33({(t address_1)},{((b . (t address_1)) - (b . (t address_2)))}))
{((b . (t address_1)) - (b . (t address_2)))} is non empty set
K33({(t address_1)},{((b . (t address_1)) - (b . (t address_2)))}) is Relation-like set
K32(K33({(t address_1)},{((b . (t address_1)) - (b . (t address_2)))})) is set
b +* ((t address_1) .--> ((b . (t address_1)) - (b . (t address_2)))) is Relation-like Function-like set
w is Element of Segm 9
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[w,{},<*a,b*>] is V1() V2() set
[w,{}] is V1() set
{w,{}} is non empty set
{w} is non empty set
{{w,{}},{w}} is non empty non with_zero V90() set
[[w,{}],<*a,b*>] is V1() set
{[w,{}],<*a,b*>} is non empty set
{[w,{}]} is non empty Relation-like Function-like set
{{[w,{}],<*a,b*>},{[w,{}]}} is non empty non with_zero V90() set
SCM-Exec-Res (t,b) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
IC b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
b . NAT is set
succ (IC b) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC b),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
SCM-Chg ((SCM-Chg (b,(t address_1),((b . (t address_1)) - (b . (t address_2))))),(succ (IC b))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
NAT .--> (succ (IC b)) is V5() Relation-like {NAT} -defined omega -valued Function-like one-to-one constant set
{NAT} --> (succ (IC b)) is non empty Relation-like non-empty {NAT} -defined omega -valued Function-like constant V35({NAT}) V36({NAT},{(succ (IC b))}) Element of K32(K33({NAT},{(succ (IC b))}))
{(succ (IC b))} is non empty non with_zero V90() set
K33({NAT},{(succ (IC b))}) is Relation-like set
K32(K33({NAT},{(succ (IC b))})) is set
(SCM-Chg (b,(t address_1),((b . (t address_1)) - (b . (t address_2))))) +* (NAT .--> (succ (IC b))) is Relation-like Function-like set
(SCM-Chg (b,(t address_1),((b . (t address_1)) - (b . (t address_2))))) . a is V86() integer complex ext-real set
e is Int-like Element of the carrier of ()
(Exec ((i,lb),a)) . e is V86() integer complex ext-real set
a . e is V86() integer complex ext-real set
c is Element of SCM-Data-Loc
(SCM-Chg (b,(t address_1),((b . (t address_1)) - (b . (t address_2))))) . c is V86() integer complex ext-real set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[4,{},<*i,lb*>] is V1() V2() set
[[4,{}],<*i,lb*>] is V1() set
{[4,{}],<*i,lb*>} is non empty set
{{[4,{}],<*i,lb*>},{[4,{}]}} is non empty non with_zero V90() set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec ((i,lb),a) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) . a is set
(Exec ((i,lb),a)) . (IC ) is set
IC a is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
a . (IC ) is set
succ (IC a) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC a),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
(Exec ((i,lb),a)) . i is V86() integer complex ext-real set
a . i is V86() integer complex ext-real set
a . lb is V86() integer complex ext-real set
(a . i) * (a . lb) is V86() integer complex ext-real set
b is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
t is Element of SCM-Instr
t address_1 is Element of SCM-Data-Loc
b . (t address_1) is V86() integer complex ext-real set
t address_2 is Element of SCM-Data-Loc
b . (t address_2) is V86() integer complex ext-real set
(b . (t address_1)) * (b . (t address_2)) is V86() integer complex ext-real set
SCM-Chg (b,(t address_1),((b . (t address_1)) * (b . (t address_2)))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
(t address_1) .--> ((b . (t address_1)) * (b . (t address_2))) is V5() Relation-like SCM-Data-Loc -defined {(t address_1)} -defined Function-like one-to-one constant set
{(t address_1)} is non empty set
{(t address_1)} --> ((b . (t address_1)) * (b . (t address_2))) is non empty Relation-like {(t address_1)} -defined Function-like constant V35({(t address_1)}) V36({(t address_1)},{((b . (t address_1)) * (b . (t address_2)))}) Element of K32(K33({(t address_1)},{((b . (t address_1)) * (b . (t address_2)))}))
{((b . (t address_1)) * (b . (t address_2)))} is non empty set
K33({(t address_1)},{((b . (t address_1)) * (b . (t address_2)))}) is Relation-like set
K32(K33({(t address_1)},{((b . (t address_1)) * (b . (t address_2)))})) is set
b +* ((t address_1) .--> ((b . (t address_1)) * (b . (t address_2)))) is Relation-like Function-like set
w is Element of Segm 9
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[w,{},<*a,b*>] is V1() V2() set
[w,{}] is V1() set
{w,{}} is non empty set
{w} is non empty set
{{w,{}},{w}} is non empty non with_zero V90() set
[[w,{}],<*a,b*>] is V1() set
{[w,{}],<*a,b*>} is non empty set
{[w,{}]} is non empty Relation-like Function-like set
{{[w,{}],<*a,b*>},{[w,{}]}} is non empty non with_zero V90() set
SCM-Exec-Res (t,b) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
IC b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
b . NAT is set
succ (IC b) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC b),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
SCM-Chg ((SCM-Chg (b,(t address_1),((b . (t address_1)) * (b . (t address_2))))),(succ (IC b))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
NAT .--> (succ (IC b)) is V5() Relation-like {NAT} -defined omega -valued Function-like one-to-one constant set
{NAT} --> (succ (IC b)) is non empty Relation-like non-empty {NAT} -defined omega -valued Function-like constant V35({NAT}) V36({NAT},{(succ (IC b))}) Element of K32(K33({NAT},{(succ (IC b))}))
{(succ (IC b))} is non empty non with_zero V90() set
K33({NAT},{(succ (IC b))}) is Relation-like set
K32(K33({NAT},{(succ (IC b))})) is set
(SCM-Chg (b,(t address_1),((b . (t address_1)) * (b . (t address_2))))) +* (NAT .--> (succ (IC b))) is Relation-like Function-like set
(SCM-Chg (b,(t address_1),((b . (t address_1)) * (b . (t address_2))))) . a is V86() integer complex ext-real set
e is Int-like Element of the carrier of ()
(Exec ((i,lb),a)) . e is V86() integer complex ext-real set
a . e is V86() integer complex ext-real set
c is Element of SCM-Data-Loc
(SCM-Chg (b,(t address_1),((b . (t address_1)) * (b . (t address_2))))) . c is V86() integer complex ext-real set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[5,{},<*i,lb*>] is V1() V2() set
[[5,{}],<*i,lb*>] is V1() set
{[5,{}],<*i,lb*>} is non empty set
{{[5,{}],<*i,lb*>},{[5,{}]}} is non empty non with_zero V90() set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec ((i,lb),a) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) . a is set
(Exec ((i,lb),a)) . (IC ) is set
IC a is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
a . (IC ) is set
succ (IC a) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC a),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
(Exec ((i,lb),a)) . i is V86() integer complex ext-real set
a . i is V86() integer complex ext-real set
a . lb is V86() integer complex ext-real set
(a . i) div (a . lb) is V86() integer complex ext-real set
(Exec ((i,lb),a)) . lb is V86() integer complex ext-real set
(a . i) mod (a . lb) is V86() integer complex ext-real set
b is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
t is Element of SCM-Instr
t address_1 is Element of SCM-Data-Loc
b . (t address_1) is V86() integer complex ext-real set
t address_2 is Element of SCM-Data-Loc
b . (t address_2) is V86() integer complex ext-real set
(b . (t address_1)) div (b . (t address_2)) is V86() integer complex ext-real set
SCM-Chg (b,(t address_1),((b . (t address_1)) div (b . (t address_2)))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
(t address_1) .--> ((b . (t address_1)) div (b . (t address_2))) is V5() Relation-like SCM-Data-Loc -defined {(t address_1)} -defined Function-like one-to-one constant set
{(t address_1)} is non empty set
{(t address_1)} --> ((b . (t address_1)) div (b . (t address_2))) is non empty Relation-like {(t address_1)} -defined Function-like constant V35({(t address_1)}) V36({(t address_1)},{((b . (t address_1)) div (b . (t address_2)))}) Element of K32(K33({(t address_1)},{((b . (t address_1)) div (b . (t address_2)))}))
{((b . (t address_1)) div (b . (t address_2)))} is non empty set
K33({(t address_1)},{((b . (t address_1)) div (b . (t address_2)))}) is Relation-like set
K32(K33({(t address_1)},{((b . (t address_1)) div (b . (t address_2)))})) is set
b +* ((t address_1) .--> ((b . (t address_1)) div (b . (t address_2)))) is Relation-like Function-like set
(b . (t address_1)) mod (b . (t address_2)) is V86() integer complex ext-real set
SCM-Chg ((SCM-Chg (b,(t address_1),((b . (t address_1)) div (b . (t address_2))))),(t address_2),((b . (t address_1)) mod (b . (t address_2)))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
(t address_2) .--> ((b . (t address_1)) mod (b . (t address_2))) is V5() Relation-like SCM-Data-Loc -defined {(t address_2)} -defined Function-like one-to-one constant set
{(t address_2)} is non empty set
{(t address_2)} --> ((b . (t address_1)) mod (b . (t address_2))) is non empty Relation-like {(t address_2)} -defined Function-like constant V35({(t address_2)}) V36({(t address_2)},{((b . (t address_1)) mod (b . (t address_2)))}) Element of K32(K33({(t address_2)},{((b . (t address_1)) mod (b . (t address_2)))}))
{((b . (t address_1)) mod (b . (t address_2)))} is non empty set
K33({(t address_2)},{((b . (t address_1)) mod (b . (t address_2)))}) is Relation-like set
K32(K33({(t address_2)},{((b . (t address_1)) mod (b . (t address_2)))})) is set
(SCM-Chg (b,(t address_1),((b . (t address_1)) div (b . (t address_2))))) +* ((t address_2) .--> ((b . (t address_1)) mod (b . (t address_2)))) is Relation-like Function-like set
e is Element of Segm 9
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[e,{},<*a,b*>] is V1() V2() set
[e,{}] is V1() set
{e,{}} is non empty set
{e} is non empty set
{{e,{}},{e}} is non empty non with_zero V90() set
[[e,{}],<*a,b*>] is V1() set
{[e,{}],<*a,b*>} is non empty set
{[e,{}]} is non empty Relation-like Function-like set
{{[e,{}],<*a,b*>},{[e,{}]}} is non empty non with_zero V90() set
SCM-Exec-Res (t,b) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
IC b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
b . NAT is set
succ (IC b) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC b),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
SCM-Chg ((SCM-Chg ((SCM-Chg (b,(t address_1),((b . (t address_1)) div (b . (t address_2))))),(t address_2),((b . (t address_1)) mod (b . (t address_2))))),(succ (IC b))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
NAT .--> (succ (IC b)) is V5() Relation-like {NAT} -defined omega -valued Function-like one-to-one constant set
{NAT} --> (succ (IC b)) is non empty Relation-like non-empty {NAT} -defined omega -valued Function-like constant V35({NAT}) V36({NAT},{(succ (IC b))}) Element of K32(K33({NAT},{(succ (IC b))}))
{(succ (IC b))} is non empty non with_zero V90() set
K33({NAT},{(succ (IC b))}) is Relation-like set
K32(K33({NAT},{(succ (IC b))})) is set
(SCM-Chg ((SCM-Chg (b,(t address_1),((b . (t address_1)) div (b . (t address_2))))),(t address_2),((b . (t address_1)) mod (b . (t address_2))))) +* (NAT .--> (succ (IC b))) is Relation-like Function-like set
(SCM-Chg ((SCM-Chg (b,(t address_1),((b . (t address_1)) div (b . (t address_2))))),(t address_2),((b . (t address_1)) mod (b . (t address_2))))) . a is V86() integer complex ext-real set
(SCM-Chg (b,(t address_1),((b . (t address_1)) div (b . (t address_2))))) . a is V86() integer complex ext-real set
(SCM-Chg ((SCM-Chg (b,(t address_1),((b . (t address_1)) div (b . (t address_2))))),(t address_2),((b . (t address_1)) mod (b . (t address_2))))) . b is V86() integer complex ext-real set
c is Int-like Element of the carrier of ()
(Exec ((i,lb),a)) . c is V86() integer complex ext-real set
a . c is V86() integer complex ext-real set
mn is Element of SCM-Data-Loc
(SCM-Chg ((SCM-Chg (b,(t address_1),((b . (t address_1)) div (b . (t address_2))))),(t address_2),((b . (t address_1)) mod (b . (t address_2))))) . mn is V86() integer complex ext-real set
(SCM-Chg (b,(t address_1),((b . (t address_1)) div (b . (t address_2))))) . mn is V86() integer complex ext-real set
i is Int-like Element of the carrier of ()
lb is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(lb) is Element of the InstructionsF of ()
<*lb*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[6,<*lb*>,{}] is V1() V2() set
[6,<*lb*>] is V1() set
{6,<*lb*>} is non empty non with_zero V90() set
{{6,<*lb*>},{6}} is non empty non with_zero V90() set
[[6,<*lb*>],{}] is V1() set
{[6,<*lb*>],{}} is non empty set
{[6,<*lb*>]} is non empty Relation-like Function-like set
{{[6,<*lb*>],{}},{[6,<*lb*>]}} is non empty non with_zero V90() set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec ((lb),a) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(lb)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(lb)) . a is set
(Exec ((lb),a)) . (IC ) is set
(Exec ((lb),a)) . i is V86() integer complex ext-real set
a . i is V86() integer complex ext-real set
b is Element of SCM-Instr
t is Element of Segm 9
a is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
<*a*> is non empty Relation-like NAT -defined NAT -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of NAT
[t,<*a*>,{}] is V1() V2() set
[t,<*a*>] is V1() set
{t,<*a*>} is non empty set
{t} is non empty set
{{t,<*a*>},{t}} is non empty non with_zero V90() set
[[t,<*a*>],{}] is V1() set
{[t,<*a*>],{}} is non empty set
{[t,<*a*>]} is non empty Relation-like Function-like set
{{[t,<*a*>],{}},{[t,<*a*>]}} is non empty non with_zero V90() set
t is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
SCM-Exec-Res (b,t) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
b jump_address is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
SCM-Chg (t,(b jump_address)) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
NAT .--> (b jump_address) is V5() Relation-like {NAT} -defined NAT -valued Function-like one-to-one constant set
{NAT} --> (b jump_address) is non empty Relation-like {NAT} -defined NAT -valued Function-like constant V35({NAT}) V36({NAT},{(b jump_address)}) Element of K32(K33({NAT},{(b jump_address)}))
{(b jump_address)} is non empty set
K33({NAT},{(b jump_address)}) is Relation-like set
K32(K33({NAT},{(b jump_address)})) is set
t +* (NAT .--> (b jump_address)) is Relation-like Function-like set
b is Element of SCM-Data-Loc
t . b is V86() integer complex ext-real set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
a is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(a,i) is Element of the InstructionsF of ()
<*a*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*i*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[7,<*a*>,<*i*>] is V1() V2() set
[7,<*a*>] is V1() set
{7,<*a*>} is non empty non with_zero V90() set
{{7,<*a*>},{7}} is non empty non with_zero V90() set
[[7,<*a*>],<*i*>] is V1() set
{[7,<*a*>],<*i*>} is non empty set
{[7,<*a*>]} is non empty Relation-like Function-like set
{{[7,<*a*>],<*i*>},{[7,<*a*>]}} is non empty non with_zero V90() set
b is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
b . i is V86() integer complex ext-real set
Exec ((a,i),b) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(a,i)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(a,i)) . b is set
(Exec ((a,i),b)) . (IC ) is set
IC b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
b . (IC ) is set
succ (IC b) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC b),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
(Exec ((a,i),b)) . lb is V86() integer complex ext-real set
b . lb is V86() integer complex ext-real set
b is Element of SCM-Instr
t is Element of Segm 9
e is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
<*e*> is non empty Relation-like NAT -defined NAT -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of NAT
w is Element of SCM-Data-Loc
<*w*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of SCM-Data-Loc
[t,<*e*>,<*w*>] is V1() V2() set
[t,<*e*>] is V1() set
{t,<*e*>} is non empty set
{t} is non empty set
{{t,<*e*>},{t}} is non empty non with_zero V90() set
[[t,<*e*>],<*w*>] is V1() set
{[t,<*e*>],<*w*>} is non empty set
{[t,<*e*>]} is non empty Relation-like Function-like set
{{[t,<*e*>],<*w*>},{[t,<*e*>]}} is non empty non with_zero V90() set
t is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
SCM-Exec-Res (b,t) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
b cond_address is Element of SCM-Data-Loc
t . (b cond_address) is V86() integer complex ext-real set
b cjump_address is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
IC t is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
t . NAT is set
succ (IC t) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC t),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
IFEQ ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of omega
SCM-Chg (t,(IFEQ ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
NAT .--> (IFEQ ((t . (b cond_address)),0,(b cjump_address),(succ (IC t)))) is V5() Relation-like {NAT} -defined omega -valued Function-like one-to-one constant set
{NAT} --> (IFEQ ((t . (b cond_address)),0,(b cjump_address),(succ (IC t)))) is non empty Relation-like {NAT} -defined omega -valued Function-like constant V35({NAT}) V36({NAT},{(IFEQ ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))}) Element of K32(K33({NAT},{(IFEQ ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))}))
{(IFEQ ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))} is non empty set
K33({NAT},{(IFEQ ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))}) is Relation-like set
K32(K33({NAT},{(IFEQ ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))})) is set
t +* (NAT .--> (IFEQ ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))) is Relation-like Function-like set
a is Element of SCM-Data-Loc
t . a is V86() integer complex ext-real set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
a is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(a,i) is Element of the InstructionsF of ()
<*a*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*i*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[8,<*a*>,<*i*>] is V1() V2() set
[8,<*a*>] is V1() set
{8,<*a*>} is non empty non with_zero V90() set
{{8,<*a*>},{8}} is non empty non with_zero V90() set
[[8,<*a*>],<*i*>] is V1() set
{[8,<*a*>],<*i*>} is non empty set
{[8,<*a*>]} is non empty Relation-like Function-like set
{{[8,<*a*>],<*i*>},{[8,<*a*>]}} is non empty non with_zero V90() set
b is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
b . i is V86() integer complex ext-real set
Exec ((a,i),b) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(a,i)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(a,i)) . b is set
(Exec ((a,i),b)) . (IC ) is set
IC b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
b . (IC ) is set
succ (IC b) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC b),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
(Exec ((a,i),b)) . lb is V86() integer complex ext-real set
b . lb is V86() integer complex ext-real set
b is Element of SCM-Instr
t is Element of Segm 9
e is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
<*e*> is non empty Relation-like NAT -defined NAT -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of NAT
w is Element of SCM-Data-Loc
<*w*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of SCM-Data-Loc
[t,<*e*>,<*w*>] is V1() V2() set
[t,<*e*>] is V1() set
{t,<*e*>} is non empty set
{t} is non empty set
{{t,<*e*>},{t}} is non empty non with_zero V90() set
[[t,<*e*>],<*w*>] is V1() set
{[t,<*e*>],<*w*>} is non empty set
{[t,<*e*>]} is non empty Relation-like Function-like set
{{[t,<*e*>],<*w*>},{[t,<*e*>]}} is non empty non with_zero V90() set
t is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
SCM-Exec-Res (b,t) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
b cond_address is Element of SCM-Data-Loc
t . (b cond_address) is V86() integer complex ext-real set
b cjump_address is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
IC t is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
t . NAT is set
succ (IC t) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC t),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
IFGT ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
SCM-Chg (t,(IFGT ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
NAT .--> (IFGT ((t . (b cond_address)),0,(b cjump_address),(succ (IC t)))) is V5() Relation-like {NAT} -defined Function-like one-to-one constant set
{NAT} --> (IFGT ((t . (b cond_address)),0,(b cjump_address),(succ (IC t)))) is non empty Relation-like {NAT} -defined Function-like constant V35({NAT}) V36({NAT},{(IFGT ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))}) Element of K32(K33({NAT},{(IFGT ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))}))
{(IFGT ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))} is non empty set
K33({NAT},{(IFGT ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))}) is Relation-like set
K32(K33({NAT},{(IFGT ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))})) is set
t +* (NAT .--> (IFGT ((t . (b cond_address)),0,(b cjump_address),(succ (IC t))))) is Relation-like Function-like set
a is Element of SCM-Data-Loc
t . a is V86() integer complex ext-real set
i is Element of the InstructionsF of ()
lb is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec (i,lb) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),i) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),i) . lb is set
(Exec (i,lb)) . (IC ) is set
IC lb is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
lb . (IC ) is set
succ (IC lb) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC lb),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
lb . NAT is set
i is Element of the InstructionsF of ()
i `3_3 is Relation-like NAT -defined Function-like V24() FinSequence-like FinSubsequence-like V84() set
lb is Element of SCM-Data-Loc
a is Element of SCM-Data-Loc
<*lb,a*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[1,{},<*lb,a*>] is V1() V2() set
[[1,{}],<*lb,a*>] is V1() set
{[1,{}],<*lb,a*>} is non empty set
{{[1,{}],<*lb,a*>},{[1,{}]}} is non empty non with_zero V90() set
b is Element of SCM-Data-Loc
a is Element of SCM-Data-Loc
<*b,a*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[2,{},<*b,a*>] is V1() V2() set
[[2,{}],<*b,a*>] is V1() set
{[2,{}],<*b,a*>} is non empty set
{{[2,{}],<*b,a*>},{[2,{}]}} is non empty non with_zero V90() set
lb is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
<*lb*> is non empty Relation-like NAT -defined NAT -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of NAT
a is Element of SCM-Data-Loc
<*a*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of SCM-Data-Loc
[7,<*lb*>,<*a*>] is V1() V2() set
[7,<*lb*>] is V1() set
{7,<*lb*>} is non empty non with_zero V90() set
{{7,<*lb*>},{7}} is non empty non with_zero V90() set
[[7,<*lb*>],<*a*>] is V1() set
{[7,<*lb*>],<*a*>} is non empty set
{[7,<*lb*>]} is non empty Relation-like Function-like set
{{[7,<*lb*>],<*a*>},{[7,<*lb*>]}} is non empty non with_zero V90() set
b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
<*b*> is non empty Relation-like NAT -defined NAT -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of NAT
a is Element of SCM-Data-Loc
<*a*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of SCM-Data-Loc
[8,<*b*>,<*a*>] is V1() V2() set
[8,<*b*>] is V1() set
{8,<*b*>} is non empty non with_zero V90() set
{{8,<*b*>},{8}} is non empty non with_zero V90() set
[[8,<*b*>],<*a*>] is V1() set
{[8,<*b*>],<*a*>} is non empty set
{[8,<*b*>]} is non empty Relation-like Function-like set
{{[8,<*b*>],<*a*>},{[8,<*b*>]}} is non empty non with_zero V90() set
i `2_3 is Relation-like NAT -defined NAT -valued Function-like V24() FinSequence-like FinSubsequence-like V84() V136() set
K13(i) is set
K13(i) `3_3 is set
lb is Element of SCM-Data-Loc
a is Element of SCM-Data-Loc
<*lb,a*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[5,{},<*lb,a*>] is V1() V2() set
[[5,{}],<*lb,a*>] is V1() set
{[5,{}],<*lb,a*>} is non empty set
{{[5,{}],<*lb,a*>},{[5,{}]}} is non empty non with_zero V90() set
b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
<*b*> is non empty Relation-like NAT -defined NAT -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of NAT
[6,<*b*>,{}] is V1() V2() set
[6,<*b*>] is V1() set
{6,<*b*>} is non empty non with_zero V90() set
{{6,<*b*>},{6}} is non empty non with_zero V90() set
[[6,<*b*>],{}] is V1() set
{[6,<*b*>],{}} is non empty set
{[6,<*b*>]} is non empty Relation-like Function-like set
{{[6,<*b*>],{}},{[6,<*b*>]}} is non empty non with_zero V90() set
a is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec (i,a) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),i) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),i) . a is set
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[3,{},<*a,b*>] is V1() V2() set
[[3,{}],<*a,b*>] is V1() set
{[3,{}],<*a,b*>} is non empty set
{{[3,{}],<*a,b*>},{[3,{}]}} is non empty non with_zero V90() set
t is Element of SCM-Data-Loc
t is Element of SCM-Data-Loc
<*t,t*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[4,{},<*t,t*>] is V1() V2() set
[[4,{}],<*t,t*>] is V1() set
{[4,{}],<*t,t*>} is non empty set
{{[4,{}],<*t,t*>},{[4,{}]}} is non empty non with_zero V90() set
lb is Element of SCM-Instr
b is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
SCM-Exec-Res (lb,b) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[1,{},<*i,lb*>] is V1() V2() set
[[1,{}],<*i,lb*>] is V1() set
{[1,{}],<*i,lb*>} is non empty set
{{[1,{}],<*i,lb*>},{[1,{}]}} is non empty non with_zero V90() set
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec ((i,lb), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is set
(Exec ((i,lb), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[2,{},<*i,lb*>] is V1() V2() set
[[2,{}],<*i,lb*>] is V1() set
{[2,{}],<*i,lb*>} is non empty set
{{[2,{}],<*i,lb*>},{[2,{}]}} is non empty non with_zero V90() set
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec ((i,lb), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is set
(Exec ((i,lb), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[3,{},<*i,lb*>] is V1() V2() set
[[3,{}],<*i,lb*>] is V1() set
{[3,{}],<*i,lb*>} is non empty set
{{[3,{}],<*i,lb*>},{[3,{}]}} is non empty non with_zero V90() set
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec ((i,lb), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is set
(Exec ((i,lb), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[4,{},<*i,lb*>] is V1() V2() set
[[4,{}],<*i,lb*>] is V1() set
{[4,{}],<*i,lb*>} is non empty set
{{[4,{}],<*i,lb*>},{[4,{}]}} is non empty non with_zero V90() set
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec ((i,lb), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is set
(Exec ((i,lb), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[5,{},<*i,lb*>] is V1() V2() set
[[5,{}],<*i,lb*>] is V1() set
{[5,{}],<*i,lb*>} is non empty set
{{[5,{}],<*i,lb*>},{[5,{}]}} is non empty non with_zero V90() set
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec ((i,lb), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i,lb)) . the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is set
(Exec ((i,lb), the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set )) . (IC ) is set
IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set . (IC ) is set
succ (IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC the Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set ),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(i) is Element of the InstructionsF of ()
<*i*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[6,<*i*>,{}] is V1() V2() set
[6,<*i*>] is V1() set
{6,<*i*>} is non empty non with_zero V90() set
{{6,<*i*>},{6}} is non empty non with_zero V90() set
[[6,<*i*>],{}] is V1() set
{[6,<*i*>],{}} is non empty set
{[6,<*i*>]} is non empty Relation-like Function-like set
{{[6,<*i*>],{}},{[6,<*i*>]}} is non empty non with_zero V90() set
the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
succ b is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417(b,1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
NAT .--> (succ b) is V5() Relation-like {NAT} -defined omega -valued Function-like one-to-one constant set
{NAT} --> (succ b) is non empty Relation-like non-empty {NAT} -defined omega -valued Function-like constant V35({NAT}) V36({NAT},{(succ b)}) Element of K32(K33({NAT},{(succ b)}))
{(succ b)} is non empty non with_zero V90() set
K33({NAT},{(succ b)}) is Relation-like set
K32(K33({NAT},{(succ b)})) is set
the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b)) is Relation-like Function-like set
proj1 the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) is set
proj1 (NAT .--> (succ b)) is V5() set
( the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b))) . NAT is set
(NAT .--> (succ b)) . NAT is set
proj1 (the_Values_of ()) is set
t is set
( the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b))) . t is set
(the_Values_of ()) . t is set
the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) . t is set
proj1 ( the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b))) is set
(proj1 the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))) \/ (proj1 (NAT .--> (succ b))) is set
SCM-Memory \/ (proj1 (NAT .--> (succ b))) is non empty set
SCM-Memory \/ {NAT} is non empty set
t is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
NAT .--> i is V5() Relation-like {NAT} -defined Function-like one-to-one constant set
{NAT} --> i is non empty Relation-like {NAT} -defined Function-like constant V35({NAT}) V36({NAT},{i}) Element of K32(K33({NAT},{i}))
{i} is non empty set
K33({NAT},{i}) is Relation-like set
K32(K33({NAT},{i})) is set
proj1 (NAT .--> i) is V5() set
t is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
t +* (NAT .--> i) is Relation-like Function-like set
(t +* (NAT .--> i)) . NAT is set
(NAT .--> i) . NAT is set
a is Element of SCM-Instr
a jump_address is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
SCM-Chg (t,(a jump_address)) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
NAT .--> (a jump_address) is V5() Relation-like {NAT} -defined NAT -valued Function-like one-to-one constant set
{NAT} --> (a jump_address) is non empty Relation-like {NAT} -defined NAT -valued Function-like constant V35({NAT}) V36({NAT},{(a jump_address)}) Element of K32(K33({NAT},{(a jump_address)}))
{(a jump_address)} is non empty set
K33({NAT},{(a jump_address)}) is Relation-like set
K32(K33({NAT},{(a jump_address)})) is set
t +* (NAT .--> (a jump_address)) is Relation-like Function-like set
SCM-Exec-Res (a,t) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
Exec ((i),t) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(i)) . t is set
i is Int-like Element of the carrier of ()
lb is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(lb,i) is Element of the InstructionsF of ()
<*lb*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*i*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[7,<*lb*>,<*i*>] is V1() V2() set
[7,<*lb*>] is V1() set
{7,<*lb*>} is non empty non with_zero V90() set
{{7,<*lb*>},{7}} is non empty non with_zero V90() set
[[7,<*lb*>],<*i*>] is V1() set
{[7,<*lb*>],<*i*>} is non empty set
{[7,<*lb*>]} is non empty Relation-like Function-like set
{{[7,<*lb*>],<*i*>},{[7,<*lb*>]}} is non empty non with_zero V90() set
the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
succ b is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417(b,1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
NAT .--> (succ b) is V5() Relation-like {NAT} -defined omega -valued Function-like one-to-one constant set
{NAT} --> (succ b) is non empty Relation-like non-empty {NAT} -defined omega -valued Function-like constant V35({NAT}) V36({NAT},{(succ b)}) Element of K32(K33({NAT},{(succ b)}))
{(succ b)} is non empty non with_zero V90() set
K33({NAT},{(succ b)}) is Relation-like set
K32(K33({NAT},{(succ b)})) is set
the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b)) is Relation-like Function-like set
proj1 the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) is set
proj1 ( the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b))) is set
proj1 (NAT .--> (succ b)) is V5() set
(proj1 the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))) \/ (proj1 (NAT .--> (succ b))) is set
SCM-Memory \/ (proj1 (NAT .--> (succ b))) is non empty set
SCM-Memory \/ {NAT} is non empty set
( the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b))) . NAT is set
(NAT .--> (succ b)) . NAT is set
proj1 (the_Values_of ()) is set
t is set
( the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b))) . t is set
(the_Values_of ()) . t is set
the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) . t is set
t is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
NAT .--> lb is V5() Relation-like {NAT} -defined Function-like one-to-one constant set
{NAT} --> lb is non empty Relation-like {NAT} -defined Function-like constant V35({NAT}) V36({NAT},{lb}) Element of K32(K33({NAT},{lb}))
{lb} is non empty set
K33({NAT},{lb}) is Relation-like set
K32(K33({NAT},{lb})) is set
proj1 (NAT .--> lb) is V5() set
w is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
w +* (NAT .--> lb) is Relation-like Function-like set
(w +* (NAT .--> lb)) . NAT is set
(NAT .--> lb) . NAT is set
a is Element of SCM-Instr
a cond_address is Element of SCM-Data-Loc
w . (a cond_address) is V86() integer complex ext-real set
IC w is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
w . NAT is set
IC t is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
t . (IC ) is set
t . i is V86() integer complex ext-real set
Exec ((lb,i),t) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(lb,i)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(lb,i)) . t is set
(Exec ((lb,i),t)) . (IC ) is set
e is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
succ e is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417(e,1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
a is Element of SCM-Instr
a cond_address is Element of SCM-Data-Loc
w . (a cond_address) is V86() integer complex ext-real set
a cjump_address is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
IC w is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
w . NAT is set
succ (IC w) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC w),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
IFEQ ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of omega
SCM-Chg (w,(IFEQ ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
NAT .--> (IFEQ ((w . (a cond_address)),0,(a cjump_address),(succ (IC w)))) is V5() Relation-like {NAT} -defined omega -valued Function-like one-to-one constant set
{NAT} --> (IFEQ ((w . (a cond_address)),0,(a cjump_address),(succ (IC w)))) is non empty Relation-like {NAT} -defined omega -valued Function-like constant V35({NAT}) V36({NAT},{(IFEQ ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))}) Element of K32(K33({NAT},{(IFEQ ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))}))
{(IFEQ ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))} is non empty set
K33({NAT},{(IFEQ ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))}) is Relation-like set
K32(K33({NAT},{(IFEQ ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))})) is set
w +* (NAT .--> (IFEQ ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))) is Relation-like Function-like set
SCM-Exec-Res (a,w) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
Exec ((lb,i),t) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(lb,i)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(lb,i)) . t is set
a is Element of SCM-Instr
a cond_address is Element of SCM-Data-Loc
w . (a cond_address) is V86() integer complex ext-real set
i is Int-like Element of the carrier of ()
lb is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(lb,i) is Element of the InstructionsF of ()
<*lb*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*i*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[8,<*lb*>,<*i*>] is V1() V2() set
[8,<*lb*>] is V1() set
{8,<*lb*>} is non empty non with_zero V90() set
{{8,<*lb*>},{8}} is non empty non with_zero V90() set
[[8,<*lb*>],<*i*>] is V1() set
{[8,<*lb*>],<*i*>} is non empty set
{[8,<*lb*>]} is non empty Relation-like Function-like set
{{[8,<*lb*>],<*i*>},{[8,<*lb*>]}} is non empty non with_zero V90() set
the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
succ b is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417(b,1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
NAT .--> (succ b) is V5() Relation-like {NAT} -defined omega -valued Function-like one-to-one constant set
{NAT} --> (succ b) is non empty Relation-like non-empty {NAT} -defined omega -valued Function-like constant V35({NAT}) V36({NAT},{(succ b)}) Element of K32(K33({NAT},{(succ b)}))
{(succ b)} is non empty non with_zero V90() set
K33({NAT},{(succ b)}) is Relation-like set
K32(K33({NAT},{(succ b)})) is set
the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b)) is Relation-like Function-like set
proj1 the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) is set
proj1 ( the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b))) is set
proj1 (NAT .--> (succ b)) is V5() set
(proj1 the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))) \/ (proj1 (NAT .--> (succ b))) is set
SCM-Memory \/ (proj1 (NAT .--> (succ b))) is non empty set
SCM-Memory \/ {NAT} is non empty set
( the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b))) . NAT is set
(NAT .--> (succ b)) . NAT is set
proj1 (the_Values_of ()) is set
t is set
( the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) +* (NAT .--> (succ b))) . t is set
(the_Values_of ()) . t is set
the Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL)) . t is set
t is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
NAT .--> lb is V5() Relation-like {NAT} -defined Function-like one-to-one constant set
{NAT} --> lb is non empty Relation-like {NAT} -defined Function-like constant V35({NAT}) V36({NAT},{lb}) Element of K32(K33({NAT},{lb}))
{lb} is non empty set
K33({NAT},{lb}) is Relation-like set
K32(K33({NAT},{lb})) is set
proj1 (NAT .--> lb) is V5() set
w is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
w +* (NAT .--> lb) is Relation-like Function-like set
(w +* (NAT .--> lb)) . NAT is set
(NAT .--> lb) . NAT is set
a is Element of SCM-Instr
a cond_address is Element of SCM-Data-Loc
w . (a cond_address) is V86() integer complex ext-real set
IC w is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
w . NAT is set
IC t is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
t . (IC ) is set
t . i is V86() integer complex ext-real set
Exec ((lb,i),t) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(lb,i)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(lb,i)) . t is set
(Exec ((lb,i),t)) . (IC ) is set
e is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
succ e is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417(e,1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
a is Element of SCM-Instr
a cond_address is Element of SCM-Data-Loc
w . (a cond_address) is V86() integer complex ext-real set
a cjump_address is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
IC w is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
w . NAT is set
succ (IC w) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC w),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
IFGT ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
SCM-Chg (w,(IFGT ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
NAT .--> (IFGT ((w . (a cond_address)),0,(a cjump_address),(succ (IC w)))) is V5() Relation-like {NAT} -defined Function-like one-to-one constant set
{NAT} --> (IFGT ((w . (a cond_address)),0,(a cjump_address),(succ (IC w)))) is non empty Relation-like {NAT} -defined Function-like constant V35({NAT}) V36({NAT},{(IFGT ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))}) Element of K32(K33({NAT},{(IFGT ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))}))
{(IFGT ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))} is non empty set
K33({NAT},{(IFGT ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))}) is Relation-like set
K32(K33({NAT},{(IFGT ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))})) is set
w +* (NAT .--> (IFGT ((w . (a cond_address)),0,(a cjump_address),(succ (IC w))))) is Relation-like Function-like set
SCM-Exec-Res (a,w) is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
Exec ((lb,i),t) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(lb,i)) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),(lb,i)) . t is set
a is Element of SCM-Instr
a cond_address is Element of SCM-Data-Loc
w . (a cond_address) is V86() integer complex ext-real set
i is set
{ [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT : b1 = 6 } is set
{[SCM-Halt,{},{}]} \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT : b1 = 6 } is non empty set
{7,8} is non empty non with_zero V90() set
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT , b3 is Element of SCM-Data-Loc : b1 in {7,8} } is set
({[SCM-Halt,{},{}]} \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT , b3 is Element of SCM-Data-Loc : b1 in {7,8} } is non empty set
{1,2,3,4,5} is non with_zero set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 9, b2, b3 is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } is set
lb is Element of Segm 9
a is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
<*a*> is non empty Relation-like NAT -defined NAT -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of NAT
[lb,<*a*>,{}] is V1() V2() set
[lb,<*a*>] is V1() set
{lb,<*a*>} is non empty set
{lb} is non empty set
{{lb,<*a*>},{lb}} is non empty non with_zero V90() set
[[lb,<*a*>],{}] is V1() set
{[lb,<*a*>],{}} is non empty set
{[lb,<*a*>]} is non empty Relation-like Function-like set
{{[lb,<*a*>],{}},{[lb,<*a*>]}} is non empty non with_zero V90() set
(a) is Element of the InstructionsF of ()
<*a*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[6,<*a*>,{}] is V1() V2() set
[6,<*a*>] is V1() set
{6,<*a*>} is non empty non with_zero V90() set
{{6,<*a*>},{6}} is non empty non with_zero V90() set
[[6,<*a*>],{}] is V1() set
{[6,<*a*>],{}} is non empty set
{[6,<*a*>]} is non empty Relation-like Function-like set
{{[6,<*a*>],{}},{[6,<*a*>]}} is non empty non with_zero V90() set
lb is Element of Segm 9
a is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
<*a*> is non empty Relation-like NAT -defined NAT -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of NAT
b is Element of SCM-Data-Loc
<*b*> is non empty Relation-like NAT -defined SCM-Data-Loc -valued Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() FinSequence of SCM-Data-Loc
[lb,<*a*>,<*b*>] is V1() V2() set
[lb,<*a*>] is V1() set
{lb,<*a*>} is non empty set
{lb} is non empty set
{{lb,<*a*>},{lb}} is non empty non with_zero V90() set
[[lb,<*a*>],<*b*>] is V1() set
{[lb,<*a*>],<*b*>} is non empty set
{[lb,<*a*>]} is non empty Relation-like Function-like set
{{[lb,<*a*>],<*b*>},{[lb,<*a*>]}} is non empty non with_zero V90() set
a is Int-like Element of the carrier of ()
(a,a) is Element of the InstructionsF of ()
<*a*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*a*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[7,<*a*>,<*a*>] is V1() V2() set
[7,<*a*>] is V1() set
{7,<*a*>} is non empty non with_zero V90() set
{{7,<*a*>},{7}} is non empty non with_zero V90() set
[[7,<*a*>],<*a*>] is V1() set
{[7,<*a*>],<*a*>} is non empty set
{[7,<*a*>]} is non empty Relation-like Function-like set
{{[7,<*a*>],<*a*>},{[7,<*a*>]}} is non empty non with_zero V90() set
(a,a) is Element of the InstructionsF of ()
[8,<*a*>,<*a*>] is V1() V2() set
[8,<*a*>] is V1() set
{8,<*a*>} is non empty non with_zero V90() set
{{8,<*a*>},{8}} is non empty non with_zero V90() set
[[8,<*a*>],<*a*>] is V1() set
{[8,<*a*>],<*a*>} is non empty set
{[8,<*a*>]} is non empty Relation-like Function-like set
{{[8,<*a*>],<*a*>},{[8,<*a*>]}} is non empty non with_zero V90() set
lb is Element of Segm 9
a is Element of SCM-Data-Loc
b is Element of SCM-Data-Loc
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[lb,{},<*a,b*>] is V1() V2() set
[lb,{}] is V1() set
{lb,{}} is non empty set
{lb} is non empty set
{{lb,{}},{lb}} is non empty non with_zero V90() set
[[lb,{}],<*a,b*>] is V1() set
{[lb,{}],<*a,b*>} is non empty set
{[lb,{}]} is non empty Relation-like Function-like set
{{[lb,{}],<*a,b*>},{[lb,{}]}} is non empty non with_zero V90() set
a is Int-like Element of the carrier of ()
b is Int-like Element of the carrier of ()
(a,b) is Element of the InstructionsF of ()
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[1,{},<*a,b*>] is V1() V2() set
[[1,{}],<*a,b*>] is V1() set
{[1,{}],<*a,b*>} is non empty set
{{[1,{}],<*a,b*>},{[1,{}]}} is non empty non with_zero V90() set
(a,b) is Element of the InstructionsF of ()
[2,{},<*a,b*>] is V1() V2() set
[[2,{}],<*a,b*>] is V1() set
{[2,{}],<*a,b*>} is non empty set
{{[2,{}],<*a,b*>},{[2,{}]}} is non empty non with_zero V90() set
(a,b) is Element of the InstructionsF of ()
[3,{},<*a,b*>] is V1() V2() set
[[3,{}],<*a,b*>] is V1() set
{[3,{}],<*a,b*>} is non empty set
{{[3,{}],<*a,b*>},{[3,{}]}} is non empty non with_zero V90() set
(a,b) is Element of the InstructionsF of ()
[4,{},<*a,b*>] is V1() V2() set
[[4,{}],<*a,b*>] is V1() set
{[4,{}],<*a,b*>} is non empty set
{{[4,{}],<*a,b*>},{[4,{}]}} is non empty non with_zero V90() set
(a,b) is Element of the InstructionsF of ()
[5,{},<*a,b*>] is V1() V2() set
[[5,{}],<*a,b*>] is V1() set
{[5,{}],<*a,b*>} is non empty set
{{[5,{}],<*a,b*>},{[5,{}]}} is non empty non with_zero V90() set
lb is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(lb,a) is Element of the InstructionsF of ()
<*lb,a*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[1,{},<*lb,a*>] is V1() V2() set
[[1,{}],<*lb,a*>] is V1() set
{[1,{}],<*lb,a*>} is non empty set
{{[1,{}],<*lb,a*>},{[1,{}]}} is non empty non with_zero V90() set
b is Int-like Element of the carrier of ()
a is Int-like Element of the carrier of ()
(b,a) is Element of the InstructionsF of ()
<*b,a*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[2,{},<*b,a*>] is V1() V2() set
[[2,{}],<*b,a*>] is V1() set
{[2,{}],<*b,a*>} is non empty set
{{[2,{}],<*b,a*>},{[2,{}]}} is non empty non with_zero V90() set
b is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(b,t) is Element of the InstructionsF of ()
<*b,t*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[3,{},<*b,t*>] is V1() V2() set
[[3,{}],<*b,t*>] is V1() set
{[3,{}],<*b,t*>} is non empty set
{{[3,{}],<*b,t*>},{[3,{}]}} is non empty non with_zero V90() set
t is Int-like Element of the carrier of ()
w is Int-like Element of the carrier of ()
(t,w) is Element of the InstructionsF of ()
<*t,w*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[4,{},<*t,w*>] is V1() V2() set
[[4,{}],<*t,w*>] is V1() set
{[4,{}],<*t,w*>} is non empty set
{{[4,{}],<*t,w*>},{[4,{}]}} is non empty non with_zero V90() set
e is Int-like Element of the carrier of ()
c is Int-like Element of the carrier of ()
(e,c) is Element of the InstructionsF of ()
<*e,c*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[5,{},<*e,c*>] is V1() V2() set
[[5,{}],<*e,c*>] is V1() set
{[5,{}],<*e,c*>} is non empty set
{{[5,{}],<*e,c*>},{[5,{}]}} is non empty non with_zero V90() set
mn is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(mn) is Element of the InstructionsF of ()
<*mn*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[6,<*mn*>,{}] is V1() V2() set
[6,<*mn*>] is V1() set
{6,<*mn*>} is non empty non with_zero V90() set
{{6,<*mn*>},{6}} is non empty non with_zero V90() set
[[6,<*mn*>],{}] is V1() set
{[6,<*mn*>],{}} is non empty set
{[6,<*mn*>]} is non empty Relation-like Function-like set
{{[6,<*mn*>],{}},{[6,<*mn*>]}} is non empty non with_zero V90() set
c14 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
c13 is Int-like Element of the carrier of ()
(c14,c13) is Element of the InstructionsF of ()
<*c14*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*c13*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[7,<*c14*>,<*c13*>] is V1() V2() set
[7,<*c14*>] is V1() set
{7,<*c14*>} is non empty non with_zero V90() set
{{7,<*c14*>},{7}} is non empty non with_zero V90() set
[[7,<*c14*>],<*c13*>] is V1() set
{[7,<*c14*>],<*c13*>} is non empty set
{[7,<*c14*>]} is non empty Relation-like Function-like set
{{[7,<*c14*>],<*c13*>},{[7,<*c14*>]}} is non empty non with_zero V90() set
c16 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
c15 is Int-like Element of the carrier of ()
(c16,c15) is Element of the InstructionsF of ()
<*c16*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*c15*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[8,<*c16*>,<*c15*>] is V1() V2() set
[8,<*c16*>] is V1() set
{8,<*c16*>} is non empty non with_zero V90() set
{{8,<*c16*>},{8}} is non empty non with_zero V90() set
[[8,<*c16*>],<*c15*>] is V1() set
{[8,<*c16*>],<*c15*>} is non empty set
{[8,<*c16*>]} is non empty Relation-like Function-like set
{{[8,<*c16*>],<*c15*>},{[8,<*c16*>]}} is non empty non with_zero V90() set
lb is Element of the InstructionsF of ()
a is Int-like Element of the carrier of ()
b is Int-like Element of the carrier of ()
(a,b) is Element of the InstructionsF of ()
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[1,{},<*a,b*>] is V1() V2() set
[[1,{}],<*a,b*>] is V1() set
{[1,{}],<*a,b*>} is non empty set
{{[1,{}],<*a,b*>},{[1,{}]}} is non empty non with_zero V90() set
a is Int-like Element of the carrier of ()
b is Int-like Element of the carrier of ()
(a,b) is Element of the InstructionsF of ()
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[2,{},<*a,b*>] is V1() V2() set
[[2,{}],<*a,b*>] is V1() set
{[2,{}],<*a,b*>} is non empty set
{{[2,{}],<*a,b*>},{[2,{}]}} is non empty non with_zero V90() set
a is Int-like Element of the carrier of ()
b is Int-like Element of the carrier of ()
(a,b) is Element of the InstructionsF of ()
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[3,{},<*a,b*>] is V1() V2() set
[[3,{}],<*a,b*>] is V1() set
{[3,{}],<*a,b*>} is non empty set
{{[3,{}],<*a,b*>},{[3,{}]}} is non empty non with_zero V90() set
a is Int-like Element of the carrier of ()
b is Int-like Element of the carrier of ()
(a,b) is Element of the InstructionsF of ()
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[4,{},<*a,b*>] is V1() V2() set
[[4,{}],<*a,b*>] is V1() set
{[4,{}],<*a,b*>} is non empty set
{{[4,{}],<*a,b*>},{[4,{}]}} is non empty non with_zero V90() set
a is Int-like Element of the carrier of ()
b is Int-like Element of the carrier of ()
(a,b) is Element of the InstructionsF of ()
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[5,{},<*a,b*>] is V1() V2() set
[[5,{}],<*a,b*>] is V1() set
{[5,{}],<*a,b*>} is non empty set
{{[5,{}],<*a,b*>},{[5,{}]}} is non empty non with_zero V90() set
a is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(a) is Element of the InstructionsF of ()
<*a*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[6,<*a*>,{}] is V1() V2() set
[6,<*a*>] is V1() set
{6,<*a*>} is non empty non with_zero V90() set
{{6,<*a*>},{6}} is non empty non with_zero V90() set
[[6,<*a*>],{}] is V1() set
{[6,<*a*>],{}} is non empty set
{[6,<*a*>]} is non empty Relation-like Function-like set
{{[6,<*a*>],{}},{[6,<*a*>]}} is non empty non with_zero V90() set
b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
a is Int-like Element of the carrier of ()
(b,a) is Element of the InstructionsF of ()
<*b*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*a*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[7,<*b*>,<*a*>] is V1() V2() set
[7,<*b*>] is V1() set
{7,<*b*>} is non empty non with_zero V90() set
{{7,<*b*>},{7}} is non empty non with_zero V90() set
[[7,<*b*>],<*a*>] is V1() set
{[7,<*b*>],<*a*>} is non empty set
{[7,<*b*>]} is non empty Relation-like Function-like set
{{[7,<*b*>],<*a*>},{[7,<*b*>]}} is non empty non with_zero V90() set
b is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
a is Int-like Element of the carrier of ()
(b,a) is Element of the InstructionsF of ()
<*b*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*a*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[8,<*b*>,<*a*>] is V1() V2() set
[8,<*b*>] is V1() set
{8,<*b*>} is non empty non with_zero V90() set
{{8,<*b*>},{8}} is non empty non with_zero V90() set
[[8,<*b*>],<*a*>] is V1() set
{[8,<*b*>],<*a*>} is non empty set
{[8,<*b*>]} is non empty Relation-like Function-like set
{{[8,<*b*>],<*a*>},{[8,<*b*>]}} is non empty non with_zero V90() set
halt () is Element of the InstructionsF of ()
halt the InstructionsF of () is V100( the InstructionsF of ()) Element of the InstructionsF of ()
i is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
[1,i] is V1() set
{1,i} is non empty set
{{1,i},{1}} is non empty non with_zero V90() set
lb is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
[1,lb] is V1() set
{1,lb} is non empty set
{{1,lb},{1}} is non empty non with_zero V90() set
i is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
lb is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(i) is Int-like Element of the carrier of ()
[1,i] is V1() set
{1,i} is non empty set
{{1,i},{1}} is non empty non with_zero V90() set
(lb) is Int-like Element of the carrier of ()
[1,lb] is V1() set
{1,lb} is non empty set
{{1,lb},{1}} is non empty non with_zero V90() set
i is Int-like Element of the carrier of ()
Values i is non empty set
(the_Values_of ()) . i is set
i is Int-like Element of the carrier of ()
lb is V86() integer complex ext-real set
i .--> lb is V5() Relation-like {i} -defined Function-like one-to-one constant set
{i} is non empty set
{i} --> lb is non empty Relation-like {i} -defined Function-like constant V35({i}) V36({i},{lb}) Element of K32(K33({i},{lb}))
{lb} is non empty set
K33({i},{lb}) is Relation-like set
K32(K33({i},{lb})) is set
Values i is non empty set
(the_Values_of ()) . i is set
a is Element of (the_Values_of ()) . i
i .--> a is V5() Relation-like {i} -defined Function-like one-to-one constant set
{i} --> a is non empty Relation-like {i} -defined Function-like constant V35({i}) V36({i},{a}) Element of K32(K33({i},{a}))
{a} is non empty set
K33({i},{a}) is Relation-like set
K32(K33({i},{a})) is set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
a is V86() integer complex ext-real set
b is V86() integer complex ext-real set
(i,lb) --> (a,b) is Relation-like Function-like set
Values i is non empty set
(the_Values_of ()) . i is set
Values lb is non empty set
(the_Values_of ()) . lb is set
a is Element of Values i
b is Element of Values lb
(i,lb) --> (a,b) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible set
i is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(i) is Int-like Element of the carrier of ()
[1,i] is V1() set
{1,i} is non empty set
{{1,i},{1}} is non empty non with_zero V90() set
lb is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
i is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(i) is Int-like Element of the carrier of ()
[1,i] is V1() set
{1,i} is non empty set
{{1,i},{1}} is non empty non with_zero V90() set
i is Element of the InstructionsF of ()
lb is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
Exec (i,lb) is Relation-like the carrier of () -defined Function-like the_Values_of () -compatible V35( the carrier of ()) set
K233(( the Object-Kind of () * the ValuesF of ())) is functional V82() V83() set
K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))) is set
the Execution of () is Relation-like Function-like V36( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) Element of K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))))
K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))) is Relation-like set
K32(K33( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))))) is set
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),i) is Element of K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ())))
K147( the InstructionsF of (),K145(K233(( the Object-Kind of () * the ValuesF of ())),K233(( the Object-Kind of () * the ValuesF of ()))), the Execution of (),i) . lb is set
(Exec (i,lb)) . (IC ) is set
IC lb is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
lb . (IC ) is set
succ (IC lb) is non empty epsilon-transitive epsilon-connected ordinal natural V86() integer with_zero complex ext-real Element of omega
K417((IC lb),1) is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of NAT
i is Element of the InstructionsF of ()
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[1,{},<*i,lb*>] is V1() V2() set
[[1,{}],<*i,lb*>] is V1() set
{[1,{}],<*i,lb*>} is non empty set
{{[1,{}],<*i,lb*>},{[1,{}]}} is non empty non with_zero V90() set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[2,{},<*i,lb*>] is V1() V2() set
[[2,{}],<*i,lb*>] is V1() set
{[2,{}],<*i,lb*>} is non empty set
{{[2,{}],<*i,lb*>},{[2,{}]}} is non empty non with_zero V90() set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[3,{},<*i,lb*>] is V1() V2() set
[[3,{}],<*i,lb*>] is V1() set
{[3,{}],<*i,lb*>} is non empty set
{{[3,{}],<*i,lb*>},{[3,{}]}} is non empty non with_zero V90() set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[4,{},<*i,lb*>] is V1() V2() set
[[4,{}],<*i,lb*>] is V1() set
{[4,{}],<*i,lb*>} is non empty set
{{[4,{}],<*i,lb*>},{[4,{}]}} is non empty non with_zero V90() set
i is Int-like Element of the carrier of ()
lb is Int-like Element of the carrier of ()
(i,lb) is Element of the InstructionsF of ()
<*i,lb*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[5,{},<*i,lb*>] is V1() V2() set
[[5,{}],<*i,lb*>] is V1() set
{[5,{}],<*i,lb*>} is non empty set
{{[5,{}],<*i,lb*>},{[5,{}]}} is non empty non with_zero V90() set
i is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(i) is Element of the InstructionsF of ()
<*i*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[6,<*i*>,{}] is V1() V2() set
[6,<*i*>] is V1() set
{6,<*i*>} is non empty non with_zero V90() set
{{6,<*i*>},{6}} is non empty non with_zero V90() set
[[6,<*i*>],{}] is V1() set
{[6,<*i*>],{}} is non empty set
{[6,<*i*>]} is non empty Relation-like Function-like set
{{[6,<*i*>],{}},{[6,<*i*>]}} is non empty non with_zero V90() set
lb is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
i is Int-like Element of the carrier of ()
(lb,i) is Element of the InstructionsF of ()
<*lb*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*i*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[7,<*lb*>,<*i*>] is V1() V2() set
[7,<*lb*>] is V1() set
{7,<*lb*>} is non empty non with_zero V90() set
{{7,<*lb*>},{7}} is non empty non with_zero V90() set
[[7,<*lb*>],<*i*>] is V1() set
{[7,<*lb*>],<*i*>} is non empty set
{[7,<*lb*>]} is non empty Relation-like Function-like set
{{[7,<*lb*>],<*i*>},{[7,<*lb*>]}} is non empty non with_zero V90() set
lb is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
i is Int-like Element of the carrier of ()
(lb,i) is Element of the InstructionsF of ()
<*lb*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*i*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[8,<*lb*>,<*i*>] is V1() V2() set
[8,<*lb*>] is V1() set
{8,<*lb*>} is non empty non with_zero V90() set
{{8,<*lb*>},{8}} is non empty non with_zero V90() set
[[8,<*lb*>],<*i*>] is V1() set
{[8,<*lb*>],<*i*>} is non empty set
{[8,<*lb*>]} is non empty Relation-like Function-like set
{{[8,<*lb*>],<*i*>},{[8,<*lb*>]}} is non empty non with_zero V90() set
i is set
lb is set
a is Int-like Element of the carrier of ()
b is Int-like Element of the carrier of ()
(a,b) is Element of the InstructionsF of ()
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[1,{},<*a,b*>] is V1() V2() set
[[1,{}],<*a,b*>] is V1() set
{[1,{}],<*a,b*>} is non empty set
{{[1,{}],<*a,b*>},{[1,{}]}} is non empty non with_zero V90() set
a is Int-like Element of the carrier of ()
b is Int-like Element of the carrier of ()
(a,b) is Element of the InstructionsF of ()
<*a,b*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[2,{},<*a,b*>] is V1() V2() set
[[2,{}],<*a,b*>] is V1() set
{[2,{}],<*a,b*>} is non empty set
{{[2,{}],<*a,b*>},{[2,{}]}} is non empty non with_zero V90() set
t is Int-like Element of the carrier of ()
t is Int-like Element of the carrier of ()
(t,t) is Element of the InstructionsF of ()
<*t,t*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[3,{},<*t,t*>] is V1() V2() set
[[3,{}],<*t,t*>] is V1() set
{[3,{}],<*t,t*>} is non empty set
{{[3,{}],<*t,t*>},{[3,{}]}} is non empty non with_zero V90() set
w is Int-like Element of the carrier of ()
e is Int-like Element of the carrier of ()
(w,e) is Element of the InstructionsF of ()
<*w,e*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[4,{},<*w,e*>] is V1() V2() set
[[4,{}],<*w,e*>] is V1() set
{[4,{}],<*w,e*>} is non empty set
{{[4,{}],<*w,e*>},{[4,{}]}} is non empty non with_zero V90() set
c is Int-like Element of the carrier of ()
mn is Int-like Element of the carrier of ()
(c,mn) is Element of the InstructionsF of ()
<*c,mn*> is non empty Relation-like NAT -defined Function-like V24() 2 -element FinSequence-like FinSubsequence-like V84() set
[5,{},<*c,mn*>] is V1() V2() set
[[5,{}],<*c,mn*>] is V1() set
{[5,{}],<*c,mn*>} is non empty set
{{[5,{}],<*c,mn*>},{[5,{}]}} is non empty non with_zero V90() set
c13 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
(c13) is Element of the InstructionsF of ()
<*c13*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[6,<*c13*>,{}] is V1() V2() set
[6,<*c13*>] is V1() set
{6,<*c13*>} is non empty non with_zero V90() set
{{6,<*c13*>},{6}} is non empty non with_zero V90() set
[[6,<*c13*>],{}] is V1() set
{[6,<*c13*>],{}} is non empty set
{[6,<*c13*>]} is non empty Relation-like Function-like set
{{[6,<*c13*>],{}},{[6,<*c13*>]}} is non empty non with_zero V90() set
c15 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
c14 is Int-like Element of the carrier of ()
(c15,c14) is Element of the InstructionsF of ()
<*c15*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*c14*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[7,<*c15*>,<*c14*>] is V1() V2() set
[7,<*c15*>] is V1() set
{7,<*c15*>} is non empty non with_zero V90() set
{{7,<*c15*>},{7}} is non empty non with_zero V90() set
[[7,<*c15*>],<*c14*>] is V1() set
{[7,<*c15*>],<*c14*>} is non empty set
{[7,<*c15*>]} is non empty Relation-like Function-like set
{{[7,<*c15*>],<*c14*>},{[7,<*c15*>]}} is non empty non with_zero V90() set
c17 is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real set
c16 is Int-like Element of the carrier of ()
(c17,c16) is Element of the InstructionsF of ()
<*c17*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
<*c16*> is non empty Relation-like NAT -defined Function-like V24() 1 -element FinSequence-like FinSubsequence-like V84() set
[8,<*c17*>,<*c16*>] is V1() V2() set
[8,<*c17*>] is V1() set
{8,<*c17*>} is non empty non with_zero V90() set
{{8,<*c17*>},{8}} is non empty non with_zero V90() set
[[8,<*c17*>],<*c16*>] is V1() set
{[8,<*c17*>],<*c16*>} is non empty set
{[8,<*c17*>]} is non empty Relation-like Function-like set
{{[8,<*c17*>],<*c16*>},{[8,<*c17*>]}} is non empty non with_zero V90() set
halt () is halting Element of the InstructionsF of ()
halt the InstructionsF of () is V100( the InstructionsF of ()) Element of the InstructionsF of ()
i is Element of the InstructionsF of ()
NonZero () is Element of K32( the carrier of ())
K32( the carrier of ()) is set
[#] () is Element of K32( the carrier of ())
{(IC )} is non empty set
([#] ()) \ {(IC )} is Element of K32( the carrier of ())
{NAT} \/ SCM-Data-Loc is non empty set
({NAT} \/ SCM-Data-Loc) \ {NAT} is Element of K32(({NAT} \/ SCM-Data-Loc))
K32(({NAT} \/ SCM-Data-Loc)) is set
SCM-Data-Loc \/ {NAT} is non empty set
(SCM-Data-Loc \/ {NAT}) \ {NAT} is Element of K32((SCM-Data-Loc \/ {NAT}))
K32((SCM-Data-Loc \/ {NAT})) is set
SCM-Data-Loc \ {NAT} is Element of K32(SCM-Memory)
i is Int-like Element of the carrier of ()
i is Relation-like Function-like SCM-OK * SCM-VAL -compatible Element of K233((SCM-OK * SCM-VAL))
i is Element of SCM-Instr
InsCode i is epsilon-transitive epsilon-connected ordinal natural V86() integer complex ext-real Element of InsCodes SCM-Instr
K13(i) is set
K13(K13(i)) is set