:: SCMRING2 semantic presentation

REAL is set

NAT is V6() V7() V8() non empty V24() countable denumerable Element of K27(REAL)

K27(REAL) is set

NAT is V6() V7() V8() non empty V24() countable denumerable set

K27(NAT) is set

K27(NAT) is set

9 is V6() V7() V8() V12() non empty V62() V164() Element of NAT

Segm 9 is countable Element of K27(NAT)

K195() is non empty set

SCM-Memory is non empty set

{NAT} is set

{NAT} \/ K195() is set

K27(SCM-Memory) is set

2 is V6() V7() V8() V12() non empty V62() V164() Element of NAT

K28(SCM-Memory,2) is set

K27(K28(SCM-Memory,2)) is set

SCM-OK is Relation-like SCM-Memory -defined 2 -valued Function-like quasi_total Element of K27(K28(SCM-Memory,2))

SCM-VAL is Relation-like 2 -defined Function-like V35(2) set

INT is set

K261(NAT,INT) is set

SCM-OK * SCM-VAL is Relation-like non-empty Function-like set

product (SCM-OK * SCM-VAL) is functional non empty with_common_domain product-like set

K196() is non empty V19() standard-ins V71() V72() V74() set

Funcs ((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))) is set

K28(K196(),(Funcs ((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))))) is set

K27(K28(K196(),(Funcs ((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL)))))) is set

SCM is non empty with_non-empty_values IC-Ins-separated strict strict halting AMI-Struct over 2

In (NAT,SCM-Memory) is Element of SCM-Memory

SCM-Exec is Relation-like K196() -defined Funcs ((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))) -valued Function-like quasi_total Element of K27(K28(K196(),(Funcs ((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))))))

AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),K196(),SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2

the InstructionsF of SCM is standard-ins V71() V72() V74() set

the carrier of SCM is non empty set

the_Values_of SCM is Relation-like the carrier of SCM -defined Function-like V35( the carrier of SCM) set

the Object-Kind of SCM is Relation-like the carrier of SCM -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of SCM,2))

K28( the carrier of SCM,2) is set

K27(K28( the carrier of SCM,2)) is set

the ValuesF of SCM is Relation-like 2 -defined Function-like V35(2) set

the Object-Kind of SCM * the ValuesF of SCM is Relation-like Function-like set

SCM-Data-Loc is non empty Element of K27(SCM-Memory)

COMPLEX is set

RAT is set

{} is set

the V6() V7() V8() V10() V11() V12() Function-like functional empty FinSequence-membered set is V6() V7() V8() V10() V11() V12() Function-like functional empty FinSequence-membered set

1 is V6() V7() V8() V12() non empty V62() V164() Element of NAT

3 is V6() V7() V8() V12() non empty V62() V164() Element of NAT

NonZero SCM is Element of K27( the carrier of SCM)

K27( the carrier of SCM) is set

