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