:: 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₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } is set
{[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } is set
{ [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } is set
({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } is set
{ [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } is set
(({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } is set
the carrier of x is non empty set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is 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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } 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 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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
[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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
[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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
[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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } 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 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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is 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 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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } 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
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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } 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 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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4} } is set
{[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4} } is set
({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } is set
{ [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of NonZero SCM : verum } is set
(({[0,{},{}]} \/ { [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 8, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4} } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of NonZero SCM : verum } is set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of NonZero SCM, b₂ is Element of the carrier of x : verum } is 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
[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₁₃ is V6() V7() V8() V12() Element of NAT
e is Int-like Element of the carrier of (x)
(x,c₁₃,e) is Element of the InstructionsF of (x)
<*c₁₃*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
<*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₁₃*>,<*e*>] is V21() V22() set
[7,<*c₁₃*>] is V21() set
[[7,<*c₁₃*>],<*e*>] is V21() set
c₁₄ is Int-like Element of the carrier of (x)
c₁₅ is Element of the carrier of x
(x,c₁₄,c₁₅) is Element of the InstructionsF of (x)
<*c₁₄,c₁₅*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set
[5,{},<*c₁₄,c₁₅*>] is V21() V22() set
[[5,{}],<*c₁₄,c₁₅*>] 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_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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is 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
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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
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
[4,{},<*R,W*>] is V21() V22() set
[[4,{}],<*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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
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 V6() V7() V8() V12() Element of NAT
(x,W) is Element of the InstructionsF of (x)
the InstructionsF of (x) is standard-ins V71() V72() V74() set
<*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 Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set
Exec ((x,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,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,W)) . s is set
(Exec ((x,W),s)) . (0. (x)) is set
(x,(Exec ((x,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
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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
f is Element of SCM-Instr x
t is Element of Segm 8
[t,<*W*>,{}] is V21() V22() set
[t,<*W*>] is V21() set
[[t,<*W*>],{}] is V21() set
f jump_address is V6() V7() V8() V12() Element of NAT
s is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
SCM-Exec-Res (f,s) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
SCM-Chg (s,(f jump_address)) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
NAT .--> (f jump_address) is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set
{NAT} --> (f jump_address) is Relation-like {NAT} -defined NAT -valued {(f jump_address)} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{(f jump_address)}))
{(f jump_address)} is set
K28({NAT},{(f jump_address)}) is set
K27(K28({NAT},{(f jump_address)})) is set
s +* (NAT .--> (f jump_address)) is Relation-like Function-like set
(Exec ((x,W),s)) . 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
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
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)
s is V6() V7() V8() V12() Element of NAT
(x,s,R) is Element of the InstructionsF of (x)
the InstructionsF of (x) is standard-ins V71() V72() V74() set
<*s*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
<*R*> 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,<*s*>,<*R*>] is V21() V22() set
[7,<*s*>] is V21() set
[[7,<*s*>],<*R*>] 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
(x,s,R) is Element of the carrier of x
Exec ((x,s,R),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,s,R) 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,s,R)) . s is set
(Exec ((x,s,R),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,s,R),s)),W) is Element of the carrier of x
(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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
f is Element of SCM-Instr x
t is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
SCM-Exec-Res (f,t) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
f cond_address is Element of K195()
t . (f cond_address) is Element of the carrier of x
f cjump_address is V6() V7() V8() V12() Element of NAT
IC t is V6() V7() V8() V12() Element of NAT
t . NAT is set
succ (IC t) is V6() V7() V8() V12() non empty V62() Element of NAT
K401((IC t),1) is V6() V7() V8() V12() Element of NAT
IFEQ ((t . (f cond_address)),(0. x),(f cjump_address),(succ (IC t))) is V6() V7() V8() V12() Element of NAT
SCM-Chg (t,(IFEQ ((t . (f cond_address)),(0. x),(f cjump_address),(succ (IC t))))) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
NAT .--> (IFEQ ((t . (f cond_address)),(0. x),(f cjump_address),(succ (IC t)))) is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set
{NAT} --> (IFEQ ((t . (f cond_address)),(0. x),(f cjump_address),(succ (IC t)))) is Relation-like {NAT} -defined NAT -valued {(IFEQ ((t . (f cond_address)),(0. x),(f cjump_address),(succ (IC t))))} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{(IFEQ ((t . (f cond_address)),(0. x),(f cjump_address),(succ (IC t))))}))
{(IFEQ ((t . (f cond_address)),(0. x),(f cjump_address),(succ (IC t))))} is set
K28({NAT},{(IFEQ ((t . (f cond_address)),(0. x),(f cjump_address),(succ (IC t))))}) is set
K27(K28({NAT},{(IFEQ ((t . (f cond_address)),(0. x),(f cjump_address),(succ (IC t))))})) is set
t +* (NAT .--> (IFEQ ((t . (f cond_address)),(0. x),(f cjump_address),(succ (IC t))))) is Relation-like Function-like set
V is Element of Segm 8
[V,<*s*>,<*R*>] is V21() V22() set
[V,<*s*>] is V21() set
[[V,<*s*>],<*R*>] is V21() set
(Exec ((x,s,R),s)) . NAT is set
(Exec ((x,s,R),s)) . NAT is set
x is non empty V106() V131() V132() V133() V141() V148() V149() L14()
the carrier of x is non empty set
(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 Element of the carrier of x
W is Int-like Element of the carrier of (x)
(x,W,R) is Element of the InstructionsF of (x)
the InstructionsF of (x) is standard-ins V71() V72() V74() set
<*W,R*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set
[5,{},<*W,R*>] is V21() V22() set
[[5,{}],<*W,R*>] 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,W,R),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,W,R) 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,W,R)) . s is set
(Exec ((x,W,R),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,W,R),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₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
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 const_address is Element of K195()
t const_value is Element of the carrier of x
SCM-Chg (s,(t const_address),(t const_value)) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
(t const_address) .--> (t const_value) is Relation-like K195() -defined {(t const_address)} -defined the carrier of x -valued Function-like one-to-one set
{(t const_address)} is set
{(t const_address)} --> (t const_value) is Relation-like {(t const_address)} -defined the carrier of x -valued {(t const_value)} -valued Function-like constant V35({(t const_address)}) quasi_total Element of K27(K28({(t const_address)},{(t const_value)}))
{(t const_value)} is set
K28({(t const_address)},{(t const_value)}) is set
K27(K28({(t const_address)},{(t const_value)})) is set
s +* ((t const_address) .--> (t const_value)) is Relation-like Function-like set
IC s is V6() V7() V8() V12() Element of NAT
s . NAT is set
V is Element of Segm 8
[V,{},<*W,R*>] is V21() V22() set
[V,{}] is V21() set
[[V,{}],<*W,R*>] is V21() 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 const_address),(t const_value))),(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 const_address),(t const_value))) +* (NAT .--> (succ (IC s))) is Relation-like Function-like set
(Exec ((x,W,R),s)) . NAT is set
(SCM-Chg (s,(t const_address),(t const_value))) . W is set
t is Int-like Element of the carrier of (x)
(x,(Exec ((x,W,R),s)),t) is Element of the carrier of x
(x,s,t) is Element of the carrier of x
(SCM-Chg (s,(t const_address),(t const_value))) . 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 InstructionsF of (x) is standard-ins V71() V72() V74() set
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 Element of the InstructionsF of (x)
W is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set
Exec (R,W) 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) . R 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) . R) . W is set
(Exec (R,W)) . (0. (x)) is set
IC W is V6() V7() V8() V12() Element of NAT
W . (0. (x)) is set
succ (IC W) is V6() V7() V8() V12() non empty V62() Element of NAT
K401((IC W),1) is V6() V7() V8() V12() Element of NAT
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
s is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
IC s is V6() V7() V8() V12() Element of NAT
s . NAT is set
s is V6() V7() V8() V12() Element of NAT
succ s is V6() V7() V8() V12() non empty V62() Element of NAT
K401(s,1) is V6() V7() V8() V12() Element of NAT
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 InstructionsF of (x) is standard-ins V71() V72() V74() set
R is Element of the InstructionsF of (x)
R `3_3 is set
W is Element of NonZero SCM
s is Element of NonZero SCM
<*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 Element of NonZero SCM
t is Element of NonZero SCM
<*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
the carrier of x is non empty 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
R `2_3 is set
K41(R) is set
K41(R) `3_3 is 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
[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
<*s*> 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,<*s*>,<*s*>] is V21() V22() set
[7,<*s*>] is V21() set
[[7,<*s*>],<*s*>] is V21() set
SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
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
s is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set
Exec (R,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) . R 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) . R) . s is 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
t is Element of NonZero SCM
f is Element of NonZero SCM
<*t,f*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set
[3,{},<*t,f*>] is V21() V22() set
[[3,{}],<*t,f*>] is V21() set
V is Element of NonZero SCM
t is Element of NonZero SCM
<*V,t*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set
[4,{},<*V,t*>] is V21() V22() set
[[4,{}],<*V,t*>] is V21() set
W 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 (W,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
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
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 Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set 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), the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ) 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)) . the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set is set
0. (x) is V47((x)) Element of the carrier of (x)
the ZeroF of (x) is Element of the carrier of (x)
(Exec ((x,R,W), the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set )) . (0. (x)) is set
IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set is V6() V7() V8() V12() Element of NAT
the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set . (0. (x)) is set
succ (IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ) is V6() V7() V8() V12() non empty V62() Element of NAT
K401((IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ),1) is V6() V7() V8() V12() Element of NAT
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
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
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 Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set 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), the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ) 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)) . the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set is set
0. (x) is V47((x)) Element of the carrier of (x)
the ZeroF of (x) is Element of the carrier of (x)
(Exec ((x,R,W), the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set )) . (0. (x)) is set
IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set is V6() V7() V8() V12() Element of NAT
the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set . (0. (x)) is set
succ (IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ) is V6() V7() V8() V12() non empty V62() Element of NAT
K401((IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ),1) is V6() V7() V8() V12() Element of NAT
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
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
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 Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set 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), the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ) 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)) . the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set is set
0. (x) is V47((x)) Element of the carrier of (x)
the ZeroF of (x) is Element of the carrier of (x)
(Exec ((x,R,W), the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set )) . (0. (x)) is set
IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set is V6() V7() V8() V12() Element of NAT
the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set . (0. (x)) is set
succ (IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ) is V6() V7() V8() V12() non empty V62() Element of NAT
K401((IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ),1) is V6() V7() V8() V12() Element of NAT
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
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
[4,{},<*R,W*>] is V21() V22() set
[[4,{}],<*R,W*>] is V21() 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 Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set 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), the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ) 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)) . the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set is set
0. (x) is V47((x)) Element of the carrier of (x)
the ZeroF of (x) is Element of the carrier of (x)
(Exec ((x,R,W), the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set )) . (0. (x)) is set
IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set is V6() V7() V8() V12() Element of NAT
the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set . (0. (x)) is set
succ (IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ) is V6() V7() V8() V12() non empty V62() Element of NAT
K401((IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ),1) is V6() V7() V8() V12() Element of NAT
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
R is V6() V7() V8() V12() Element of NAT
(x,R) is Element of the InstructionsF of (x)
the InstructionsF of (x) is standard-ins V71() V72() V74() set
<*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
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
the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
succ R is V6() V7() V8() V12() non empty V62() Element of NAT
K401(R,1) is V6() V7() V8() V12() Element of NAT
NAT .--> (succ R) is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set
{NAT} --> (succ R) is Relation-like non-empty {NAT} -defined NAT -valued {(succ R)} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{(succ R)}))
{(succ R)} is set
K28({NAT},{(succ R)}) is set
K27(K28({NAT},{(succ R)})) is set
the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) +* (NAT .--> (succ R)) is Relation-like Function-like set
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
proj1 ( the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) +* (NAT .--> (succ R))) is set
proj1 the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) is set
proj1 (NAT .--> (succ R)) is set
(proj1 the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))) \/ (proj1 (NAT .--> (succ R))) is set
SCM-Memory \/ (proj1 (NAT .--> (succ R))) is set
SCM-Memory \/ {NAT} is set
( the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) +* (NAT .--> (succ R))) . NAT is set
(NAT .--> (succ R)) . NAT is set
W is V6() V7() V8() V12() Element of NAT
succ W is V6() V7() V8() V12() non empty V62() Element of NAT
K401(W,1) is V6() V7() V8() V12() Element of NAT
proj1 (the_Values_of (x)) is set
f is set
( the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) +* (NAT .--> (succ R))) . f is set
(the_Values_of (x)) . f is set
the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) . f is set
f is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible set
proj1 f is set
V is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set
NAT .--> R is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set
{NAT} --> R is Relation-like {NAT} -defined NAT -valued {R} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{R}))
{R} is set
K28({NAT},{R}) is set
K27(K28({NAT},{R})) is set
proj1 (NAT .--> R) is set
t is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
t +* (NAT .--> R) is Relation-like Function-like set
(t +* (NAT .--> R)) . NAT is set
(NAT .--> R) . NAT is set
SCM-Instr x is non empty V19() standard-ins V71() V72() V74() set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
SCM-Chg (t,W) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
NAT .--> W is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set
{NAT} --> W is Relation-like {NAT} -defined NAT -valued {W} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{W}))
{W} is set
K28({NAT},{W}) is set
K27(K28({NAT},{W})) is set
t +* (NAT .--> W) is Relation-like Function-like set
t is Element of SCM-Instr x
t jump_address is V6() V7() V8() V12() Element of NAT
SCM-Chg (t,(t jump_address)) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
NAT .--> (t jump_address) is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set
{NAT} --> (t jump_address) is Relation-like {NAT} -defined NAT -valued {(t jump_address)} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{(t jump_address)}))
{(t jump_address)} is set
K28({NAT},{(t jump_address)}) is set
K27(K28({NAT},{(t jump_address)})) is set
t +* (NAT .--> (t jump_address)) is Relation-like Function-like set
SCM-Exec-Res (t,t) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
Exec ((x,R),V) 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) 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)) . V 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
R is Int-like Element of the carrier of (x)
W is V6() V7() V8() V12() Element of NAT
(x,W,R) is Element of the InstructionsF of (x)
the InstructionsF of (x) is standard-ins V71() V72() V74() set
<*W*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
<*R*> 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,<*W*>,<*R*>] is V21() V22() set
[7,<*W*>] is V21() set
[[7,<*W*>],<*R*>] is V21() 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
the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
succ W is V6() V7() V8() V12() non empty V62() Element of NAT
K401(W,1) is V6() V7() V8() V12() Element of NAT
NAT .--> (succ W) is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set
{NAT} --> (succ W) is Relation-like non-empty {NAT} -defined NAT -valued {(succ W)} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{(succ W)}))
{(succ W)} is set
K28({NAT},{(succ W)}) is set
K27(K28({NAT},{(succ W)})) is set
the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) +* (NAT .--> (succ W)) is Relation-like Function-like 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-Instr x is non empty V19() standard-ins V71() V72() V74() set
{ [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
((({[0,{},{}]} \/ { [b₁,{},K88(K195(),b₂,b₃)] where b₁ is Element of Segm 8, b₂, b₃ is Element of K195() : b₁ in K131(1,2,3,4) } ) \/ { [6,<*b₁*>,{}] where b₁ is V6() V7() V8() V12() Element of NAT : verum } ) \/ { [7,<*b₁*>,<*b₂*>] where b₁ is V6() V7() V8() V12() Element of NAT , b₂ is Element of K195() : verum } ) \/ { [5,{},<*b₁,b₂*>] where b₁ is Element of K195(), b₂ is Element of the carrier of x : verum } is set
proj1 ( the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) +* (NAT .--> (succ W))) is set
proj1 the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) is set
proj1 (NAT .--> (succ W)) is set
(proj1 the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))) \/ (proj1 (NAT .--> (succ W))) is set
SCM-Memory \/ (proj1 (NAT .--> (succ W))) is set
SCM-Memory \/ {NAT} is set
( the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) +* (NAT .--> (succ W))) . NAT is set
(NAT .--> (succ W)) . NAT is set
s is V6() V7() V8() V12() Element of NAT
succ s is V6() V7() V8() V12() non empty V62() Element of NAT
K401(s,1) is V6() V7() V8() V12() Element of NAT
proj1 (the_Values_of (x)) is set
t is set
( the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) +* (NAT .--> (succ W))) . t is set
(the_Values_of (x)) . t is set
the Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x)) . t is set
t is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible set
proj1 t is set
t is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set
NAT .--> W is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set
{NAT} --> W is Relation-like {NAT} -defined NAT -valued {W} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{W}))
{W} is set
K28({NAT},{W}) is set
K27(K28({NAT},{W})) is set
proj1 (NAT .--> W) is set
w is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
w +* (NAT .--> W) is Relation-like Function-like set
(w +* (NAT .--> W)) . NAT is set
(NAT .--> W) . NAT is set
V is Element of SCM-Instr x
V cond_address is Element of K195()
w . (V cond_address) is Element of the carrier of x
0. x is V47(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
IC w is V6() V7() V8() V12() Element of NAT
w . NAT is set
IC t 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)
t . (0. (x)) is set
Exec ((x,W,R),t) 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,W,R) 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,W,R)) . t is set
(Exec ((x,W,R),t)) . (0. (x)) is set
(x,t,R) is Element of the carrier of x
e is V6() V7() V8() V12() Element of NAT
succ e is V6() V7() V8() V12() non empty V62() Element of NAT
K401(e,1) is V6() V7() V8() V12() Element of NAT
V is Element of SCM-Instr x
V cond_address is Element of K195()
w . (V cond_address) is Element of the carrier of x
0. x is V47(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
SCM-Chg (w,s) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
NAT .--> s is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set
{NAT} --> s is Relation-like {NAT} -defined NAT -valued {s} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{s}))
{s} is set
K28({NAT},{s}) is set
K27(K28({NAT},{s})) is set
w +* (NAT .--> s) is Relation-like Function-like set
V cjump_address is V6() V7() V8() V12() Element of NAT
SCM-Chg (w,(V cjump_address)) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
NAT .--> (V cjump_address) is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set
{NAT} --> (V cjump_address) is Relation-like {NAT} -defined NAT -valued {(V cjump_address)} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{(V cjump_address)}))
{(V cjump_address)} is set
K28({NAT},{(V cjump_address)}) is set
K27(K28({NAT},{(V cjump_address)})) is set
w +* (NAT .--> (V cjump_address)) is Relation-like Function-like set
IC w is V6() V7() V8() V12() Element of NAT
w . NAT is set
succ (IC w) is V6() V7() V8() V12() non empty V62() Element of NAT
K401((IC w),1) is V6() V7() V8() V12() Element of NAT
IFEQ ((w . (V cond_address)),(0. x),(V cjump_address),(succ (IC w))) is V6() V7() V8() V12() Element of NAT
SCM-Chg (w,(IFEQ ((w . (V cond_address)),(0. x),(V cjump_address),(succ (IC w))))) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
NAT .--> (IFEQ ((w . (V cond_address)),(0. x),(V cjump_address),(succ (IC w)))) is Relation-like {NAT} -defined NAT -valued Function-like one-to-one set
{NAT} --> (IFEQ ((w . (V cond_address)),(0. x),(V cjump_address),(succ (IC w)))) is Relation-like {NAT} -defined NAT -valued {(IFEQ ((w . (V cond_address)),(0. x),(V cjump_address),(succ (IC w))))} -valued Function-like constant V35({NAT}) quasi_total Element of K27(K28({NAT},{(IFEQ ((w . (V cond_address)),(0. x),(V cjump_address),(succ (IC w))))}))
{(IFEQ ((w . (V cond_address)),(0. x),(V cjump_address),(succ (IC w))))} is set
K28({NAT},{(IFEQ ((w . (V cond_address)),(0. x),(V cjump_address),(succ (IC w))))}) is set
K27(K28({NAT},{(IFEQ ((w . (V cond_address)),(0. x),(V cjump_address),(succ (IC w))))})) is set
w +* (NAT .--> (IFEQ ((w . (V cond_address)),(0. x),(V cjump_address),(succ (IC w))))) is Relation-like Function-like set
SCM-Exec-Res (V,w) is Relation-like Function-like SCM-OK * (SCM-VAL x) -compatible Element of product (SCM-OK * (SCM-VAL x))
Exec ((x,W,R),t) 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,W,R) 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,W,R)) . t is set
V is Element of SCM-Instr x
V cond_address is Element of K195()
w . (V cond_address) is Element of the carrier of x
0. x is V47(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
x is non empty V106() V131() V132() V133() V141() V148() V149() L14()
the carrier of x is non empty set
(x) is non empty with_non-empty_values IC-Ins-separated strict AMI-Struct over 2
the carrier of (x) is non empty set
R is Element of the carrier of x
W is Int-like Element of the carrier of (x)
(x,W,R) is Element of the InstructionsF of (x)
the InstructionsF of (x) is standard-ins V71() V72() V74() set
<*W,R*> is Relation-like NAT -defined Function-like non empty V24() 2 -element FinSequence-like FinSubsequence-like countable set
[5,{},<*W,R*>] is V21() V22() set
[[5,{}],<*W,R*>] is V21() 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 Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set is Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set
Exec ((x,W,R), the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ) 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,W,R) 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,W,R)) . the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set is set
0. (x) is V47((x)) Element of the carrier of (x)
the ZeroF of (x) is Element of the carrier of (x)
(Exec ((x,W,R), the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set )) . (0. (x)) is set
IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set is V6() V7() V8() V12() Element of NAT
the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set . (0. (x)) is set
succ (IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ) is V6() V7() V8() V12() non empty V62() Element of NAT
K401((IC the Relation-like the carrier of (x) -defined Function-like the_Values_of (x) -compatible V35( the carrier of (x)) set ),1) is V6() V7() V8() V12() Element of NAT
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
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
(x,R,W) is Element of the InstructionsF of (x)
[2,{},<*R,W*>] is V21() V22() set
[[2,{}],<*R,W*>] is V21() set
(x,R,W) is Element of the InstructionsF of (x)
[3,{},<*R,W*>] is V21() V22() set
[[3,{}],<*R,W*>] is V21() set
(x,R,W) is Element of the InstructionsF of (x)
[4,{},<*R,W*>] is V21() V22() set
[[4,{}],<*R,W*>] is V21() 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
R is V6() V7() V8() V12() Element of NAT
(x,R) is Element of the InstructionsF of (x)
the InstructionsF of (x) is standard-ins V71() V72() V74() set
<*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 IC-Ins-separated strict AMI-Struct over 2
the carrier of (x) is non empty set
W is V6() V7() V8() V12() Element of NAT
R is Int-like Element of the carrier of (x)
(x,W,R) is Element of the InstructionsF of (x)
the InstructionsF of (x) is standard-ins V71() V72() V74() set
<*W*> is Relation-like NAT -defined NAT -valued Function-like non empty V24() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
<*R*> 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,<*W*>,<*R*>] is V21() V22() set
[7,<*W*>] is V21() set
[[7,<*W*>],<*R*>] is V21() 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 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
(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
[5,{},<*R,W*>] is V21() V22() set
[[5,{}],<*R,W*>] is V21() 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 InstructionsF of (x) is standard-ins V71() V72() V74() set
W is Element of the InstructionsF of (x)
the carrier of (x) is non empty set
s is Int-like Element of the carrier of (x)
s is Int-like Element of the carrier of (x)
(x,s,s) is non halting 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
[1,{},<*s,s*>] is V21() V22() set
[[1,{}],<*s,s*>] is V21() set
the carrier of (x) is non empty set
s is Int-like Element of the carrier of (x)
s is Int-like Element of the carrier of (x)
(x,s,s) is non halting 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
[2,{},<*s,s*>] is V21() V22() set
[[2,{}],<*s,s*>] is V21() set
the carrier of (x) is non empty set
s is Int-like Element of the carrier of (x)
s is Int-like Element of the carrier of (x)
(x,s,s) is non halting 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
[3,{},<*s,s*>] is V21() V22() set
[[3,{}],<*s,s*>] is V21() set
the carrier of (x) is non empty set
s is Int-like Element of the carrier of (x)
s is Int-like Element of the carrier of (x)
(x,s,s) is non halting 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
[4,{},<*s,s*>] is V21() V22() set
[[4,{}],<*s,s*>] is V21() set
s is V6() V7() V8() V12() Element of NAT
(x,s) is non halting 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
the carrier of (x) is non empty set
s is V6() V7() V8() V12() Element of NAT
s is Int-like Element of the carrier of (x)
(x,s,s) is non halting 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
<*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,<*s*>,<*s*>] is V21() V22() set
[7,<*s*>] is V21() set
[[7,<*s*>],<*s*>] is V21() set
the carrier of (x) is non empty set
the carrier of x is non empty set
s is Int-like Element of the carrier of (x)
s is Element of the carrier of x
(x,s,s) is non halting 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
the carrier of (x) is non empty set
the carrier of x is non empty 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
halt (x) is Element of the InstructionsF of (x)
the InstructionsF of (x) is standard-ins V71() V72() V74() set
halt the InstructionsF of (x) is Element of the InstructionsF 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 halting AMI-Struct over 2
the InstructionsF of (x) is standard-ins V71() V72() V74() set
R is Element of the InstructionsF of (x)
halt (x) is halting Element of the InstructionsF of (x)
halt the InstructionsF of (x) is Element of the InstructionsF 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 halting AMI-Struct over 2
halt (x) is halting Element of the InstructionsF of (x)
the InstructionsF of (x) is standard-ins V71() V72() V74() set
halt the InstructionsF of (x) is Element of the InstructionsF 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 halting AMI-Struct over 2
NonZero (x) is Element of K27( the carrier of (x))
the carrier of (x) is non empty set
K27( the carrier of (x)) is set
[#] (x) is non empty non proper Element of K27( the carrier of (x))
0. (x) is V47((x)) Element of the carrier of (x)
the ZeroF of (x) is Element of the carrier of (x)
{(0. (x))} is set
([#] (x)) \ {(0. (x))} is Element of K27( the carrier of (x))
{(0. (x))} is Element of K27( the carrier of (x))
SCM-Memory \ {(0. (x))} is Element of K27(SCM-Memory)
SCM-Memory \ {NAT} is Element of K27(SCM-Memory)
(NonZero SCM) \/ {NAT} is set
((NonZero SCM) \/ {NAT}) \ {NAT} is Element of K27(((NonZero SCM) \/ {NAT}))
K27(((NonZero SCM) \/ {NAT})) is set
(NonZero SCM) \ {NAT} is Element of K27( the carrier of SCM)
x is set
R is non empty V106() V131() V132() V133() V141() V148() V149() L14()
(R) is non empty with_non-empty_values IC-Ins-separated strict halting AMI-Struct over 2
the carrier of (R) is non empty set
NonZero (R) is Element of K27( the carrier of (R))
K27( the carrier of (R)) is set
[#] (R) is non empty non proper Element of K27( the carrier of (R))
0. (R) is V47((R)) Element of the carrier of (R)
the ZeroF of (R) is Element of the carrier of (R)
{(0. (R))} is set
([#] (R)) \ {(0. (R))} is Element of K27( the carrier of (R))
x is non empty V106() V131() V132() V133() V141() V148() V149() L14()
(x) is non empty with_non-empty_values IC-Ins-separated strict halting 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 IC-Ins-separated strict halting 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