[#] SCM is non empty non proper Element of K27( the carrier of SCM)

0. SCM is V47( SCM ) Element of the carrier of SCM

the ZeroF of SCM is Element of the carrier of SCM

{(0. SCM)} is set

([#] SCM) \ {(0. SCM)} is Element of K27( the carrier of SCM)

4 is V6() V7() V8() V12() non empty V62() V164() Element of NAT

6 is V6() V7() V8() V12() non empty V62() V164() Element of NAT

7 is V6() V7() V8() V12() non empty V62() V164() Element of NAT

5 is V6() V7() V8() V12() non empty V62() V164() Element of NAT

8 is V6() V7() V8() V12() non empty V62() V164() Element of NAT

Segm 8 is countable Element of K27(NAT)

0 is V6() V7() V8() V12() Element of NAT

[0,{},{}] is V21() V22() set

[0,{}] is V21() set

[[0,{}],{}] is V21() set

K131(1,2,3,4) is set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

{[0,{},{}]} is set

{ [b

{[0,{},{}]} \/ { [b

{ [6,<*b

({[0,{},{}]} \/ { [b

{ [7,<*b

(({[0,{},{}]} \/ { [b

the carrier of x is non empty set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

SCM-VAL x is Relation-like 2 -defined Function-like V35(2) set

K261(NAT, the carrier of x) is set

SCM-Exec x is Relation-like SCM-Instr x -defined Funcs ((product (SCM-OK * (SCM-VAL x))),(product (SCM-OK * (SCM-VAL x)))) -valued Function-like quasi_total Element of K27(K28((SCM-Instr x),(Funcs ((product (SCM-OK * (SCM-VAL x))),(product (SCM-OK * (SCM-VAL x)))))))

SCM-OK * (SCM-VAL x) is Relation-like non-empty Function-like set

product (SCM-OK * (SCM-VAL x)) is functional non empty with_common_domain product-like set

Funcs ((product (SCM-OK * (SCM-VAL x))),(product (SCM-OK * (SCM-VAL x)))) is set

K28((SCM-Instr x),(Funcs ((product (SCM-OK * (SCM-VAL x))),(product (SCM-OK * (SCM-VAL x)))))) is set

K27(K28((SCM-Instr x),(Funcs ((product (SCM-OK * (SCM-VAL x))),(product (SCM-OK * (SCM-VAL x))))))) is set

AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) is strict AMI-Struct over 2

the carrier of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) is set

the ZeroF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) is Element of the carrier of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #)

the InstructionsF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) is standard-ins V71() V72() V74() set

the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) is Relation-like the carrier of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #),2))

K28( the carrier of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #),2) is set

K27(K28( the carrier of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #),2)) is set

the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) is Relation-like 2 -defined Function-like V35(2) set

the Execution of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) is Relation-like the InstructionsF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) -defined Funcs ((product ( the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #))),(product ( the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #)))) -valued Function-like quasi_total Element of K27(K28( the InstructionsF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #),(Funcs ((product ( the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #))),(product ( the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #)))))))

the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) is Relation-like Function-like set

product ( the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #)) is functional with_common_domain product-like set

Funcs ((product ( the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #))),(product ( the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #)))) is set

K28( the InstructionsF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #),(Funcs ((product ( the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #))),(product ( the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #)))))) is set

K27(K28( the InstructionsF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #),(Funcs ((product ( the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #))),(product ( the Object-Kind of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #) * the ValuesF of AMI-Struct(# SCM-Memory,(In (NAT,SCM-Memory)),(SCM-Instr x),SCM-OK,(SCM-VAL x),(SCM-Exec x) #))))))) is set

R is strict AMI-Struct over 2

the carrier of R is set

the ZeroF of R is Element of the carrier of R

the InstructionsF of R is standard-ins V71() V72() V74() set

the Object-Kind of R is Relation-like the carrier of R -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of R,2))

K28( the carrier of R,2) is set

K27(K28( the carrier of R,2)) is set

the ValuesF of R is Relation-like 2 -defined Function-like V35(2) set

the Execution of R is Relation-like the InstructionsF of R -defined Funcs ((product ( the Object-Kind of R * the ValuesF of R)),(product ( the Object-Kind of R * the ValuesF of R))) -valued Function-like quasi_total Element of K27(K28( the InstructionsF of R,(Funcs ((product ( the Object-Kind of R * the ValuesF of R)),(product ( the Object-Kind of R * the ValuesF of R))))))

the Object-Kind of R * the ValuesF of R is Relation-like Function-like set

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

Funcs ((product ( the Object-Kind of R * the ValuesF of R)),(product ( the Object-Kind of R * the ValuesF of R))) is set

K28( the InstructionsF of R,(Funcs ((product ( the Object-Kind of R * the ValuesF of R)),(product ( the Object-Kind of R * the ValuesF of R))))) is set

K27(K28( the InstructionsF of R,(Funcs ((product ( the Object-Kind of R * the ValuesF of R)),(product ( the Object-Kind of R * the ValuesF of R)))))) is set

W is strict AMI-Struct over 2

the carrier of W is set

the ZeroF of W is Element of the carrier of W

the InstructionsF of W is standard-ins V71() V72() V74() set

the Object-Kind of W is Relation-like the carrier of W -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of W,2))

K28( the carrier of W,2) is set

K27(K28( the carrier of W,2)) is set

the ValuesF of W is Relation-like 2 -defined Function-like V35(2) set

the Execution of W is Relation-like the InstructionsF of W -defined Funcs ((product ( the Object-Kind of W * the ValuesF of W)),(product ( the Object-Kind of W * the ValuesF of W))) -valued Function-like quasi_total Element of K27(K28( the InstructionsF of W,(Funcs ((product ( the Object-Kind of W * the ValuesF of W)),(product ( the Object-Kind of W * the ValuesF of W))))))

the Object-Kind of W * the ValuesF of W is Relation-like Function-like set

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

Funcs ((product ( the Object-Kind of W * the ValuesF of W)),(product ( the Object-Kind of W * the ValuesF of W))) is set

K28( the InstructionsF of W,(Funcs ((product ( the Object-Kind of W * the ValuesF of W)),(product ( the Object-Kind of W * the ValuesF of W))))) is set

K27(K28( the InstructionsF of W,(Funcs ((product ( the Object-Kind of W * the ValuesF of W)),(product ( the Object-Kind of W * the ValuesF of W)))))) is set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is strict AMI-Struct over 2

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty strict AMI-Struct over 2

the_Values_of (x) is Relation-like the carrier of (x) -defined Function-like V35( the carrier of (x)) set

the carrier of (x) is non empty set

the Object-Kind of (x) is Relation-like the carrier of (x) -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of (x),2))

K28( the carrier of (x),2) is set

K27(K28( the carrier of (x),2)) is set

the ValuesF of (x) is Relation-like 2 -defined Function-like V35(2) set

the Object-Kind of (x) * the ValuesF of (x) is Relation-like Function-like set

SCM-OK * the ValuesF of (x) is Relation-like Function-like set

SCM-VAL x is Relation-like 2 -defined Function-like V35(2) set

the carrier of x is non empty set

K261(NAT, the carrier of x) is set

SCM-OK * (SCM-VAL x) is Relation-like non-empty Function-like set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty strict AMI-Struct over 2

the_Values_of (x) is Relation-like the carrier of (x) -defined Function-like V35( the carrier of (x)) set

the carrier of (x) is non empty set

the Object-Kind of (x) is Relation-like the carrier of (x) -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of (x),2))

K28( the carrier of (x),2) is set

K27(K28( the carrier of (x),2)) is set

the ValuesF of (x) is Relation-like 2 -defined Function-like V35(2) set

the Object-Kind of (x) * the ValuesF of (x) is Relation-like Function-like set

SCM-VAL x is Relation-like 2 -defined Function-like V35(2) set

the carrier of x is non empty set

K261(NAT, the carrier of x) is set

SCM-OK * (SCM-VAL x) is Relation-like non-empty Function-like set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values strict AMI-Struct over 2

the carrier of (x) is non empty set

the carrier of (x) \ {NAT} is Element of K27( the carrier of (x))

K27( the carrier of (x)) is set

SCM-Memory \ {NAT} is Element of K27(SCM-Memory)

{NAT} \/ SCM-Data-Loc is set

({NAT} \/ SCM-Data-Loc) \ {NAT} is Element of K27(({NAT} \/ SCM-Data-Loc))

K27(({NAT} \/ SCM-Data-Loc)) is set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values strict AMI-Struct over 2

the carrier of (x) is non empty set

the Element of SCM-Data-Loc is Element of SCM-Data-Loc

R is Element of the carrier of (x)

x is set

R is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(R) is non empty with_non-empty_values strict AMI-Struct over 2

the carrier of (R) is non empty set

W is set

s is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(s) is non empty with_non-empty_values strict AMI-Struct over 2

the carrier of (s) is non empty set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values strict AMI-Struct over 2

the carrier of (x) is non empty set

the_Values_of (x) is Relation-like the carrier of (x) -defined Function-like V35( the carrier of (x)) set

the Object-Kind of (x) is Relation-like the carrier of (x) -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of (x),2))

K28( the carrier of (x),2) is set

K27(K28( the carrier of (x),2)) is set

the ValuesF of (x) is Relation-like 2 -defined Function-like V35(2) set

the Object-Kind of (x) * the ValuesF of (x) is Relation-like Function-like set

R is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set

W is Int-like Element of the carrier of (x)

R . W is set

the carrier of x is non empty set

SCM-VAL x is Relation-like 2 -defined Function-like V35(2) set

K261(NAT, the carrier of x) is set

SCM-OK * (SCM-VAL x) is Relation-like non-empty Function-like set

product (SCM-OK * (SCM-VAL x)) is functional non empty with_common_domain product-like set

s is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

s is Element of SCM-Data-Loc

s . s is Element of the carrier of x

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values strict AMI-Struct over 2

the InstructionsF of (x) is standard-ins V71() V72() V74() set

halt (x) is Element of the InstructionsF of (x)

halt the InstructionsF of (x) is Element of the InstructionsF of (x)

{1,2,3,4} is countable Element of K27(NAT)

x is non empty 1-sorted

SCM-Instr x is non empty V19() V74() set

the carrier of x is non empty set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

R is set

W is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(W) is non empty with_non-empty_values strict AMI-Struct over 2

the carrier of (W) is non empty set

s is Int-like Element of the carrier of (W)

s is Int-like Element of the carrier of (W)

<*s,s*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[R,{},<*s,s*>] is V21() V22() set

[R,{}] is V21() set

[[R,{}],<*s,s*>] is V21() set

t is Element of SCM-Data-Loc

f is Element of SCM-Data-Loc

<*t,f*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[R,{},<*t,f*>] is V21() V22() set

[[R,{}],<*t,f*>] is V21() set

x is non empty 1-sorted

the carrier of x is non empty set

SCM-Instr x is non empty V19() V74() set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

R is Element of the carrier of x

W is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(W) is non empty with_non-empty_values strict AMI-Struct over 2

the carrier of (W) is non empty set

s is Int-like Element of the carrier of (W)

<*s,R*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[5,{},<*s,R*>] is V21() V22() set

[5,{}] is V21() set

[[5,{}],<*s,R*>] is V21() set

s is Element of SCM-Data-Loc

<*s,R*> is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of x -valued Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable FinSequence of SCM-Data-Loc \/ the carrier of x

SCM-Data-Loc \/ the carrier of x is set

[5,{},<*s,R*>] is V21() V22() set

[[5,{}],<*s,R*>] is V21() set

R is V6() V7() V8() V12() Element of NAT

<*R*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

[6,<*R*>,{}] is V21() V22() set

[6,<*R*>] is V21() set

[[6,<*R*>],{}] is V21() set

x is non empty 1-sorted

SCM-Instr x is non empty V19() V74() set

the carrier of x is non empty set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

x is non empty 1-sorted

SCM-Instr x is non empty V19() V74() set

the carrier of x is non empty set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

R is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(R) is non empty with_non-empty_values strict AMI-Struct over 2

the carrier of (R) is non empty set

W is Int-like Element of the carrier of (R)

<*W*> is Relation-like NAT -defined the carrier of (R) -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (R)

s is V6() V7() V8() V12() Element of NAT

<*s*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

[7,<*s*>,<*W*>] is V21() V22() set

[7,<*s*>] is V21() set

[[7,<*s*>],<*W*>] is V21() set

s is Element of SCM-Data-Loc

<*s*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of SCM-Data-Loc

[7,<*s*>,<*s*>] is V21() V22() set

[[7,<*s*>],<*s*>] is V21() set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values strict AMI-Struct over 2

the carrier of (x) is non empty set

R is Int-like Element of the carrier of (x)

W is Int-like Element of the carrier of (x)

<*R,W*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[1,{},<*R,W*>] is V21() V22() set

[1,{}] is V21() set

[[1,{}],<*R,W*>] is V21() set

the InstructionsF of (x) is standard-ins V71() V72() V74() set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

the carrier of x is non empty set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

[2,{},<*R,W*>] is V21() V22() set

[2,{}] is V21() set

[[2,{}],<*R,W*>] is V21() set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

the carrier of x is non empty set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

[3,{},<*R,W*>] is V21() V22() set

[3,{}] is V21() set

[[3,{}],<*R,W*>] is V21() set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

the carrier of x is non empty set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

[4,{},<*R,W*>] is V21() V22() set

[4,{}] is V21() set

[[4,{}],<*R,W*>] is V21() set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

the carrier of x is non empty set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values strict AMI-Struct over 2

the carrier of (x) is non empty set

the carrier of x is non empty set

R is Int-like Element of the carrier of (x)

W is Element of the carrier of x

<*R,W*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[5,{},<*R,W*>] is V21() V22() set

[5,{}] is V21() set

[[5,{}],<*R,W*>] is V21() set

the InstructionsF of (x) is standard-ins V71() V72() V74() set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

R is V6() V7() V8() V12() Element of NAT

<*R*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

[6,<*R*>,{}] is V21() V22() set

[6,<*R*>] is V21() set

[[6,<*R*>],{}] is V21() set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values strict AMI-Struct over 2

the InstructionsF of (x) is standard-ins V71() V72() V74() set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

the carrier of x is non empty set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values strict AMI-Struct over 2

the carrier of (x) is non empty set

R is V6() V7() V8() V12() Element of NAT

<*R*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

W is Int-like Element of the carrier of (x)

<*W*> is Relation-like NAT -defined the carrier of (x) -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (x)

[7,<*R*>,<*W*>] is V21() V22() set

[7,<*R*>] is V21() set

[[7,<*R*>],<*W*>] is V21() set

the InstructionsF of (x) is standard-ins V71() V72() V74() set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

the carrier of x is non empty set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values strict AMI-Struct over 2

the InstructionsF of (x) is standard-ins V71() V72() V74() set

the carrier of (x) is non empty set

the carrier of x is non empty set

R is set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

{ [b

{[0,{},{}]} \/ { [b

({[0,{},{}]} \/ { [b

{ [7,<*b

(({[0,{},{}]} \/ { [b

{ [5,{},<*b

W is V6() V7() V8() V12() Element of NAT

<*W*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

[6,<*W*>,{}] is V21() V22() set

[6,<*W*>] is V21() set

[[6,<*W*>],{}] is V21() set

s is V6() V7() V8() V12() Element of NAT

(x,s) is Element of the InstructionsF of (x)

<*s*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

[6,<*s*>,{}] is V21() V22() set

[6,<*s*>] is V21() set

[[6,<*s*>],{}] is V21() set

W is V6() V7() V8() V12() Element of NAT

<*W*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

s is Element of NonZero SCM

<*s*> is Relation-like NAT -defined Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable set

[7,<*W*>,<*s*>] is V21() V22() set

[7,<*W*>] is V21() set

[[7,<*W*>],<*s*>] is V21() set

t is V6() V7() V8() V12() Element of NAT

s is Int-like Element of the carrier of (x)

(x,t,s) is Element of the InstructionsF of (x)

<*t*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

<*s*> is Relation-like NAT -defined the carrier of (x) -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (x)

[7,<*t*>,<*s*>] is V21() V22() set

[7,<*t*>] is V21() set

[[7,<*t*>],<*s*>] is V21() set

W is Element of NonZero SCM

s is Element of the carrier of x

<*W,s*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[5,{},<*W,s*>] is V21() V22() set

[[5,{}],<*W,s*>] is V21() set

s is Int-like Element of the carrier of (x)

(x,s,s) is Element of the InstructionsF of (x)

<*s,s*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[5,{},<*s,s*>] is V21() V22() set

[[5,{}],<*s,s*>] is V21() set

W is Element of Segm 8

s is Element of NonZero SCM

s is Element of NonZero SCM

<*s,s*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[W,{},<*s,s*>] is V21() V22() set

[W,{}] is V21() set

[[W,{}],<*s,s*>] is V21() set

t is Int-like Element of the carrier of (x)

f is Int-like Element of the carrier of (x)

(x,t,f) is Element of the InstructionsF of (x)

<*t,f*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[1,{},<*t,f*>] is V21() V22() set

[[1,{}],<*t,f*>] is V21() set

(x,t,f) is Element of the InstructionsF of (x)

[2,{},<*t,f*>] is V21() V22() set

[[2,{}],<*t,f*>] is V21() set

(x,t,f) is Element of the InstructionsF of (x)

[3,{},<*t,f*>] is V21() V22() set

[[3,{}],<*t,f*>] is V21() set

(x,t,f) is Element of the InstructionsF of (x)

[4,{},<*t,f*>] is V21() V22() set

[[4,{}],<*t,f*>] is V21() set

W is Int-like Element of the carrier of (x)

s is Int-like Element of the carrier of (x)

(x,W,s) is Element of the InstructionsF of (x)

<*W,s*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[1,{},<*W,s*>] is V21() V22() set

[[1,{}],<*W,s*>] is V21() set

s is Int-like Element of the carrier of (x)

t is Int-like Element of the carrier of (x)

(x,s,t) is Element of the InstructionsF of (x)

<*s,t*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[2,{},<*s,t*>] is V21() V22() set

[[2,{}],<*s,t*>] is V21() set

f is Int-like Element of the carrier of (x)

V is Int-like Element of the carrier of (x)

(x,f,V) is Element of the InstructionsF of (x)

<*f,V*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[3,{},<*f,V*>] is V21() V22() set

[[3,{}],<*f,V*>] is V21() set

t is Int-like Element of the carrier of (x)

t is Int-like Element of the carrier of (x)

(x,t,t) is Element of the InstructionsF of (x)

<*t,t*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[4,{},<*t,t*>] is V21() V22() set

[[4,{}],<*t,t*>] is V21() set

w is V6() V7() V8() V12() Element of NAT

(x,w) is Element of the InstructionsF of (x)

<*w*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT

[6,<*w*>,{}] is V21() V22() set

[6,<*w*>] is V21() set

[[6,<*w*>],{}] is V21() set

c

e is Int-like Element of the carrier of (x)

(x,c

<*c

<*e*> is Relation-like NAT -defined the carrier of (x) -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (x)

[7,<*c

[7,<*c

[[7,<*c

c

c

(x,c

<*c

[5,{},<*c

[[5,{}],<*c

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values strict AMI-Struct over 2

the_Values_of (x) is Relation-like the carrier of (x) -defined Function-like V35( the carrier of (x)) set

the carrier of (x) is non empty set

the Object-Kind of (x) is Relation-like the carrier of (x) -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of (x),2))

K28( the carrier of (x),2) is set

K27(K28( the carrier of (x),2)) is set

the ValuesF of (x) is Relation-like 2 -defined Function-like V35(2) set

the Object-Kind of (x) * the ValuesF of (x) is Relation-like Function-like set

SCM-VAL x is Relation-like 2 -defined Function-like V35(2) set

the carrier of x is non empty set

K261(NAT, the carrier of x) is set

SCM-OK * (SCM-VAL x) is Relation-like non-empty Function-like set

0. (x) is V47((x)) Element of the carrier of (x)

the ZeroF of (x) is Element of the carrier of (x)

Values (0. (x)) is set

(the_Values_of (x)) . (0. (x)) is set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values IC-Ins-separated strict AMI-Struct over 2

0. (x) is V47((x)) Element of the carrier of (x)

the carrier of (x) is non empty set

the ZeroF of (x) is Element of the carrier of (x)

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values IC-Ins-separated strict AMI-Struct over 2

the carrier of (x) is non empty set

the_Values_of (x) is Relation-like the carrier of (x) -defined Function-like V35( the carrier of (x)) set

the Object-Kind of (x) is Relation-like the carrier of (x) -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of (x),2))

K28( the carrier of (x),2) is set

K27(K28( the carrier of (x),2)) is set

the ValuesF of (x) is Relation-like 2 -defined Function-like V35(2) set

the Object-Kind of (x) * the ValuesF of (x) is Relation-like Function-like set

SCM-VAL x is Relation-like 2 -defined Function-like V35(2) set

the carrier of x is non empty set

K261(NAT, the carrier of x) is set

SCM-OK * (SCM-VAL x) is Relation-like non-empty Function-like set

product (SCM-OK * (SCM-VAL x)) is functional non empty with_common_domain product-like set

W is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

R is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set

IC R is V6() V7() V8() V12() Element of NAT

0. (x) is V47((x)) Element of the carrier of (x)

the ZeroF of (x) is Element of the carrier of (x)

R . (0. (x)) is set

IC W is V6() V7() V8() V12() Element of NAT

W . NAT is set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values IC-Ins-separated strict AMI-Struct over 2

the carrier of (x) is non empty set

the_Values_of (x) is Relation-like the carrier of (x) -defined Function-like V35( the carrier of (x)) set

the Object-Kind of (x) is Relation-like the carrier of (x) -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of (x),2))

K28( the carrier of (x),2) is set

K27(K28( the carrier of (x),2)) is set

the ValuesF of (x) is Relation-like 2 -defined Function-like V35(2) set

the Object-Kind of (x) * the ValuesF of (x) is Relation-like Function-like set

the InstructionsF of (x) is standard-ins V71() V72() V74() set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

the carrier of x is non empty set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

SCM-VAL x is Relation-like 2 -defined Function-like V35(2) set

K261(NAT, the carrier of x) is set

SCM-OK * (SCM-VAL x) is Relation-like non-empty Function-like set

product (SCM-OK * (SCM-VAL x)) is functional non empty with_common_domain product-like set

R is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set

W is Element of the InstructionsF of (x)

Exec (W,R) is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set

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

Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))) is set

the Execution of (x) is Relation-like the InstructionsF of (x) -defined Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))) -valued Function-like quasi_total Element of K27(K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))))))

K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))))) is set

K27(K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x))))))) is set

the Execution of (x) . W is Element of Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x))))

( the Execution of (x) . W) . R is set

s is Element of SCM-Instr x

s is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

SCM-Exec-Res (s,s) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

Funcs ((product (SCM-OK * (SCM-VAL x))),(product (SCM-OK * (SCM-VAL x)))) is set

SCM-Exec x is Relation-like SCM-Instr x -defined Funcs ((product (SCM-OK * (SCM-VAL x))),(product (SCM-OK * (SCM-VAL x)))) -valued Function-like quasi_total Element of K27(K28((SCM-Instr x),(Funcs ((product (SCM-OK * (SCM-VAL x))),(product (SCM-OK * (SCM-VAL x)))))))

K28((SCM-Instr x),(Funcs ((product (SCM-OK * (SCM-VAL x))),(product (SCM-OK * (SCM-VAL x)))))) is set

K27(K28((SCM-Instr x),(Funcs ((product (SCM-OK * (SCM-VAL x))),(product (SCM-OK * (SCM-VAL x))))))) is set

(SCM-Exec x) . s is Element of Funcs ((product (SCM-OK * (SCM-VAL x))),(product (SCM-OK * (SCM-VAL x))))

((SCM-Exec x) . s) . s is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values IC-Ins-separated strict AMI-Struct over 2

the carrier of (x) is non empty set

the_Values_of (x) is Relation-like the carrier of (x) -defined Function-like V35( the carrier of (x)) set

the Object-Kind of (x) is Relation-like the carrier of (x) -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of (x),2))

K28( the carrier of (x),2) is set

K27(K28( the carrier of (x),2)) is set

the ValuesF of (x) is Relation-like 2 -defined Function-like V35(2) set

the Object-Kind of (x) * the ValuesF of (x) is Relation-like Function-like set

0. (x) is V47((x)) Element of the carrier of (x)

the ZeroF of (x) is Element of the carrier of (x)

R is Int-like Element of the carrier of (x)

W is Int-like Element of the carrier of (x)

(x,R,W) is Element of the InstructionsF of (x)

the InstructionsF of (x) is standard-ins V71() V72() V74() set

<*R,W*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[1,{},<*R,W*>] is V21() V22() set

[[1,{}],<*R,W*>] is V21() set

s is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set

Exec ((x,R,W),s) is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set

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

Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))) is set

