:: AMI_3 semantic presentation

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

{ [b

{[SCM-Halt,{},{}]} \/ { [b

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)

{ [b

({[SCM-Halt,{},{}]} \/ { [b

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)

{ [b

(({[SCM-Halt,{},{}]} \/ { [b

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