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

{[SCM-Halt,{},{}]} \/ { [b

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

({[SCM-Halt,{},{}]} \/ { [b

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

(({[SCM-Halt,{},{}]} \/ { [b

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

({[SCM-Halt,{},{}]} \/ { [b

{ [b

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

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

({[SCM-Halt,{},{}]} \/ { [b

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

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

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

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

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

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

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

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

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

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

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

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

({[SCM-Halt,{},{}]} \/ { [b

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

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

({[SCM-Halt,{},{}]} \/ { [b

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

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

({[SCM-Halt,{},{}]} \/ { [b

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