the Execution of (x) is Relation-like the InstructionsF of (x) -defined Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))) -valued Function-like quasi_total Element of K27(K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))))))

K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))))) is set

K27(K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x))))))) is set

the Execution of (x) . (x,R,W) is Element of Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x))))

( the Execution of (x) . (x,R,W)) . s is set

(Exec ((x,R,W),s)) . (0. (x)) is set

IC s is V6() V7() V8() V12() Element of NAT

s . (0. (x)) is set

succ (IC s) is V6() V7() V8() V12() non empty V62() Element of NAT

K401((IC s),1) is V6() V7() V8() V12() Element of NAT

(x,(Exec ((x,R,W),s)),R) is Element of the carrier of x

the carrier of x is non empty set

(x,s,W) is Element of the carrier of x

SCM-VAL x is Relation-like 2 -defined Function-like V35(2) set

K261(NAT, the carrier of x) is set

SCM-OK * (SCM-VAL x) is Relation-like non-empty Function-like set

product (SCM-OK * (SCM-VAL x)) is functional non empty with_common_domain product-like set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

s is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

t is Element of SCM-Instr x

t address_1 is Element of K195()

t address_2 is Element of K195()

s . (t address_2) is Element of the carrier of x

SCM-Chg (s,(t address_1),(s . (t address_2))) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

