:: AMI_5 semantic presentation

REAL is set
NAT is non empty V5() V17() V18() V19() non finite cardinal limit_cardinal V63() Element of K32(REAL)
K32(REAL) is set
NAT is non empty V5() V17() V18() V19() non finite cardinal limit_cardinal V63() set
K32(NAT) is non empty V5() non finite V63() set
K32(NAT) is non empty V5() non finite V63() set
9 is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real positive Element of NAT
Segm 9 is Element of K32(NAT)
SCM-Data-Loc is set
1 is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real positive Element of NAT
{1} is non empty V5() finite V28() 1 -element V62() V63() Element of K32(NAT)
K66(NAT,REAL,{1},NAT) is non empty V5() Relation-like non finite V63() Element of K32(K33(NAT,REAL))
K33(NAT,REAL) is Relation-like set
K32(K33(NAT,REAL)) is set
K198() is set
{NAT} is non empty V5() finite 1 -element V62() V63() set
{NAT} \/ SCM-Data-Loc is non empty set
K32(K198()) is set
2 is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real positive Element of NAT
K33(K198(),2) is Relation-like set
K32(K33(K198(),2)) is set
K200() is Relation-like Function-like V36(K198(),2) Element of K32(K33(K198(),2))
K201() is Relation-like 2 -defined Function-like total set
INT is set
K257(NAT,INT) is set
K200() * K201() is Relation-like Function-like set
K173((K200() * K201())) is set
SCM-Instr is non empty set
SCM-Halt is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() finite finite-yielding V28() cardinal {} -element V59() integer Function-yielding V93() V98() ext-real Element of Segm 9
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() finite finite-yielding V28() cardinal {} -element V59() integer Function-yielding V93() V98() ext-real set
[SCM-Halt,{},{}] is V1() V2() set
[SCM-Halt,{}] is V1() set
{SCM-Halt,{}} is non empty functional finite V28() set
{SCM-Halt} is non empty V5() functional finite V28() 1 -element set
{{SCM-Halt,{}},{SCM-Halt}} is non empty finite V28() V62() V63() set
[[SCM-Halt,{}],{}] is V1() set
{[SCM-Halt,{}],{}} is non empty finite set
{[SCM-Halt,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[SCM-Halt,{}],{}},{[SCM-Halt,{}]}} is non empty finite V28() V62() V63() set
{[SCM-Halt,{},{}]} is non empty V5() Relation-like finite 1 -element standard-ins V71() V72() V74() set
6 is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real positive Element of NAT
{ [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } is set
{[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } is non empty set
7 is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real positive Element of NAT
8 is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real positive Element of NAT
{7,8} is non empty finite V28() V62() V63() Element of K32(NAT)
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of SCM-Data-Loc : b₁ in {7,8} } is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of SCM-Data-Loc : b₁ in {7,8} } is non empty set
3 is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real positive Element of NAT
4 is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real positive Element of NAT
5 is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real positive Element of NAT
{1,2,3,4,5} is finite V62() Element of K32(NAT)
{ [b₁,{},K129(SCM-Data-Loc,b₂,b₃)] where b₁ is Element of Segm 9, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4,5} } is set
(({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of SCM-Data-Loc : b₁ in {7,8} } ) \/ { [b₁,{},K129(SCM-Data-Loc,b₂,b₃)] where b₁ is Element of Segm 9, b₂, b₃ is Element of SCM-Data-Loc : b₁ in {1,2,3,4,5} } is non empty set
K145(K173((K200() * K201())),K173((K200() * K201()))) is set
K33(SCM-Instr,K145(K173((K200() * K201())),K173((K200() * K201())))) is Relation-like set
K32(K33(SCM-Instr,K145(K173((K200() * K201())),K173((K200() * K201()))))) is set
SCM is non empty V81(2) IC-Ins-separated strict strict V89(2) AMI-Struct over 2
K460(NAT,K198()) is Element of K198()
K206() is Relation-like Function-like V36( SCM-Instr ,K145(K173((K200() * K201())),K173((K200() * K201())))) Element of K32(K33(SCM-Instr,K145(K173((K200() * K201())),K173((K200() * K201())))))
AMI-Struct(# K198(),K460(NAT,K198()),SCM-Instr,K200(),K201(),K206() #) is strict AMI-Struct over 2
the InstructionsF of SCM is non empty Relation-like standard-ins V71() V72() V74() set
the carrier of SCM is set
K286(2,SCM) is Relation-like non-empty the carrier of SCM -defined Function-like total set
the Object-Kind of SCM is Relation-like Function-like V36( the carrier of SCM,2) Element of K32(K33( the carrier of SCM,2))
K33( the carrier of SCM,2) is Relation-like set
K32(K33( the carrier of SCM,2)) is set
the U7 of SCM is Relation-like 2 -defined Function-like total set
the Object-Kind of SCM * the U7 of SCM is Relation-like Function-like set
COMPLEX is set
RAT is set
0 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() finite finite-yielding V28() cardinal {} -element V59() integer Function-yielding V93() V98() ext-real Element of NAT
IC is Element of the carrier of SCM
halt SCM is V88(2, SCM ) Element of the InstructionsF of SCM
[0,{},{}] is V1() V2() set
[0,{}] is V1() set
{0,{}} is non empty functional finite V28() set
{0} is non empty V5() functional finite V28() 1 -element set
{{0,{}},{0}} is non empty finite V28() V62() V63() set
[[0,{}],{}] is V1() set
{[0,{}],{}} is non empty finite set
{[0,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[0,{}],{}},{[0,{}]}} is non empty finite V28() V62() V63() set
NonZero SCM is Element of K32( the carrier of SCM)
K32( the carrier of SCM) is set
K199() is Element of K32(K198())
s1 is V61() Element of the carrier of SCM
s2 is set
x is set
[s2,x] is V1() set
{s2,x} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,x},{s2}} is non empty finite V28() V62() V63() set
s2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
dl. s2 is V61() Element of the carrier of SCM
[1,s2] is V1() set
{1,s2} is non empty finite V28() set
{1} is non empty V5() finite V28() 1 -element V62() V63() set
{{1,s2},{1}} is non empty finite V28() V62() V63() set
s1 is V61() Element of the carrier of SCM
s2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
dl. s2 is V61() Element of the carrier of SCM
[1,s2] is V1() set
{1,s2} is non empty finite V28() set
{1} is non empty V5() finite V28() 1 -element V62() V63() set
{{1,s2},{1}} is non empty finite V28() V62() V63() set
s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
s2 is V61() Element of the carrier of SCM
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
dl. x is V61() Element of the carrier of SCM
[1,x] is V1() set
{1,x} is non empty finite V28() set
{1} is non empty V5() finite V28() 1 -element V62() V63() set
{{1,x},{1}} is non empty finite V28() V62() V63() set
s1 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
proj1 s1 is set
s2 is V61() Element of the carrier of SCM
s1 is Element of NonZero SCM
s2 is Element of the carrier of SCM
s1 is Element of the InstructionsF of SCM
InsCode s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K13(s1) is set
K13(K13(s1)) is set
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is non empty set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4,5} } is set
s1 `1_3 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real set
s1 `1_3 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
[s2,<*x*>,{}] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],{}] is V1() set
{[s2,<*x*>],{}} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
s1 `1_3 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
s2 is Element of NonZero SCM
<*s2*> is Relation-like Function-like FinSequence-like FinSequence of NonZero SCM
[s2,<*x*>,<*s2*>] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],<*s2*>] is V1() set
{[s2,<*x*>],<*s2*>} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
s1 `1_3 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real set
s2 is Element of Segm 9
x is Element of NonZero SCM
s2 is Element of NonZero SCM
<*x,s2*> is set
[s2,{},<*x,s2*>] is V1() V2() set
[s2,{}] is V1() set
{s2,{}} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,{}},{s2}} is non empty finite V28() V62() V63() set
[[s2,{}],<*x,s2*>] is V1() set
{[s2,{}],<*x,s2*>} is non empty finite set
{[s2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
s1 is Element of the InstructionsF of SCM
InsCode s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K13(s1) is set
K13(K13(s1)) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
[s2,<*x*>,{}] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],{}] is V1() set
{[s2,<*x*>],{}} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4,5} } is set
s2 is Element of Segm 9
x is Element of NonZero SCM
s2 is Element of NonZero SCM
<*x,s2*> is set
[s2,{},<*x,s2*>] is V1() V2() set
[s2,{}] is V1() set
{s2,{}} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,{}},{s2}} is non empty finite V28() V62() V63() set
[[s2,{}],<*x,s2*>] is V1() set
{[s2,{}],<*x,s2*>} is non empty finite set
{[s2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is non empty set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
s2 is Element of NonZero SCM
<*s2*> is Relation-like Function-like FinSequence-like FinSequence of NonZero SCM
[s2,<*x*>,<*s2*>] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],<*s2*>] is V1() set
{[s2,<*x*>],<*s2*>} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
s1 is Element of the InstructionsF of SCM
InsCode s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K13(s1) is set
K13(K13(s1)) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
[s2,<*x*>,{}] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],{}] is V1() set
{[s2,<*x*>],{}} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
s2 is Element of NonZero SCM
<*s2*> is Relation-like Function-like FinSequence-like FinSequence of NonZero SCM
[s2,<*x*>,<*s2*>] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],<*s2*>] is V1() set
{[s2,<*x*>],<*s2*>} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode (halt SCM) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13((halt SCM)) is set
K13(K13((halt SCM))) is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is non empty set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4,5} } is set
s2 is Element of Segm 9
x is Element of NonZero SCM
s2 is Element of NonZero SCM
<*x,s2*> is set
[s2,{},<*x,s2*>] is V1() V2() set
[s2,{}] is V1() set
{s2,{}} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,{}},{s2}} is non empty finite V28() V62() V63() set
[[s2,{}],<*x,s2*>] is V1() set
{[s2,{}],<*x,s2*>} is non empty finite set
{[s2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
P1 is V61() Element of the carrier of SCM
P2 is V61() Element of the carrier of SCM
P1 := P2 is Element of the InstructionsF of SCM
<*P1,P2*> is set
[1,{},<*P1,P2*>] is V1() V2() set
[1,{}] is V1() set
{1,{}} is non empty finite V28() set
{1} is non empty V5() finite V28() 1 -element V62() V63() set
{{1,{}},{1}} is non empty finite V28() V62() V63() set
[[1,{}],<*P1,P2*>] is V1() set
{[1,{}],<*P1,P2*>} is non empty finite set
{[1,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[1,{}],<*P1,P2*>},{[1,{}]}} is non empty finite V28() V62() V63() set
s1 is Element of the InstructionsF of SCM
InsCode s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K13(s1) is set
K13(K13(s1)) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
[s2,<*x*>,{}] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],{}] is V1() set
{[s2,<*x*>],{}} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
s2 is Element of NonZero SCM
<*s2*> is Relation-like Function-like FinSequence-like FinSequence of NonZero SCM
[s2,<*x*>,<*s2*>] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],<*s2*>] is V1() set
{[s2,<*x*>],<*s2*>} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode (halt SCM) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13((halt SCM)) is set
K13(K13((halt SCM))) is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is non empty set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4,5} } is set
s2 is Element of Segm 9
x is Element of NonZero SCM
s2 is Element of NonZero SCM
<*x,s2*> is set
[s2,{},<*x,s2*>] is V1() V2() set
[s2,{}] is V1() set
{s2,{}} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,{}},{s2}} is non empty finite V28() V62() V63() set
[[s2,{}],<*x,s2*>] is V1() set
{[s2,{}],<*x,s2*>} is non empty finite set
{[s2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
P1 is V61() Element of the carrier of SCM
P2 is V61() Element of the carrier of SCM
AddTo (P1,P2) is Element of the InstructionsF of SCM
<*P1,P2*> is set
[2,{},<*P1,P2*>] is V1() V2() set
[2,{}] is V1() set
{2,{}} is non empty finite V28() set
{2} is non empty V5() finite V28() 1 -element V62() V63() set
{{2,{}},{2}} is non empty finite V28() V62() V63() set
[[2,{}],<*P1,P2*>] is V1() set
{[2,{}],<*P1,P2*>} is non empty finite set
{[2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[2,{}],<*P1,P2*>},{[2,{}]}} is non empty finite V28() V62() V63() set
s1 is Element of the InstructionsF of SCM
InsCode s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K13(s1) is set
K13(K13(s1)) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
[s2,<*x*>,{}] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],{}] is V1() set
{[s2,<*x*>],{}} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
s2 is Element of NonZero SCM
<*s2*> is Relation-like Function-like FinSequence-like FinSequence of NonZero SCM
[s2,<*x*>,<*s2*>] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],<*s2*>] is V1() set
{[s2,<*x*>],<*s2*>} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode (halt SCM) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13((halt SCM)) is set
K13(K13((halt SCM))) is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is non empty set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4,5} } is set
s2 is Element of Segm 9
x is Element of NonZero SCM
s2 is Element of NonZero SCM
<*x,s2*> is set
[s2,{},<*x,s2*>] is V1() V2() set
[s2,{}] is V1() set
{s2,{}} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,{}},{s2}} is non empty finite V28() V62() V63() set
[[s2,{}],<*x,s2*>] is V1() set
{[s2,{}],<*x,s2*>} is non empty finite set
{[s2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
P1 is V61() Element of the carrier of SCM
P2 is V61() Element of the carrier of SCM
SubFrom (P1,P2) is Element of the InstructionsF of SCM
<*P1,P2*> is set
[3,{},<*P1,P2*>] is V1() V2() set
[3,{}] is V1() set
{3,{}} is non empty finite V28() set
{3} is non empty V5() finite V28() 1 -element V62() V63() set
{{3,{}},{3}} is non empty finite V28() V62() V63() set
[[3,{}],<*P1,P2*>] is V1() set
{[3,{}],<*P1,P2*>} is non empty finite set
{[3,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[3,{}],<*P1,P2*>},{[3,{}]}} is non empty finite V28() V62() V63() set
s1 is Element of the InstructionsF of SCM
InsCode s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K13(s1) is set
K13(K13(s1)) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
[s2,<*x*>,{}] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],{}] is V1() set
{[s2,<*x*>],{}} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
s2 is Element of NonZero SCM
<*s2*> is Relation-like Function-like FinSequence-like FinSequence of NonZero SCM
[s2,<*x*>,<*s2*>] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],<*s2*>] is V1() set
{[s2,<*x*>],<*s2*>} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode (halt SCM) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13((halt SCM)) is set
K13(K13((halt SCM))) is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is non empty set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4,5} } is set
s2 is Element of Segm 9
x is Element of NonZero SCM
s2 is Element of NonZero SCM
<*x,s2*> is set
[s2,{},<*x,s2*>] is V1() V2() set
[s2,{}] is V1() set
{s2,{}} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,{}},{s2}} is non empty finite V28() V62() V63() set
[[s2,{}],<*x,s2*>] is V1() set
{[s2,{}],<*x,s2*>} is non empty finite set
{[s2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
P1 is V61() Element of the carrier of SCM
P2 is V61() Element of the carrier of SCM
MultBy (P1,P2) is Element of the InstructionsF of SCM
<*P1,P2*> is set
[4,{},<*P1,P2*>] is V1() V2() set
[4,{}] is V1() set
{4,{}} is non empty finite V28() set
{4} is non empty V5() finite V28() 1 -element V62() V63() set
{{4,{}},{4}} is non empty finite V28() V62() V63() set
[[4,{}],<*P1,P2*>] is V1() set
{[4,{}],<*P1,P2*>} is non empty finite set
{[4,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[4,{}],<*P1,P2*>},{[4,{}]}} is non empty finite V28() V62() V63() set
s1 is Element of the InstructionsF of SCM
InsCode s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K13(s1) is set
K13(K13(s1)) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
[s2,<*x*>,{}] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],{}] is V1() set
{[s2,<*x*>],{}} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
s2 is Element of NonZero SCM
<*s2*> is Relation-like Function-like FinSequence-like FinSequence of NonZero SCM
[s2,<*x*>,<*s2*>] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],<*s2*>] is V1() set
{[s2,<*x*>],<*s2*>} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode (halt SCM) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13((halt SCM)) is set
K13(K13((halt SCM))) is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is non empty set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4,5} } is set
s2 is Element of Segm 9
x is Element of NonZero SCM
s2 is Element of NonZero SCM
<*x,s2*> is set
[s2,{},<*x,s2*>] is V1() V2() set
[s2,{}] is V1() set
{s2,{}} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,{}},{s2}} is non empty finite V28() V62() V63() set
[[s2,{}],<*x,s2*>] is V1() set
{[s2,{}],<*x,s2*>} is non empty finite set
{[s2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
P1 is V61() Element of the carrier of SCM
P2 is V61() Element of the carrier of SCM
Divide (P1,P2) is Element of the InstructionsF of SCM
<*P1,P2*> is set
[5,{},<*P1,P2*>] is V1() V2() set
[5,{}] is V1() set
{5,{}} is non empty finite V28() set
{5} is non empty V5() finite V28() 1 -element V62() V63() set
{{5,{}},{5}} is non empty finite V28() V62() V63() set
[[5,{}],<*P1,P2*>] is V1() set
{[5,{}],<*P1,P2*>} is non empty finite set
{[5,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[5,{}],<*P1,P2*>},{[5,{}]}} is non empty finite V28() V62() V63() set
s1 is Element of the InstructionsF of SCM
InsCode s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K13(s1) is set
K13(K13(s1)) is set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4,5} } is set
s2 is Element of Segm 9
x is Element of NonZero SCM
s2 is Element of NonZero SCM
<*x,s2*> is set
[s2,{},<*x,s2*>] is V1() V2() set
[s2,{}] is V1() set
{s2,{}} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,{}},{s2}} is non empty finite V28() V62() V63() set
[[s2,{}],<*x,s2*>] is V1() set
{[s2,{}],<*x,s2*>} is non empty finite set
{[s2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is non empty set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
s2 is Element of NonZero SCM
<*s2*> is Relation-like Function-like FinSequence-like FinSequence of NonZero SCM
[s2,<*x*>,<*s2*>] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],<*s2*>] is V1() set
{[s2,<*x*>],<*s2*>} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode (halt SCM) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13((halt SCM)) is set
K13(K13((halt SCM))) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
[s2,<*x*>,{}] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],{}] is V1() set
{[s2,<*x*>],{}} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
s2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
SCM-goto s2 is Element of the InstructionsF of SCM
<*s2*> is Relation-like Function-like set
[6,<*s2*>,{}] is V1() V2() set
[6,<*s2*>] is V1() set
{6,<*s2*>} is non empty finite set
{6} is non empty V5() finite V28() 1 -element V62() V63() set
{{6,<*s2*>},{6}} is non empty finite V28() V62() V63() set
[[6,<*s2*>],{}] is V1() set
{[6,<*s2*>],{}} is non empty finite set
{[6,<*s2*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[6,<*s2*>],{}},{[6,<*s2*>]}} is non empty finite V28() V62() V63() set
s1 is Element of the InstructionsF of SCM
InsCode s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K13(s1) is set
K13(K13(s1)) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
[s2,<*x*>,{}] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],{}] is V1() set
{[s2,<*x*>],{}} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4,5} } is set
s2 is Element of Segm 9
x is Element of NonZero SCM
s2 is Element of NonZero SCM
<*x,s2*> is set
[s2,{},<*x,s2*>] is V1() V2() set
[s2,{}] is V1() set
{s2,{}} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,{}},{s2}} is non empty finite V28() V62() V63() set
[[s2,{}],<*x,s2*>] is V1() set
{[s2,{}],<*x,s2*>} is non empty finite set
{[s2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is non empty set
InsCode (halt SCM) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13((halt SCM)) is set
K13(K13((halt SCM))) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
s2 is Element of NonZero SCM
<*s2*> is Relation-like Function-like FinSequence-like FinSequence of NonZero SCM
[s2,<*x*>,<*s2*>] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],<*s2*>] is V1() set
{[s2,<*x*>],<*s2*>} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
P2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
P1 is V61() Element of the carrier of SCM
P1 =0_goto P2 is Element of the InstructionsF of SCM
<*P2*> is Relation-like Function-like set
<*P1*> is Relation-like Function-like set
[7,<*P2*>,<*P1*>] is V1() V2() set
[7,<*P2*>] is V1() set
{7,<*P2*>} is non empty finite set
{7} is non empty V5() finite V28() 1 -element V62() V63() set
{{7,<*P2*>},{7}} is non empty finite V28() V62() V63() set
[[7,<*P2*>],<*P1*>] is V1() set
{[7,<*P2*>],<*P1*>} is non empty finite set
{[7,<*P2*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[7,<*P2*>],<*P1*>},{[7,<*P2*>]}} is non empty finite V28() V62() V63() set
s1 is Element of the InstructionsF of SCM
InsCode s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
InsCodes the InstructionsF of SCM is non empty set
K13(s1) is set
K13(K13(s1)) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
[s2,<*x*>,{}] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],{}] is V1() set
{[s2,<*x*>],{}} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b₁,{},<*b₂,b₃*>] where b₁ is Element of Segm 9, b₂, b₃ is Element of NonZero SCM : b₁ in {1,2,3,4,5} } is set
s2 is Element of Segm 9
x is Element of NonZero SCM
s2 is Element of NonZero SCM
<*x,s2*> is set
[s2,{},<*x,s2*>] is V1() V2() set
[s2,{}] is V1() set
{s2,{}} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,{}},{s2}} is non empty finite V28() V62() V63() set
[[s2,{}],<*x,s2*>] is V1() set
{[s2,{}],<*x,s2*>} is non empty finite set
{[s2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
{ [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is set
({[SCM-Halt,{},{}]} \/ { [b₁,<*b₂*>,{}] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b₁ = 6 } ) \/ { [b₁,<*b₂*>,<*b₃*>] where b₁ is Element of Segm 9, b₂ is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b₃ is Element of NonZero SCM : b₁ in {7,8} } is non empty set
InsCode (halt SCM) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13((halt SCM)) is set
K13(K13((halt SCM))) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
<*x*> is Relation-like Function-like FinSequence-like FinSequence of NAT
s2 is Element of NonZero SCM
<*s2*> is Relation-like Function-like FinSequence-like FinSequence of NonZero SCM
[s2,<*x*>,<*s2*>] is V1() V2() set
[s2,<*x*>] is V1() set
{s2,<*x*>} is non empty finite set
{s2} is non empty V5() finite 1 -element set
{{s2,<*x*>},{s2}} is non empty finite V28() V62() V63() set
[[s2,<*x*>],<*s2*>] is V1() set
{[s2,<*x*>],<*s2*>} is non empty finite set
{[s2,<*x*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[s2,<*x*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
P2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
P1 is V61() Element of the carrier of SCM
P1 >0_goto P2 is Element of the InstructionsF of SCM
<*P2*> is Relation-like Function-like set
<*P1*> is Relation-like Function-like set
[8,<*P2*>,<*P1*>] is V1() V2() set
[8,<*P2*>] is V1() set
{8,<*P2*>} is non empty finite set
{8} is non empty V5() finite V28() 1 -element V62() V63() set
{{8,<*P2*>},{8}} is non empty finite V28() V62() V63() set
[[8,<*P2*>],<*P1*>] is V1() set
{[8,<*P2*>],<*P1*>} is non empty finite set
{[8,<*P2*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[8,<*P2*>],<*P1*>},{[8,<*P2*>]}} is non empty finite V28() V62() V63() set
s1 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
s2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Start-At (s2,SCM) is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite s2 -started set
(IC ) .--> s2 is V5() Relation-like {(IC )} -defined NAT -valued Function-like one-to-one constant finite set
{(IC )} is non empty V5() finite 1 -element set
{(IC )} --> s2 is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant finite total V36({(IC )},{s2}) Element of K32(K33({(IC )},{s2}))
{s2} is non empty V5() finite V28() 1 -element set
K33({(IC )},{s2}) is Relation-like finite set
K32(K33({(IC )},{s2})) is finite V28() set
s1 +* (Start-At (s2,SCM)) is non empty Relation-like the carrier of SCM -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible K286(2,SCM) -compatible total s2 -started set
x is V61() Element of the carrier of SCM
s1 . x is V59() integer V98() ext-real set
(s1 +* (Start-At (s2,SCM))) . x is V59() integer V98() ext-real set
proj1 s1 is set
proj1 (Start-At (s2,SCM)) is non empty finite set
(proj1 s1) \/ (proj1 (Start-At (s2,SCM))) is non empty set
s1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite non halt-free set
s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite s1 -autonomic set
DataPart s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite data-only set
s2 | (NonZero SCM) is Relation-like NonZero SCM -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
proj1 s2 is finite set
proj1 (DataPart s2) is finite set
{(IC )} is non empty V5() finite 1 -element set
(proj1 s2) /\ {(IC )} is finite set
proj1 s1 is finite set
NAT \ (proj1 s1) is Element of K32(REAL)
the Element of NAT \ (proj1 s1) is Element of NAT \ (proj1 s1)
(NonZero SCM) \ (proj1 s2) is Element of K32( the carrier of SCM)
the Element of (NonZero SCM) \ (proj1 s2) is Element of (NonZero SCM) \ (proj1 s2)
the Element of proj1 (DataPart s2) is Element of proj1 (DataPart s2)
i is V61() Element of the carrier of SCM
{i} is non empty V5() finite 1 -element set
da is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
P2 is Element of the carrier of SCM
i .--> 1 is V5() Relation-like the carrier of SCM -defined {i} -defined NAT -valued Function-like one-to-one constant K286(2,SCM) -compatible finite set
{i} --> 1 is non empty Relation-like non-empty {i} -defined NAT -valued Function-like constant finite total V36({i},{1}) Element of K32(K33({i},{1}))
{1} is non empty V5() finite V28() 1 -element V62() V63() set
K33({i},{1}) is Relation-like finite set
K32(K33({i},{1})) is finite V28() set
Start-At (da,SCM) is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite da -started set
(IC ) .--> da is V5() Relation-like {(IC )} -defined NAT -valued Function-like one-to-one constant finite set
{(IC )} --> da is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant finite total V36({(IC )},{da}) Element of K32(K33({(IC )},{da}))
{da} is non empty V5() finite V28() 1 -element set
K33({(IC )},{da}) is Relation-like finite set
K32(K33({(IC )},{da})) is finite V28() set
(i .--> 1) +* (Start-At (da,SCM)) is non empty Relation-like the carrier of SCM -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible K286(2,SCM) -compatible finite da -started set
s2 +* ((i .--> 1) +* (Start-At (da,SCM))) is non empty Relation-like the carrier of SCM -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible K286(2,SCM) -compatible finite da -started set
i .--> 0 is V5() Relation-like the carrier of SCM -defined {i} -defined NAT -valued Function-like one-to-one constant K286(2,SCM) -compatible finite Function-yielding V93() set
{i} --> 0 is non empty Relation-like {i} -defined NAT -valued Function-like constant finite total V36({i},{0}) Function-yielding V93() Element of K32(K33({i},{0}))
K33({i},{0}) is Relation-like finite set
K32(K33({i},{0})) is finite V28() set
(i .--> 0) +* (Start-At (da,SCM)) is non empty Relation-like the carrier of SCM -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible K286(2,SCM) -compatible finite da -started set
s2 +* ((i .--> 0) +* (Start-At (da,SCM))) is non empty Relation-like the carrier of SCM -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible K286(2,SCM) -compatible finite da -started set
loc is V61() Element of the carrier of SCM
loc := i is Element of the InstructionsF of SCM
<*loc,i*> is set
[1,{},<*loc,i*>] is V1() V2() set
[1,{}] is V1() set
{1,{}} is non empty finite V28() set
{{1,{}},{1}} is non empty finite V28() V62() V63() set
[[1,{}],<*loc,i*>] is V1() set
{[1,{}],<*loc,i*>} is non empty finite set
{[1,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[1,{}],<*loc,i*>},{[1,{}]}} is non empty finite V28() V62() V63() set
da .--> (loc := i) is V5() Relation-like NAT -defined {da} -defined the InstructionsF of SCM -valued Function-like one-to-one constant finite set
{da} --> (loc := i) is non empty Relation-like {da} -defined the InstructionsF of SCM -valued Function-like constant finite total V36({da},{(loc := i)}) Element of K32(K33({da},{(loc := i)}))
{(loc := i)} is non empty V5() finite 1 -element set
K33({da},{(loc := i)}) is Relation-like finite set
K32(K33({da},{(loc := i)})) is finite V28() set
s1 +* (da .--> (loc := i)) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
Cs1i is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Cs1i is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
proj1 ((i .--> 1) +* (Start-At (da,SCM))) is non empty finite set
proj1 (i .--> 1) is V5() finite set
proj1 (Start-At (da,SCM)) is non empty finite set
(proj1 (i .--> 1)) \/ (proj1 (Start-At (da,SCM))) is non empty finite set
k is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Cs1k is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Comput (Cs1k,k,1) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
proj1 (Comput (Cs1k,k,1)) is set
(Comput (Cs1k,k,1)) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
proj1 ((Comput (Cs1k,k,1)) | (proj1 s2)) is finite set
Comput (Cs1i,Cs1i,1) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
proj1 (Comput (Cs1i,Cs1i,1)) is set
(Comput (Cs1i,Cs1i,1)) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
proj1 ((Comput (Cs1i,Cs1i,1)) | (proj1 s2)) is finite set
proj1 (s2 +* ((i .--> 1) +* (Start-At (da,SCM)))) is non empty finite set
(proj1 s2) \/ (proj1 ((i .--> 1) +* (Start-At (da,SCM)))) is non empty finite set
proj1 (s1 +* (da .--> (loc := i))) is finite set
proj1 (da .--> (loc := i)) is V5() finite set
(proj1 s1) \/ (proj1 (da .--> (loc := i))) is finite set
IC k is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
k . (IC ) is set
(s2 +* ((i .--> 1) +* (Start-At (da,SCM)))) . (IC ) is set
((i .--> 1) +* (Start-At (da,SCM))) . (IC ) is set
(Start-At (da,SCM)) . (IC ) is set
k . i is V59() integer V98() ext-real set
(s2 +* ((i .--> 1) +* (Start-At (da,SCM)))) . i is set
((i .--> 1) +* (Start-At (da,SCM))) . i is set
(i .--> 1) . i is set
{da} is non empty V5() finite V28() 1 -element Element of K32(NAT)
Cs1k . da is Element of the InstructionsF of SCM
(s1 +* (da .--> (loc := i))) . da is set
(da .--> (loc := i)) . da is set
Cs1k /. (IC k) is Element of the InstructionsF of SCM
Cs1k . (IC k) is Element of the InstructionsF of SCM
0 + 1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (Cs1k,k,(0 + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (Cs1k,k,(0 + 1))) . loc is V59() integer V98() ext-real set
Comput (Cs1k,k,0) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Following (Cs1k,(Comput (Cs1k,k,0))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (Cs1k,(Comput (Cs1k,k,0))) is Element of the InstructionsF of SCM
IC (Comput (Cs1k,k,0)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (Cs1k,k,0)) . (IC ) is set
Cs1k /. (IC (Comput (Cs1k,k,0))) is Element of the InstructionsF of SCM
Exec ((CurInstr (Cs1k,(Comput (Cs1k,k,0)))),(Comput (Cs1k,k,0))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K173(( the Object-Kind of SCM * the U7 of SCM)) is set
K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) Element of K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))))
K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))))) is set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (Cs1k,(Comput (Cs1k,k,0))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (Cs1k,(Comput (Cs1k,k,0))))) . (Comput (Cs1k,k,0)) is set
(Following (Cs1k,(Comput (Cs1k,k,0)))) . loc is V59() integer V98() ext-real set
Following (Cs1k,k) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (Cs1k,k) is Element of the InstructionsF of SCM
Exec ((CurInstr (Cs1k,k)),k) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (Cs1k,k))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (Cs1k,k))) . k is set
(Following (Cs1k,k)) . loc is V59() integer V98() ext-real set
Cs2k is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Q is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
proj1 ((i .--> 0) +* (Start-At (da,SCM))) is non empty finite set
proj1 (i .--> 0) is V5() finite set
(proj1 (i .--> 0)) \/ (proj1 (Start-At (da,SCM))) is non empty finite set
(proj1 (i .--> 0)) \/ {(IC )} is non empty finite set
{i} \/ {(IC )} is non empty finite set
(proj1 s2) /\ (proj1 ((i .--> 0) +* (Start-At (da,SCM)))) is finite set
(proj1 s2) /\ {i} is finite set
((proj1 s2) /\ {i}) \/ {} is finite set
proj1 (s2 +* ((i .--> 0) +* (Start-At (da,SCM)))) is non empty finite set
(proj1 s2) \/ (proj1 ((i .--> 0) +* (Start-At (da,SCM)))) is non empty finite set
(proj1 (i .--> 1)) \/ {(IC )} is non empty finite set
(proj1 s2) /\ (proj1 ((i .--> 1) +* (Start-At (da,SCM)))) is finite set
Comput (Cs2k,Cs1i,1) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (Cs2k,Cs1i,1)) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
Comput (Q,k,1) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (Q,k,1)) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
IC Cs1i is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Cs1i . (IC ) is set
(s2 +* ((i .--> 0) +* (Start-At (da,SCM)))) . (IC ) is set
((i .--> 0) +* (Start-At (da,SCM))) . (IC ) is set
Cs1i . i is V59() integer V98() ext-real set
(s2 +* ((i .--> 0) +* (Start-At (da,SCM)))) . i is set
((i .--> 0) +* (Start-At (da,SCM))) . i is set
(i .--> 0) . i is Relation-like Function-like set
Cs1i . da is Element of the InstructionsF of SCM
Cs1i /. (IC Cs1i) is Element of the InstructionsF of SCM
Cs1i . (IC Cs1i) is Element of the InstructionsF of SCM
Comput (Cs1i,Cs1i,(0 + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (Cs1i,Cs1i,(0 + 1))) . loc is V59() integer V98() ext-real set
Comput (Cs1i,Cs1i,0) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Following (Cs1i,(Comput (Cs1i,Cs1i,0))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (Cs1i,(Comput (Cs1i,Cs1i,0))) is Element of the InstructionsF of SCM
IC (Comput (Cs1i,Cs1i,0)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (Cs1i,Cs1i,0)) . (IC ) is set
Cs1i /. (IC (Comput (Cs1i,Cs1i,0))) is Element of the InstructionsF of SCM
Exec ((CurInstr (Cs1i,(Comput (Cs1i,Cs1i,0)))),(Comput (Cs1i,Cs1i,0))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (Cs1i,(Comput (Cs1i,Cs1i,0))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (Cs1i,(Comput (Cs1i,Cs1i,0))))) . (Comput (Cs1i,Cs1i,0)) is set
(Following (Cs1i,(Comput (Cs1i,Cs1i,0)))) . loc is V59() integer V98() ext-real set
((Comput (Cs2k,Cs1i,1)) | (proj1 s2)) . loc is set
s1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite non halt-free set
proj1 s1 is finite set
s2 is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite s1 -autonomic set
x is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
s2 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
P1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (s2,x,P1) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (s2,x,P1)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (s2,x,P1)) . (IC ) is set
(IC (Comput (s2,x,P1))) + 1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
dl. 0 is V61() Element of the carrier of SCM
[1,0] is V1() set
{1,0} is non empty finite V28() set
{1} is non empty V5() finite V28() 1 -element V62() V63() set
{{1,0},{1}} is non empty finite V28() V62() V63() set
(dl. 0) := (dl. 0) is Element of the InstructionsF of SCM
<*(dl. 0),(dl. 0)*> is set
[1,{},<*(dl. 0),(dl. 0)*>] is V1() V2() set
[1,{}] is V1() set
{1,{}} is non empty finite V28() set
{{1,{}},{1}} is non empty finite V28() V62() V63() set
[[1,{}],<*(dl. 0),(dl. 0)*>] is V1() set
{[1,{}],<*(dl. 0),(dl. 0)*>} is non empty finite set
{[1,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[1,{}],<*(dl. 0),(dl. 0)*>},{[1,{}]}} is non empty finite V28() V62() V63() set
(IC (Comput (s2,x,P1))) .--> ((dl. 0) := (dl. 0)) is V5() Relation-like NAT -defined {(IC (Comput (s2,x,P1)))} -defined the InstructionsF of SCM -valued Function-like one-to-one constant finite set
{(IC (Comput (s2,x,P1)))} is non empty V5() finite V28() 1 -element set
{(IC (Comput (s2,x,P1)))} --> ((dl. 0) := (dl. 0)) is non empty Relation-like {(IC (Comput (s2,x,P1)))} -defined the InstructionsF of SCM -valued Function-like constant finite total V36({(IC (Comput (s2,x,P1)))},{((dl. 0) := (dl. 0))}) Element of K32(K33({(IC (Comput (s2,x,P1)))},{((dl. 0) := (dl. 0))}))
{((dl. 0) := (dl. 0))} is non empty V5() finite 1 -element set
K33({(IC (Comput (s2,x,P1)))},{((dl. 0) := (dl. 0))}) is Relation-like finite set
K32(K33({(IC (Comput (s2,x,P1)))},{((dl. 0) := (dl. 0))})) is finite V28() set
s1 +* ((IC (Comput (s2,x,P1))) .--> ((dl. 0) := (dl. 0))) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
(IC (Comput (s2,x,P1))) .--> (halt SCM) is V5() Relation-like NAT -defined {(IC (Comput (s2,x,P1)))} -defined the InstructionsF of SCM -valued Function-like one-to-one constant finite set
{(IC (Comput (s2,x,P1)))} --> (halt SCM) is non empty Relation-like {(IC (Comput (s2,x,P1)))} -defined the InstructionsF of SCM -valued Function-like constant finite total V36({(IC (Comput (s2,x,P1)))},{(halt SCM)}) Element of K32(K33({(IC (Comput (s2,x,P1)))},{(halt SCM)}))
{(halt SCM)} is non empty V5() finite 1 -element set
K33({(IC (Comput (s2,x,P1)))},{(halt SCM)}) is Relation-like finite set
K32(K33({(IC (Comput (s2,x,P1)))},{(halt SCM)})) is finite V28() set
s1 +* ((IC (Comput (s2,x,P1))) .--> (halt SCM)) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
s2 +* ((IC (Comput (s2,x,P1))) .--> ((dl. 0) := (dl. 0))) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
s2 +* ((IC (Comput (s2,x,P1))) .--> (halt SCM)) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
proj1 ((IC (Comput (s2,x,P1))) .--> (halt SCM)) is V5() finite set
{(IC (Comput (s2,x,P1)))} is non empty V5() finite V28() 1 -element Element of K32(NAT)
proj1 ((IC (Comput (s2,x,P1))) .--> ((dl. 0) := (dl. 0))) is V5() finite set
Cs1i1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Cs2i is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Comput (Cs2i,x,P1) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Comput (Cs1i1,x,P1) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
((IC (Comput (s2,x,P1))) .--> (halt SCM)) . (IC (Comput (s2,x,P1))) is set
Cs2i . (IC (Comput (s2,x,P1))) is Element of the InstructionsF of SCM
((IC (Comput (s2,x,P1))) .--> ((dl. 0) := (dl. 0))) . (IC (Comput (s2,x,P1))) is set
proj1 s2 is non empty finite set
(Comput (Cs1i1,x,P1)) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(Comput (s2,x,P1)) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(Comput (Cs2i,x,P1)) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
P1 + 1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
k is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (Cs1i1,x,k) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (Cs1i1,x,k)) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
Comput (Cs2i,x,k) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (Cs2i,x,k)) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
IC ((Comput (s2,x,P1)) | (proj1 s2)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
((Comput (s2,x,P1)) | (proj1 s2)) . (IC ) is set
IC (Comput (Cs1i1,x,P1)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (Cs1i1,x,P1)) . (IC ) is set
CurInstr (Cs1i1,(Comput (Cs1i1,x,P1))) is Element of the InstructionsF of SCM
Cs1i1 /. (IC (Comput (Cs1i1,x,P1))) is Element of the InstructionsF of SCM
Cs1i1 . (IC (Comput (s2,x,P1))) is Element of the InstructionsF of SCM
Following (Cs1i1,(Comput (Cs1i1,x,P1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Exec ((CurInstr (Cs1i1,(Comput (Cs1i1,x,P1)))),(Comput (Cs1i1,x,P1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K173(( the Object-Kind of SCM * the U7 of SCM)) is set
K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) Element of K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))))
K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))))) is set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (Cs1i1,(Comput (Cs1i1,x,P1))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (Cs1i1,(Comput (Cs1i1,x,P1))))) . (Comput (Cs1i1,x,P1)) is set
Exec (((dl. 0) := (dl. 0)),(Comput (Cs1i1,x,P1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 0) := (dl. 0))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 0) := (dl. 0))) . (Comput (Cs1i1,x,P1)) is set
IC (Exec (((dl. 0) := (dl. 0)),(Comput (Cs1i1,x,P1)))) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Exec (((dl. 0) := (dl. 0)),(Comput (Cs1i1,x,P1)))) . (IC ) is set
succ (IC (Comput (Cs1i1,x,P1))) is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real set
IC (Comput (Cs1i1,x,k)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (Cs1i1,x,k)) . (IC ) is set
succ (IC (Comput (s2,x,P1))) is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real set
Following (Cs2i,(Comput (Cs2i,x,P1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (Cs2i,(Comput (Cs2i,x,P1))) is Element of the InstructionsF of SCM
IC (Comput (Cs2i,x,P1)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (Cs2i,x,P1)) . (IC ) is set
Cs2i /. (IC (Comput (Cs2i,x,P1))) is Element of the InstructionsF of SCM
Exec ((CurInstr (Cs2i,(Comput (Cs2i,x,P1)))),(Comput (Cs2i,x,P1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (Cs2i,(Comput (Cs2i,x,P1))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (Cs2i,(Comput (Cs2i,x,P1))))) . (Comput (Cs2i,x,P1)) is set
Cs2i . (IC (Comput (Cs2i,x,P1))) is Element of the InstructionsF of SCM
IC (Comput (Cs2i,x,k)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (Cs2i,x,k)) . (IC ) is set
IC ((Comput (Cs1i1,x,k)) | (proj1 s2)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
((Comput (Cs1i1,x,k)) | (proj1 s2)) . (IC ) is set
IC ((Comput (Cs2i,x,k)) | (proj1 s2)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
((Comput (Cs2i,x,k)) | (proj1 s2)) . (IC ) is set
s1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite non halt-free set
s2 is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite s1 -autonomic set
proj1 s2 is non empty finite set
x is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
P1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
P2 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
i is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P1,x,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P1,(Comput (P1,x,i))) is Element of the InstructionsF of SCM
IC (Comput (P1,x,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P1,x,i)) . (IC ) is set
P1 /. (IC (Comput (P1,x,i))) is Element of the InstructionsF of SCM
Comput (P2,s2,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
da is V61() Element of the carrier of SCM
loc is V61() Element of the carrier of SCM
da := loc is Element of the InstructionsF of SCM
<*da,loc*> is set
[1,{},<*da,loc*>] is V1() V2() set
[1,{}] is V1() set
{1,{}} is non empty finite V28() set
{1} is non empty V5() finite V28() 1 -element V62() V63() set
{{1,{}},{1}} is non empty finite V28() V62() V63() set
[[1,{}],<*da,loc*>] is V1() set
{[1,{}],<*da,loc*>} is non empty finite set
{[1,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[1,{}],<*da,loc*>},{[1,{}]}} is non empty finite V28() V62() V63() set
(Comput (P1,x,i)) . loc is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . loc is V59() integer V98() ext-real set
I is Element of the InstructionsF of SCM
i + 1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K173(( the Object-Kind of SCM * the U7 of SCM)) is set
K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) Element of K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))))
K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))))) is set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P2,s2,(i + 1))) . da is V59() integer V98() ext-real set
Comput (P1,x,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (P1,x,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P1,x,(i + 1))) | (proj1 s2)) . da is set
(Comput (P1,x,(i + 1))) . da is V59() integer V98() ext-real set
(Comput (P2,s2,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P2,s2,(i + 1))) | (proj1 s2)) . da is set
Following (P1,(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,x,i)))),(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) . (Comput (P1,x,i)) is set
s1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite non halt-free set
s2 is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite s1 -autonomic set
proj1 s2 is non empty finite set
x is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
P1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
P2 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
i is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P1,x,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P1,(Comput (P1,x,i))) is Element of the InstructionsF of SCM
IC (Comput (P1,x,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P1,x,i)) . (IC ) is set
P1 /. (IC (Comput (P1,x,i))) is Element of the InstructionsF of SCM
Comput (P2,s2,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
da is V61() Element of the carrier of SCM
loc is V61() Element of the carrier of SCM
AddTo (da,loc) is Element of the InstructionsF of SCM
<*da,loc*> is set
[2,{},<*da,loc*>] is V1() V2() set
[2,{}] is V1() set
{2,{}} is non empty finite V28() set
{2} is non empty V5() finite V28() 1 -element V62() V63() set
{{2,{}},{2}} is non empty finite V28() V62() V63() set
[[2,{}],<*da,loc*>] is V1() set
{[2,{}],<*da,loc*>} is non empty finite set
{[2,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[2,{}],<*da,loc*>},{[2,{}]}} is non empty finite V28() V62() V63() set
(Comput (P1,x,i)) . da is V59() integer V98() ext-real set
(Comput (P1,x,i)) . loc is V59() integer V98() ext-real set
((Comput (P1,x,i)) . da) + ((Comput (P1,x,i)) . loc) is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . da is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . loc is V59() integer V98() ext-real set
((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . loc) is V59() integer V98() ext-real set
I is Element of the InstructionsF of SCM
i + 1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K173(( the Object-Kind of SCM * the U7 of SCM)) is set
K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) Element of K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))))
K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))))) is set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P2,s2,(i + 1))) . da is V59() integer V98() ext-real set
Comput (P1,x,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (P1,x,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P1,x,(i + 1))) | (proj1 s2)) . da is set
(Comput (P1,x,(i + 1))) . da is V59() integer V98() ext-real set
(Comput (P2,s2,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P2,s2,(i + 1))) | (proj1 s2)) . da is set
Following (P1,(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,x,i)))),(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) . (Comput (P1,x,i)) is set
s1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite non halt-free set
s2 is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite s1 -autonomic set
proj1 s2 is non empty finite set
x is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
P1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
P2 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
i is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P1,x,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P1,(Comput (P1,x,i))) is Element of the InstructionsF of SCM
IC (Comput (P1,x,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P1,x,i)) . (IC ) is set
P1 /. (IC (Comput (P1,x,i))) is Element of the InstructionsF of SCM
Comput (P2,s2,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
da is V61() Element of the carrier of SCM
loc is V61() Element of the carrier of SCM
SubFrom (da,loc) is Element of the InstructionsF of SCM
<*da,loc*> is set
[3,{},<*da,loc*>] is V1() V2() set
[3,{}] is V1() set
{3,{}} is non empty finite V28() set
{3} is non empty V5() finite V28() 1 -element V62() V63() set
{{3,{}},{3}} is non empty finite V28() V62() V63() set
[[3,{}],<*da,loc*>] is V1() set
{[3,{}],<*da,loc*>} is non empty finite set
{[3,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[3,{}],<*da,loc*>},{[3,{}]}} is non empty finite V28() V62() V63() set
(Comput (P1,x,i)) . da is V59() integer V98() ext-real set
(Comput (P1,x,i)) . loc is V59() integer V98() ext-real set
((Comput (P1,x,i)) . da) - ((Comput (P1,x,i)) . loc) is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . da is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . loc is V59() integer V98() ext-real set
((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . loc) is V59() integer V98() ext-real set
I is Element of the InstructionsF of SCM
i + 1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K173(( the Object-Kind of SCM * the U7 of SCM)) is set
K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) Element of K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))))
K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))))) is set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P2,s2,(i + 1))) . da is V59() integer V98() ext-real set
Comput (P1,x,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (P1,x,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P1,x,(i + 1))) | (proj1 s2)) . da is set
(Comput (P1,x,(i + 1))) . da is V59() integer V98() ext-real set
(Comput (P2,s2,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P2,s2,(i + 1))) | (proj1 s2)) . da is set
Following (P1,(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,x,i)))),(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) . (Comput (P1,x,i)) is set
s1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite non halt-free set
s2 is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite s1 -autonomic set
proj1 s2 is non empty finite set
x is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
P1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
P2 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
i is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P1,x,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P1,(Comput (P1,x,i))) is Element of the InstructionsF of SCM
IC (Comput (P1,x,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P1,x,i)) . (IC ) is set
P1 /. (IC (Comput (P1,x,i))) is Element of the InstructionsF of SCM
Comput (P2,s2,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
da is V61() Element of the carrier of SCM
loc is V61() Element of the carrier of SCM
MultBy (da,loc) is Element of the InstructionsF of SCM
<*da,loc*> is set
[4,{},<*da,loc*>] is V1() V2() set
[4,{}] is V1() set
{4,{}} is non empty finite V28() set
{4} is non empty V5() finite V28() 1 -element V62() V63() set
{{4,{}},{4}} is non empty finite V28() V62() V63() set
[[4,{}],<*da,loc*>] is V1() set
{[4,{}],<*da,loc*>} is non empty finite set
{[4,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[4,{}],<*da,loc*>},{[4,{}]}} is non empty finite V28() V62() V63() set
(Comput (P1,x,i)) . da is V59() integer V98() ext-real set
(Comput (P1,x,i)) . loc is V59() integer V98() ext-real set
((Comput (P1,x,i)) . da) * ((Comput (P1,x,i)) . loc) is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . da is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . loc is V59() integer V98() ext-real set
((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . loc) is V59() integer V98() ext-real set
I is Element of the InstructionsF of SCM
i + 1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K173(( the Object-Kind of SCM * the U7 of SCM)) is set
K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) Element of K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))))
K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))))) is set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P2,s2,(i + 1))) . da is V59() integer V98() ext-real set
Comput (P1,x,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (P1,x,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P1,x,(i + 1))) | (proj1 s2)) . da is set
(Comput (P1,x,(i + 1))) . da is V59() integer V98() ext-real set
(Comput (P2,s2,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P2,s2,(i + 1))) | (proj1 s2)) . da is set
Following (P1,(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,x,i)))),(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) . (Comput (P1,x,i)) is set
s1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite non halt-free set
s2 is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite s1 -autonomic set
proj1 s2 is non empty finite set
x is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
P1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
P2 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
i is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P1,x,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P1,(Comput (P1,x,i))) is Element of the InstructionsF of SCM
IC (Comput (P1,x,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P1,x,i)) . (IC ) is set
P1 /. (IC (Comput (P1,x,i))) is Element of the InstructionsF of SCM
Comput (P2,s2,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
da is V61() Element of the carrier of SCM
loc is V61() Element of the carrier of SCM
Divide (da,loc) is Element of the InstructionsF of SCM
<*da,loc*> is set
[5,{},<*da,loc*>] is V1() V2() set
[5,{}] is V1() set
{5,{}} is non empty finite V28() set
{5} is non empty V5() finite V28() 1 -element V62() V63() set
{{5,{}},{5}} is non empty finite V28() V62() V63() set
[[5,{}],<*da,loc*>] is V1() set
{[5,{}],<*da,loc*>} is non empty finite set
{[5,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[5,{}],<*da,loc*>},{[5,{}]}} is non empty finite V28() V62() V63() set
(Comput (P1,x,i)) . da is V59() integer V98() ext-real set
(Comput (P1,x,i)) . loc is V59() integer V98() ext-real set
((Comput (P1,x,i)) . da) div ((Comput (P1,x,i)) . loc) is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . da is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . loc is V59() integer V98() ext-real set
((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . loc) is V59() integer V98() ext-real set
I is Element of the InstructionsF of SCM
i + 1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K173(( the Object-Kind of SCM * the U7 of SCM)) is set
K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) Element of K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))))
K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))))) is set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P2,s2,(i + 1))) . da is V59() integer V98() ext-real set
Comput (P1,x,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (P1,x,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P1,x,(i + 1))) | (proj1 s2)) . da is set
(Comput (P1,x,(i + 1))) . da is V59() integer V98() ext-real set
(Comput (P2,s2,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P2,s2,(i + 1))) | (proj1 s2)) . da is set
Following (P1,(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,x,i)))),(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) . (Comput (P1,x,i)) is set
s1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite non halt-free set
s2 is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite s1 -autonomic set
proj1 s2 is non empty finite set
x is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
P1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
P2 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
i is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P1,x,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P1,(Comput (P1,x,i))) is Element of the InstructionsF of SCM
IC (Comput (P1,x,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P1,x,i)) . (IC ) is set
P1 /. (IC (Comput (P1,x,i))) is Element of the InstructionsF of SCM
Comput (P2,s2,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
da is V61() Element of the carrier of SCM
loc is V61() Element of the carrier of SCM
Divide (da,loc) is Element of the InstructionsF of SCM
<*da,loc*> is set
[5,{},<*da,loc*>] is V1() V2() set
[5,{}] is V1() set
{5,{}} is non empty finite V28() set
{5} is non empty V5() finite V28() 1 -element V62() V63() set
{{5,{}},{5}} is non empty finite V28() V62() V63() set
[[5,{}],<*da,loc*>] is V1() set
{[5,{}],<*da,loc*>} is non empty finite set
{[5,{}]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[5,{}],<*da,loc*>},{[5,{}]}} is non empty finite V28() V62() V63() set
(Comput (P1,x,i)) . da is V59() integer V98() ext-real set
(Comput (P1,x,i)) . loc is V59() integer V98() ext-real set
((Comput (P1,x,i)) . da) mod ((Comput (P1,x,i)) . loc) is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . da is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . loc is V59() integer V98() ext-real set
((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . loc) is V59() integer V98() ext-real set
I is Element of the InstructionsF of SCM
i + 1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P1,x,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K173(( the Object-Kind of SCM * the U7 of SCM)) is set
K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) Element of K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))))
K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))))) is set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P1,x,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P1,x,(i + 1))) | (proj1 s2)) . loc is set
(Comput (P1,x,(i + 1))) . loc is V59() integer V98() ext-real set
(Comput (P2,s2,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P2,s2,(i + 1))) | (proj1 s2)) . loc is set
(Comput (P2,s2,(i + 1))) . loc is V59() integer V98() ext-real set
Following (P1,(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,x,i)))),(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) . (Comput (P1,x,i)) is set
s1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite non halt-free set
s2 is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite s1 -autonomic set
x is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
P1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
P2 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
i is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P1,x,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P1,(Comput (P1,x,i))) is Element of the InstructionsF of SCM
IC (Comput (P1,x,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P1,x,i)) . (IC ) is set
P1 /. (IC (Comput (P1,x,i))) is Element of the InstructionsF of SCM
succ (IC (Comput (P1,x,i))) is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real set
Comput (P2,s2,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
da is V61() Element of the carrier of SCM
(Comput (P1,x,i)) . da is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . da is V59() integer V98() ext-real set
loc is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
da =0_goto loc is Element of the InstructionsF of SCM
<*loc*> is Relation-like Function-like set
<*da*> is Relation-like Function-like set
[7,<*loc*>,<*da*>] is V1() V2() set
[7,<*loc*>] is V1() set
{7,<*loc*>} is non empty finite set
{7} is non empty V5() finite V28() 1 -element V62() V63() set
{{7,<*loc*>},{7}} is non empty finite V28() V62() V63() set
[[7,<*loc*>],<*da*>] is V1() set
{[7,<*loc*>],<*da*>} is non empty finite set
{[7,<*loc*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[7,<*loc*>],<*da*>},{[7,<*loc*>]}} is non empty finite V28() V62() V63() set
I is Element of the InstructionsF of SCM
i + 1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Comput (P1,x,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Following (P1,(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,x,i)))),(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K173(( the Object-Kind of SCM * the U7 of SCM)) is set
K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) Element of K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))))
K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))))) is set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) . (Comput (P1,x,i)) is set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
proj1 s2 is non empty finite set
(Comput (P1,x,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P1,x,(i + 1))) | (proj1 s2)) . (IC ) is set
IC (Comput (P1,x,(i + 1))) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P1,x,(i + 1))) . (IC ) is set
(Comput (P2,s2,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
((Comput (P2,s2,(i + 1))) | (proj1 s2)) . (IC ) is set
IC (Comput (P2,s2,(i + 1))) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P2,s2,(i + 1))) . (IC ) is set
succ (IC (Comput (P2,s2,i))) is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real set
s1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite non halt-free set
s2 is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite s1 -autonomic set
x is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
P1 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
P2 is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
i is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P1,x,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P1,(Comput (P1,x,i))) is Element of the InstructionsF of SCM
IC (Comput (P1,x,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P1,x,i)) . (IC ) is set
P1 /. (IC (Comput (P1,x,i))) is Element of the InstructionsF of SCM
succ (IC (Comput (P1,x,i))) is non empty V17() V18() V19() V23() finite cardinal V59() integer V62() V98() ext-real set
Comput (P2,s2,i) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
da is V61() Element of the carrier of SCM
(Comput (P1,x,i)) . da is V59() integer V98() ext-real set
(Comput (P2,s2,i)) . da is V59() integer V98() ext-real set
loc is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
da >0_goto loc is Element of the InstructionsF of SCM
<*loc*> is Relation-like Function-like set
<*da*> is Relation-like Function-like set
[8,<*loc*>,<*da*>] is V1() V2() set
[8,<*loc*>] is V1() set
{8,<*loc*>} is non empty finite set
{8} is non empty V5() finite V28() 1 -element V62() V63() set
{{8,<*loc*>},{8}} is non empty finite V28() V62() V63() set
[[8,<*loc*>],<*da*>] is V1() set
{[8,<*loc*>],<*da*>} is non empty finite set
{[8,<*loc*>]} is non empty V5() Relation-like Function-like constant finite 1 -element set
{{[8,<*loc*>],<*da*>},{[8,<*loc*>]}} is non empty finite V28() V62() V63() set
I is Element of the InstructionsF of SCM
i + 1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Comput (P1,x,(i + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
proj1 s2 is non empty finite set
(Comput (P1,x,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(Comput (P2,s2,(i + 1))) | (proj1 s2) is Relation-like proj1 s2 -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
Following (P1,(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,x,i)))),(Comput (P1,x,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K173(( the Object-Kind of SCM * the U7 of SCM)) is set
K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) Element of K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))))
K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K32(K33( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))))) is set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P1,(Comput (P1,x,i))))) . (Comput (P1,x,i)) is set
((Comput (P1,x,(i + 1))) | (proj1 s2)) . (IC ) is set
IC (Comput (P1,x,(i + 1))) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P1,x,(i + 1))) . (IC ) is set
((Comput (P2,s2,(i + 1))) | (proj1 s2)) . (IC ) is set
IC (Comput (P2,s2,(i + 1))) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P2,s2,(i + 1))) . (IC ) is set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM)))
K147( the InstructionsF of SCM,K145(K173(( the Object-Kind of SCM * the U7 of SCM)),K173(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
s1 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC s1 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
s1 . (IC ) is set
s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC s2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT
s2 . (IC ) is set
proj1 s1 is set
proj1 s2 is set
DataPart s1 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible data-only set
s1 | (NonZero SCM) is Relation-like NonZero SCM -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible set
Start-At ((IC s1),SCM) is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite IC s1 -started set
(IC ) .--> (IC s1) is V5() Relation-like {(IC )} -defined NAT -valued Function-like one-to-one constant finite set
{(IC )} is non empty V5() finite 1 -element set
{(IC )} --> (IC s1) is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant finite total V36({(IC )},{(IC s1)}) Element of K32(K33({(IC )},{(IC s1)}))
{(IC s1)} is non empty V5() finite V28() 1 -element set
K33({(IC )},{(IC s1)}) is Relation-like finite set
K32(K33({(IC )},{(IC s1)})) is finite V28() set
(DataPart s1) +* (Start-At ((IC s1),SCM)) is non empty Relation-like the carrier of SCM -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible K286(2,SCM) -compatible IC s1 -started set
DataPart s2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible data-only set
s2 | (NonZero SCM) is Relation-like NonZero SCM -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible set
Start-At ((IC s2),SCM) is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite IC s2 -started set
(IC ) .--> (IC s2) is V5() Relation-like {(IC )} -defined NAT -valued Function-like one-to-one constant finite set
{(IC )} --> (IC s2) is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant finite total V36({(IC )},{(IC s2)}) Element of K32(K33({(IC )},{(IC s2)}))
{(IC s2)} is non empty V5() finite V28() 1 -element set
K33({(IC )},{(IC s2)}) is Relation-like finite set
K32(K33({(IC )},{(IC s2)})) is finite V28() set
(DataPart s2) +* (Start-At ((IC s2),SCM)) is non empty Relation-like the carrier of SCM -defined the carrier of SCM -defined Function-like K286(2,SCM) -compatible K286(2,SCM) -compatible IC s2 -started set
proj1 (DataPart s1) is set
proj1 (DataPart s2) is set
x is set
(DataPart s1) . x is set
(DataPart s2) . x is set
s1 . x is set
s2 . x is set