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

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

K32(K33(NAT,REAL)) is set
K198() is set
is non empty V5() finite 1 -element V62() V63() set
\/ 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))

INT is set
K257(NAT,INT) is set

K173((K200() * K201())) is set
SCM-Instr is non empty set

is V1() V2() set
is V1() set
is non empty functional finite V28() set
is non empty V5() functional finite V28() 1 -element set
is non empty finite V28() V62() V63() set
is V1() set
is non empty finite set

is non empty finite V28() V62() V63() set
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
{ [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } is set
\/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 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)
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of SCM-Data-Loc : b1 in {7,8} } is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of SCM-Data-Loc : b1 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)
{ [b1,{},K129(SCM-Data-Loc,b2,b3)] where b1 is Element of Segm 9, b2, b3 is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } is set
(( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of SCM-Data-Loc : b1 in {7,8} } ) \/ { [b1,{},K129(SCM-Data-Loc,b2,b3)] where b1 is Element of Segm 9, b2, b3 is Element of SCM-Data-Loc : b1 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

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

RAT is set

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
is V1() set
is non empty functional finite V28() set
is non empty V5() functional finite V28() 1 -element set
is non empty finite V28() V62() V63() set
is V1() set
is non empty finite set

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

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
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is non empty set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 9, b2, b3 is Element of NonZero SCM : b1 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

[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*>],{}},{[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

s2 is Element 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*>],<*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,{}],<*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

[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*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 9, b2, b3 is Element of NonZero SCM : b1 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,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 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

s2 is Element 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*>],<*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

[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*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 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

s2 is Element 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*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode () is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13(()) is set
K13(K13(())) is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is non empty set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 9, b2, b3 is Element of NonZero SCM : b1 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,{}],<*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,{}],<*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

[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*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 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

s2 is Element 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*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode () is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13(()) is set
K13(K13(())) is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is non empty set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 9, b2, b3 is Element of NonZero SCM : b1 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,{}],<*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,{}],<*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

[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*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 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

s2 is Element 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*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode () is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13(()) is set
K13(K13(())) is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is non empty set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 9, b2, b3 is Element of NonZero SCM : b1 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,{}],<*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,{}],<*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

[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*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 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

s2 is Element 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*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode () is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13(()) is set
K13(K13(())) is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is non empty set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 9, b2, b3 is Element of NonZero SCM : b1 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,{}],<*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,{}],<*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

[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*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 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

s2 is Element 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*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode () is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13(()) is set
K13(K13(())) is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is non empty set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 9, b2, b3 is Element of NonZero SCM : b1 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,{}],<*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,{}],<*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
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 9, b2, b3 is Element of NonZero SCM : b1 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,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 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

s2 is Element 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*>],<*s2*>},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
InsCode () is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13(()) is set
K13(K13(())) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element 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*>],{}},{[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

[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*>],{}},{[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

[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*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 9, b2, b3 is Element of NonZero SCM : b1 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,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is non empty set
InsCode () is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13(()) is set
K13(K13(())) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT

s2 is Element 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*>],<*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

[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*>],<*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

[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*>],{}},{[s2,<*x*>]}} is non empty finite V28() V62() V63() set
{ [b1,{},<*b2,b3*>] where b1 is Element of Segm 9, b2, b3 is Element of NonZero SCM : b1 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,{}],<*x,s2*>},{[s2,{}]}} is non empty finite V28() V62() V63() set
{ [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is set
( \/ { [b1,<*b2*>,{}] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT : b1 = 6 } ) \/ { [b1,<*b2*>,<*b3*>] where b1 is Element of Segm 9, b2 is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT , b3 is Element of NonZero SCM : b1 in {7,8} } is non empty set
InsCode () is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of InsCodes the InstructionsF of SCM
K13(()) is set
K13(K13(())) is set
s2 is Element of Segm 9
x is V17() V18() V19() V23() finite cardinal V59() integer V98() ext-real Element of NAT

s2 is Element 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*>],<*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

[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*>],<*P1*>},{[8,<*P2*>]}} is non empty finite V28() V62() V63() 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

{()} is non empty V5() finite 1 -element set
{()} --> s2 is non empty Relation-like {()} -defined NAT -valued Function-like constant finite total V36({()},{s2}) Element of K32(K33({()},{s2}))
{s2} is non empty V5() finite V28() 1 -element set
K33({()},{s2}) is Relation-like finite set
K32(K33({()},{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

s2