(t address_1) .--> (s . (t address_2)) is Relation-like K195() -defined {(t address_1)} -defined the carrier of x -valued Function-like one-to-one set

{(t address_1)} is set

{(t address_1)} --> (s . (t address_2)) is Relation-like {(t address_1)} -defined the carrier of x -valued {(s . (t address_2))} -valued Function-like constant V35({(t address_1)}) quasi_total Element of K27(K28({(t address_1)},{(s . (t address_2))}))

{(s . (t address_2))} is set

K28({(t address_1)},{(s . (t address_2))}) is set

K27(K28({(t address_1)},{(s . (t address_2))})) is set

s +* ((t address_1) .--> (s . (t address_2))) is Relation-like Function-like set

IC s is V6() V7() V8() V12() Element of NAT

s . NAT is set

SCM-Exec-Res (t,s) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

succ (IC s) is V6() V7() V8() V12() non empty V62() Element of NAT

K401((IC s),1) is V6() V7() V8() V12() Element of NAT

SCM-Chg ((SCM-Chg (s,(t address_1),(s . (t address_2)))),(succ (IC s))) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

NAT .--> (succ (IC s)) is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set

{NAT} --> (succ (IC s)) is Relation-like non-empty {NAT} -defined NAT -valued {(succ (IC s))} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{(succ (IC s))}))

