:: 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