{(succ (IC s))} is set

K28({NAT},{(succ (IC s))}) is set

K27(K28({NAT},{(succ (IC s))})) is set

(SCM-Chg (s,(t address_1),(s . (t address_2)))) +* (NAT .--> (succ (IC s))) is Relation-like Function-like set

V is Element of Segm 8

[V,{},<*R,W*>] is V21() V22() set

[V,{}] is V21() set

[[V,{}],<*R,W*>] is V21() set

(Exec ((x,R,W),s)) . NAT is set

(SCM-Chg (s,(t address_1),(s . (t address_2)))) . R is set

t is Int-like Element of the carrier of (x)

(x,(Exec ((x,R,W),s)),t) is Element of the carrier of x

(x,s,t) is Element of the carrier of x

(SCM-Chg (s,(t address_1),(s . (t address_2)))) . t is set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values IC-Ins-separated strict AMI-Struct over 2

the carrier of (x) is non empty set

the_Values_of (x) is Relation-like the carrier of (x) -defined Function-like V35( the carrier of (x)) set

the Object-Kind of (x) is Relation-like the carrier of (x) -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of (x),2))

K28( the carrier of (x),2) is set

K27(K28( the carrier of (x),2)) is set

the ValuesF of (x) is Relation-like 2 -defined Function-like V35(2) set

the Object-Kind of (x) * the ValuesF of (x) is Relation-like Function-like set

0. (x) is V47((x)) Element of the carrier of (x)

the ZeroF of (x) is Element of the carrier of (x)

R is Int-like Element of the carrier of (x)

W is Int-like Element of the carrier of (x)

(x,R,W) is Element of the InstructionsF of (x)

the InstructionsF of (x) is standard-ins V71() V72() V74() set

<*R,W*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[2,{},<*R,W*>] is V21() V22() set

[[2,{}],<*R,W*>] is V21() set

s is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set

Exec ((x,R,W),s) is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set

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

Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))) is set

the Execution of (x) is Relation-like the InstructionsF of (x) -defined Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))) -valued Function-like quasi_total Element of K27(K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))))))

K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))))) is set

K27(K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x))))))) is set

the Execution of (x) . (x,R,W) is Element of Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x))))

( the Execution of (x) . (x,R,W)) . s is set

(Exec ((x,R,W),s)) . (0. (x)) is set

IC s is V6() V7() V8() V12() Element of NAT

s . (0. (x)) is set

succ (IC s) is V6() V7() V8() V12() non empty V62() Element of NAT

K401((IC s),1) is V6() V7() V8() V12() Element of NAT

(x,(Exec ((x,R,W),s)),R) is Element of the carrier of x

the carrier of x is non empty set

(x,s,R) is Element of the carrier of x

(x,s,W) is Element of the carrier of x

(x,s,R) + (x,s,W) is Element of the carrier of x

SCM-VAL x is Relation-like 2 -defined Function-like V35(2) set

K261(NAT, the carrier of x) is set

SCM-OK * (SCM-VAL x) is Relation-like non-empty Function-like set

product (SCM-OK * (SCM-VAL x)) is functional non empty with_common_domain product-like set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

s is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

t is Element of SCM-Instr x

t address_1 is Element of K195()

s . (t address_1) is Element of the carrier of x

t address_2 is Element of K195()

s . (t address_2) is Element of the carrier of x

(s . (t address_1)) + (s . (t address_2)) is Element of the carrier of x

SCM-Chg (s,(t address_1),((s . (t address_1)) + (s . (t address_2)))) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

(t address_1) .--> ((s . (t address_1)) + (s . (t address_2))) is Relation-like K195() -defined {(t address_1)} -defined the carrier of x -valued Function-like one-to-one set

{(t address_1)} is set

{(t address_1)} --> ((s . (t address_1)) + (s . (t address_2))) is Relation-like {(t address_1)} -defined the carrier of x -valued {((s . (t address_1)) + (s . (t address_2)))} -valued Function-like constant V35({(t address_1)}) quasi_total Element of K27(K28({(t address_1)},{((s . (t address_1)) + (s . (t address_2)))}))

{((s . (t address_1)) + (s . (t address_2)))} is set

K28({(t address_1)},{((s . (t address_1)) + (s . (t address_2)))}) is set

K27(K28({(t address_1)},{((s . (t address_1)) + (s . (t address_2)))})) is set

s +* ((t address_1) .--> ((s . (t address_1)) + (s . (t address_2)))) is Relation-like Function-like set

IC s is V6() V7() V8() V12() Element of NAT

s . NAT is set

SCM-Exec-Res (t,s) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

succ (IC s) is V6() V7() V8() V12() non empty V62() Element of NAT

K401((IC s),1) is V6() V7() V8() V12() Element of NAT

SCM-Chg ((SCM-Chg (s,(t address_1),((s . (t address_1)) + (s . (t address_2))))),(succ (IC s))) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

NAT .--> (succ (IC s)) is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set

{NAT} --> (succ (IC s)) is Relation-like non-empty {NAT} -defined NAT -valued {(succ (IC s))} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{(succ (IC s))}))

{(succ (IC s))} is set

K28({NAT},{(succ (IC s))}) is set

K27(K28({NAT},{(succ (IC s))})) is set

(SCM-Chg (s,(t address_1),((s . (t address_1)) + (s . (t address_2))))) +* (NAT .--> (succ (IC s))) is Relation-like Function-like set

V is Element of Segm 8

[V,{},<*R,W*>] is V21() V22() set

[V,{}] is V21() set

[[V,{}],<*R,W*>] is V21() set

(Exec ((x,R,W),s)) . NAT is set

(SCM-Chg (s,(t address_1),((s . (t address_1)) + (s . (t address_2))))) . R is set

t is Int-like Element of the carrier of (x)

(x,(Exec ((x,R,W),s)),t) is Element of the carrier of x

(x,s,t) is Element of the carrier of x

(SCM-Chg (s,(t address_1),((s . (t address_1)) + (s . (t address_2))))) . t is set

x is non empty V106() V131() V132() V133() V141() V148() V149() L14()

(x) is non empty with_non-empty_values IC-Ins-separated strict AMI-Struct over 2

the carrier of (x) is non empty set

the_Values_of (x) is Relation-like the carrier of (x) -defined Function-like V35( the carrier of (x)) set

the Object-Kind of (x) is Relation-like the carrier of (x) -defined 2 -valued Function-like quasi_total Element of K27(K28( the carrier of (x),2))

K28( the carrier of (x),2) is set

K27(K28( the carrier of (x),2)) is set

the ValuesF of (x) is Relation-like 2 -defined Function-like V35(2) set

the Object-Kind of (x) * the ValuesF of (x) is Relation-like Function-like set

0. (x) is V47((x)) Element of the carrier of (x)

the ZeroF of (x) is Element of the carrier of (x)

R is Int-like Element of the carrier of (x)

W is Int-like Element of the carrier of (x)

(x,R,W) is Element of the InstructionsF of (x)

the InstructionsF of (x) is standard-ins V71() V72() V74() set

<*R,W*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set

[3,{},<*R,W*>] is V21() V22() set

[[3,{}],<*R,W*>] is V21() set

s is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set

Exec ((x,R,W),s) is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set

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

Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))) is set

the Execution of (x) is Relation-like the InstructionsF of (x) -defined Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))) -valued Function-like quasi_total Element of K27(K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))))))

K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x)))))) is set

K27(K28( the InstructionsF of (x),(Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x))))))) is set

the Execution of (x) . (x,R,W) is Element of Funcs ((product ( the Object-Kind of (x) * the ValuesF of (x))),(product ( the Object-Kind of (x) * the ValuesF of (x))))

( the Execution of (x) . (x,R,W)) . s is set

(Exec ((x,R,W),s)) . (0. (x)) is set

IC s is V6() V7() V8() V12() Element of NAT

s . (0. (x)) is set

succ (IC s) is V6() V7() V8() V12() non empty V62() Element of NAT

K401((IC s),1) is V6() V7() V8() V12() Element of NAT

(x,(Exec ((x,R,W),s)),R) is Element of the carrier of x

the carrier of x is non empty set

(x,s,R) is Element of the carrier of x

(x,s,W) is Element of the carrier of x

(x,s,R) - (x,s,W) is Element of the carrier of x

SCM-VAL x is Relation-like 2 -defined Function-like V35(2) set

K261(NAT, the carrier of x) is set

SCM-OK * (SCM-VAL x) is Relation-like non-empty Function-like set

product (SCM-OK * (SCM-VAL x)) is functional non empty with_common_domain product-like set

SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set

{ [5,{},<*b

((({[0,{},{}]} \/ { [b

s is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

t is Element of SCM-Instr x

t address_1 is Element of K195()

s . (t address_1) is Element of the carrier of x

t address_2 is Element of K195()

s . (t address_2) is Element of the carrier of x

(s . (t address_1)) - (s . (t address_2)) is Element of the carrier of x

SCM-Chg (s,(t address_1),((s . (t address_1)) - (s . (t address_2)))) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))

(t address_1) .--> ((s . (t address_1)) - (s . (t address_2))) is Relation-like K195() -defined {(t address_1)} -defined the carrier of x -valued Function-like one-to-one set

{(t address_1)} is set

{(t address_1)} --> ((s . (t address_1)) - (s . (t address_2))) is Relation-like {(t address_1)} -defined the carrier of x -valued {((s . (t address_1)) - (s . (t address_2)))} -valued Function-like constant