:: SCM_1 semantic presentation

REAL is V4() V24() set

NAT is V4() V17() V18() V19() Element of K24(REAL)

K24(REAL) is set

NAT is V4() V17() V18() V19() set

K24(NAT) is set

K24(NAT) is set

9 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

K84(9) is Element of K24(NAT)

K156() is set

K163() is set

K24(K163()) is set

2 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

K25(K163(),2) is Relation-like set

K24(K25(K163(),2)) is set

K165() is Relation-like Function-like V36(K163(),2) Element of K24(K25(K163(),2))

K166() is V4() Relation-like 2 -defined Function-like total set

K165() * K166() is Relation-like set

K138((K165() * K166())) is set

K157() is V4() set

K110(K138((K165() * K166())),K138((K165() * K166()))) is set

K25(K157(),K110(K138((K165() * K166())),K138((K165() * K166())))) is Relation-like set

K24(K25(K157(),K110(K138((K165() * K166())),K138((K165() * K166()))))) is set

SCM is V40() with_non-empty_values IC-Ins-separated strict strict V89(2) AMI-Struct over 2

the InstructionsF of SCM is V4() Relation-like V70() V71() V72() V74() set

the carrier of SCM is V4() set

the_Values_of SCM is V4() Relation-like 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 K24(K25( the carrier of SCM,2))

K25( the carrier of SCM,2) is Relation-like set

K24(K25( the carrier of SCM,2)) is set

the ValuesF of SCM is V4() Relation-like 2 -defined Function-like total set

the Object-Kind of SCM * the ValuesF of SCM is Relation-like set

COMPLEX is V4() V24() set

RAT is V4() V24() set

INT is V4() V24() set

0 is V4() Relation-like non-empty empty-yielding RAT -valued functional V17() V18() V19() V21() V22() V23() FinSequence-like FinSequence-membered V59() integer V98() ext-real non positive non negative V103() V104() V105() V106() set

1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

3 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

0 is V4() Relation-like non-empty empty-yielding RAT -valued functional V17() V18() V19() V21() V22() V23() FinSequence-like FinSequence-membered V59() integer V98() ext-real non positive non negative V103() V104() V105() V106() Element of NAT

IC is V47( SCM ) Element of the carrier of SCM

halt SCM is Element of the InstructionsF of SCM

[0,0,0] is V1() V2() set

[0,0] is V1() set

{0,0} is V4() set

{0} is V4() set

{{0,0},{0}} is V4() set

[[0,0],0] is V1() set

{[0,0],0} is V4() set

{[0,0]} is V4() Relation-like set

{{[0,0],0},{[0,0]}} is V4() set

4 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

{0} is V4() set

{0,1} is V4() set

s is V59() integer V98() ext-real set

<*s*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set

k is V59() integer V98() ext-real Element of INT

<*k*> is V4() Relation-like NAT -defined INT -valued Function-like V24() V31(1) FinSequence-like FinSubsequence-like V103() V104() V105() FinSequence of INT

s is V59() integer V98() ext-real set

<%s%> is V4() Relation-like NAT -defined Function-like V21() V24() V31(1) initial set

K284(0,s) is V5() INT -valued V103() V104() V105() set

K275({0},s) is Relation-like INT -valued Function-like V36({0},{s}) V103() V104() V105() Element of K24(K25({0},{s}))

{s} is V4() set

K25({0},{s}) is Relation-like set

K24(K25({0},{s})) is set

k is V59() integer V98() ext-real set

<%s,k%> is Relation-like NAT -defined Function-like V21() V24() V31(2) initial set

<%k%> is V4() Relation-like NAT -defined INT -valued Function-like V21() V24() V31(1) initial V103() V104() V105() set

K284(0,k) is V5() INT -valued V103() V104() V105() set

K275({0},k) is Relation-like INT -valued Function-like V36({0},{k}) V103() V104() V105() Element of K24(K25({0},{k}))

{k} is V4() set

K25({0},{k}) is Relation-like set

K24(K25({0},{k})) is set

<%s%> ^ <%k%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set

i2 is V59() integer V98() ext-real set

<%s,k,i2%> is Relation-like NAT -defined Function-like V21() V24() V31(3) initial set

<%i2%> is V4() Relation-like NAT -defined INT -valued Function-like V21() V24() V31(1) initial V103() V104() V105() set

K284(0,i2) is V5() INT -valued V103() V104() V105() set

K275({0},i2) is Relation-like INT -valued Function-like V36({0},{i2}) V103() V104() V105() Element of K24(K25({0},{i2}))

{i2} is V4() set

K25({0},{i2}) is Relation-like set

K24(K25({0},{i2})) is set

(<%s%> ^ <%k%>) ^ <%i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set

s is V59() integer V98() ext-real set

<%s,k,i2,s%> is Relation-like NAT -defined Function-like V21() V24() initial set

<%s%> is V4() Relation-like NAT -defined INT -valued Function-like V21() V24() V31(1) initial V103() V104() V105() set

K284(0,s) is V5() INT -valued V103() V104() V105() set

K275({0},s) is Relation-like INT -valued Function-like V36({0},{s}) V103() V104() V105() Element of K24(K25({0},{s}))

{s} is V4() set

K25({0},{s}) is Relation-like set

K24(K25({0},{s})) is set

((<%s%> ^ <%k%>) ^ <%i2%>) ^ <%s%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set

s is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set

len s is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

proj1 s is V17() V18() V19() V23() V59() integer V98() ext-real non negative set

k is set

s is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

dl. s is V61() Element of the carrier of SCM

[1,s] is V1() set

{1,s} is V4() set

{1} is V4() set

{{1,s},{1}} is V4() set

i2 is set

s . s is V59() integer V98() ext-real set

k is set

s1 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

dl. s1 is V61() Element of the carrier of SCM

[1,s1] is V1() set

{1,s1} is V4() set

{1} is V4() set

{{1,s1},{1}} is V4() set

i2 is set

s . s1 is V59() integer V98() ext-real set

d is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

dl. d is V61() Element of the carrier of SCM

[1,d] is V1() set

{1,d} is V4() set

{{1,d},{1}} is V4() set

s is set

s . d is V59() integer V98() ext-real set

K25( the carrier of SCM,INT) is Relation-like set

K24(K25( the carrier of SCM,INT)) is set

k is Relation-like Function-like Element of K24(K25( the carrier of SCM,INT))

proj1 k is set

i2 is set

i2 is set

k . i2 is set

(the_Values_of SCM) . i2 is set

s is Element of the carrier of SCM

Values s is set

(the_Values_of SCM) . s is set

d is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

dl. d is V61() Element of the carrier of SCM

[1,d] is V1() set

{1,d} is V4() set

{1} is V4() set

{{1,d},{1}} is V4() set

s1 is set

s . d is V59() integer V98() ext-real set

k . s is set

s1 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

dl. s1 is V61() Element of the carrier of SCM

[1,s1] is V1() set

{1,s1} is V4() set

{1} is V4() set

{{1,s1},{1}} is V4() set

s . s1 is V59() integer V98() ext-real set

the V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

i2 is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible set

the V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set +* i2 is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

s1 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

dl. s1 is V61() Element of the carrier of SCM

[1,s1] is V1() set

{1,s1} is V4() set

{1} is V4() set

{{1,s1},{1}} is V4() set

s . (dl. s1) is V59() integer V98() ext-real set

s . s1 is V59() integer V98() ext-real set

proj1 i2 is set

d is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

dl. d is V61() Element of the carrier of SCM

[1,d] is V1() set

{1,d} is V4() set

{{1,d},{1}} is V4() set

s . d is V59() integer V98() ext-real set

i2 . (dl. s1) is set

d is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

dl. d is V61() Element of the carrier of SCM

[1,d] is V1() set

{1,d} is V4() set

{{1,d},{1}} is V4() set

s . d is V59() integer V98() ext-real set

s is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set

k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

the V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total (s) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total (s)

Start-At (k,SCM) is Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible set

K284((IC ),k) is V5() INT -valued V103() V104() V105() V106() set

{(IC )} is V4() set

K275({(IC )},k) is Relation-like INT -valued Function-like V36({(IC )},{k}) V103() V104() V105() V106() Element of K24(K25({(IC )},{k}))

{k} is V4() set

K25({(IC )},{k}) is Relation-like set

K24(K25({(IC )},{k})) is set

the V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total (s) +* (Start-At (k,SCM)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

len s is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

proj1 s is V17() V18() V19() V23() V59() integer V98() ext-real non negative set

s1 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

dl. s1 is V61() Element of the carrier of SCM

[1,s1] is V1() set

{1,s1} is V4() set

{1} is V4() set

{{1,s1},{1}} is V4() set

( the V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total (s) +* (Start-At (k,SCM))) . (dl. s1) is V59() integer V98() ext-real set

s . s1 is V59() integer V98() ext-real set

proj1 (Start-At (k,SCM)) is set

the V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total (s) . (dl. s1) is V59() integer V98() ext-real set

s1 is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total (s)

IC s1 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s1 . (IC ) is set

dl. 0 is V61() Element of the carrier of SCM

[1,0] is V1() set

{1,0} is V4() set

{1} is V4() set

{{1,0},{1}} is V4() set

dl. 1 is V61() Element of the carrier of SCM

[1,1] is V1() set

{1,1} is V4() set

{{1,1},{1}} is V4() set

dl. 2 is V61() Element of the carrier of SCM

[1,2] is V1() set

{1,2} is V4() set

{{1,2},{1}} is V4() set

dl. 3 is V61() Element of the carrier of SCM

[1,3] is V1() set

{1,3} is V4() set

{{1,3},{1}} is V4() set

s is V59() integer V98() ext-real set

k is V59() integer V98() ext-real set

i2 is V59() integer V98() ext-real set

s is V59() integer V98() ext-real set

<%s,k,i2,s%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set

<%s%> is V4() Relation-like NAT -defined INT -valued Function-like V21() V24() V31(1) initial V103() V104() V105() set

K284(0,s) is V5() INT -valued V103() V104() V105() set

K275({0},s) is Relation-like INT -valued Function-like V36({0},{s}) V103() V104() V105() Element of K24(K25({0},{s}))

{s} is V4() set

K25({0},{s}) is Relation-like set

K24(K25({0},{s})) is set

<%k%> is V4() Relation-like NAT -defined INT -valued Function-like V21() V24() V31(1) initial V103() V104() V105() set

K284(0,k) is V5() INT -valued V103() V104() V105() set

K275({0},k) is Relation-like INT -valued Function-like V36({0},{k}) V103() V104() V105() Element of K24(K25({0},{k}))

{k} is V4() set

K25({0},{k}) is Relation-like set

K24(K25({0},{k})) is set

<%s%> ^ <%k%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set

<%i2%> is V4() Relation-like NAT -defined INT -valued Function-like V21() V24() V31(1) initial V103() V104() V105() set

K284(0,i2) is V5() INT -valued V103() V104() V105() set

K275({0},i2) is Relation-like INT -valued Function-like V36({0},{i2}) V103() V104() V105() Element of K24(K25({0},{i2}))

{i2} is V4() set

K25({0},{i2}) is Relation-like set

K24(K25({0},{i2})) is set

(<%s%> ^ <%k%>) ^ <%i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set

<%s%> is V4() Relation-like NAT -defined INT -valued Function-like V21() V24() V31(1) initial V103() V104() V105() set

K284(0,s) is V5() INT -valued V103() V104() V105() set

K275({0},s) is Relation-like INT -valued Function-like V36({0},{s}) V103() V104() V105() Element of K24(K25({0},{s}))

{s} is V4() set

K25({0},{s}) is Relation-like set

K24(K25({0},{s})) is set

((<%s%> ^ <%k%>) ^ <%i2%>) ^ <%s%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set

s1 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

d is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total s1 -started (<%s,k,i2,s%>)

d . (dl. 0) is V59() integer V98() ext-real set

d . (dl. 1) is V59() integer V98() ext-real set

d . (dl. 2) is V59() integer V98() ext-real set

d . (dl. 3) is V59() integer V98() ext-real set

<%s,k,i2,s%> . 2 is V59() integer V98() ext-real set

<%s,k,i2,s%> . 3 is V59() integer V98() ext-real set

len <%s,k,i2,s%> is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

proj1 <%s,k,i2,s%> is V17() V18() V19() V23() V59() integer V98() ext-real non negative set

0 + 0 is V4() Relation-like non-empty empty-yielding RAT -valued functional V17() V18() V19() V21() V22() V23() FinSequence-like FinSequence-membered V59() integer V98() ext-real non positive non negative V103() V104() V105() V106() Element of NAT

<%s,k,i2,s%> . 0 is V59() integer V98() ext-real set

<%s,k,i2,s%> . 1 is V59() integer V98() ext-real set

s is V59() integer V98() ext-real set

k is V59() integer V98() ext-real set

<%s,k%> is Relation-like NAT -defined INT -valued Function-like V21() V24() V31(2) initial V103() V104() V105() set

<%s%> is V4() Relation-like NAT -defined INT -valued Function-like V21() V24() V31(1) initial V103() V104() V105() set

K284(0,s) is V5() INT -valued V103() V104() V105() set

K275({0},s) is Relation-like INT -valued Function-like V36({0},{s}) V103() V104() V105() Element of K24(K25({0},{s}))

{s} is V4() set

K25({0},{s}) is Relation-like set

K24(K25({0},{s})) is set

<%k%> is V4() Relation-like NAT -defined INT -valued Function-like V21() V24() V31(1) initial V103() V104() V105() set

K284(0,k) is V5() INT -valued V103() V104() V105() set

K275({0},k) is Relation-like INT -valued Function-like V36({0},{k}) V103() V104() V105() Element of K24(K25({0},{k}))

{k} is V4() set

K25({0},{k}) is Relation-like set

K24(K25({0},{k})) is set

<%s%> ^ <%k%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set

i2 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total i2 -started (<%s,k%>)

s . (dl. 0) is V59() integer V98() ext-real set

s . (dl. 1) is V59() integer V98() ext-real set

len <%s,k%> is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

proj1 <%s,k%> is V17() V18() V19() V23() V59() integer V98() ext-real non negative set

<%s,k%> . 0 is V59() integer V98() ext-real set

<%s,k%> . 1 is V59() integer V98() ext-real set

s is Element of the InstructionsF of SCM

<%s%> is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(1) initial set

K284(0,s) is V5() set

K275({0},s) is Relation-like Function-like V36({0},{s}) Element of K24(K25({0},{s}))

{s} is V4() set

K25({0},{s}) is Relation-like set

K24(K25({0},{s})) is set

k is Element of the InstructionsF of SCM

<%k%> is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(1) initial set

K284(0,k) is V5() set

K275({0},k) is Relation-like Function-like V36({0},{k}) Element of K24(K25({0},{k}))

{k} is V4() set

K25({0},{k}) is Relation-like set

K24(K25({0},{k})) is set

<%s%> ^ <%k%> is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() initial set

i2 is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set

i2 . 0 is Element of the InstructionsF of SCM

i2 . 1 is Element of the InstructionsF of SCM

<%s,k%> is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(2) initial set

(<%s%> ^ <%k%>) . 1 is set

(<%s%> ^ <%k%>) . 0 is set

len (<%s%> ^ <%k%>) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

proj1 (<%s%> ^ <%k%>) is V17() V18() V19() V23() V59() integer V98() ext-real non negative set

dom (<%s%> ^ <%k%>) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of K24(NAT)

s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set

k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

k + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

i2 is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

Comput (s,i2,(k + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

Comput (s,i2,k) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

CurInstr (s,(Comput (s,i2,k))) is Element of the InstructionsF of SCM

IC (Comput (s,i2,k)) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,i2,k)) . (IC ) is set

s /. (IC (Comput (s,i2,k))) is Element of the InstructionsF of SCM

Exec ((CurInstr (s,(Comput (s,i2,k)))),(Comput (s,i2,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K138(( the Object-Kind of SCM * the ValuesF of SCM)) is set

K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))) is set

the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))) Element of K24(K25( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))))

K25( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))) is Relation-like set

K24(K25( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))))) is set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(CurInstr (s,(Comput (s,i2,k))))) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(CurInstr (s,(Comput (s,i2,k))))) . (Comput (s,i2,k)) is set

Following (s,(Comput (s,i2,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set

s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

Comput (s,s,k) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,k)) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,k)) . (IC ) is set

i2 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

k + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

Comput (s,s,(k + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

s . i2 is Element of the InstructionsF of SCM

s1 is V61() Element of the carrier of SCM

d is V61() Element of the carrier of SCM

s1 := d is Element of the InstructionsF of SCM

<*s1,d*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set

[1,0,<*s1,d*>] is V1() V2() set

[1,0] is V1() set

{1,0} is V4() set

{{1,0},{1}} is V4() set

[[1,0],<*s1,d*>] is V1() set

{[1,0],<*s1,d*>} is V4() set

{[1,0]} is V4() Relation-like set

{{[1,0],<*s1,d*>},{[1,0]}} is V4() set

AddTo (s1,d) is Element of the InstructionsF of SCM

[2,0,<*s1,d*>] is V1() V2() set

[2,0] is V1() set

{2,0} is V4() set

{2} is V4() set

{{2,0},{2}} is V4() set

[[2,0],<*s1,d*>] is V1() set

{[2,0],<*s1,d*>} is V4() set

{[2,0]} is V4() Relation-like set

{{[2,0],<*s1,d*>},{[2,0]}} is V4() set

SubFrom (s1,d) is Element of the InstructionsF of SCM

[3,0,<*s1,d*>] is V1() V2() set

[3,0] is V1() set

{3,0} is V4() set

{3} is V4() set

{{3,0},{3}} is V4() set

[[3,0],<*s1,d*>] is V1() set

{[3,0],<*s1,d*>} is V4() set

{[3,0]} is V4() Relation-like set

{{[3,0],<*s1,d*>},{[3,0]}} is V4() set

MultBy (s1,d) is Element of the InstructionsF of SCM

[4,0,<*s1,d*>] is V1() V2() set

[4,0] is V1() set

{4,0} is V4() set

{4} is V4() set

{{4,0},{4}} is V4() set

[[4,0],<*s1,d*>] is V1() set

{[4,0],<*s1,d*>} is V4() set

{[4,0]} is V4() Relation-like set

{{[4,0],<*s1,d*>},{[4,0]}} is V4() set

Divide (s1,d) is Element of the InstructionsF of SCM

5 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

[5,0,<*s1,d*>] is V1() V2() set

[5,0] is V1() set

{5,0} is V4() set

{5} is V4() set

{{5,0},{5}} is V4() set

[[5,0],<*s1,d*>] is V1() set

{[5,0],<*s1,d*>} is V4() set

{[5,0]} is V4() Relation-like set

{{[5,0],<*s1,d*>},{[5,0]}} is V4() set

proj1 s is V4() set

CurInstr (s,(Comput (s,s,k))) is Element of the InstructionsF of SCM

s /. (IC (Comput (s,s,k))) is Element of the InstructionsF of SCM

Exec ((CurInstr (s,(Comput (s,s,k)))),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K138(( the Object-Kind of SCM * the ValuesF of SCM)) is set

K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))) is set

the Execution of SCM is Relation-like Function-like V36( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))) Element of K24(K25( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))))

K25( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))) is Relation-like set

K24(K25( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))))) is set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(CurInstr (s,(Comput (s,s,k))))) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(CurInstr (s,(Comput (s,s,k))))) . (Comput (s,s,k)) is set

Exec ((s . i2),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(s . i2)) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(s . i2)) . (Comput (s,s,k)) is set

IC (Comput (s,s,(k + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,(k + 1))) . (IC ) is set

succ (IC (Comput (s,s,k))) is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative set

(IC (Comput (s,s,k))) + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

i2 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set

k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

i2 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s . i2 is Element of the InstructionsF of SCM

k + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

i2 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

Comput (s,s,k) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,k)) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,k)) . (IC ) is set

Comput (s,s,(k + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,(k + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,(k + 1))) . (IC ) is set

s1 is V61() Element of the carrier of SCM

d is V61() Element of the carrier of SCM

s1 := d is Element of the InstructionsF of SCM

<*s1,d*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set

[1,0,<*s1,d*>] is V1() V2() set

[[1,0],<*s1,d*>] is V1() set

{[1,0],<*s1,d*>} is V4() set

{{[1,0],<*s1,d*>},{[1,0]}} is V4() set

(Comput (s,s,(k + 1))) . s1 is V59() integer V98() ext-real set

(Comput (s,s,k)) . d is V59() integer V98() ext-real set

Exec ((s1 := d),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(s1 := d)) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(s1 := d)) . (Comput (s,s,k)) is set

d is V61() Element of the carrier of SCM

(Comput (s,s,(k + 1))) . d is V59() integer V98() ext-real set

(Comput (s,s,k)) . d is V59() integer V98() ext-real set

s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set

k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

i2 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s . i2 is Element of the InstructionsF of SCM

k + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

i2 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

Comput (s,s,k) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,k)) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,k)) . (IC ) is set

Comput (s,s,(k + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,(k + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,(k + 1))) . (IC ) is set

s1 is V61() Element of the carrier of SCM

d is V61() Element of the carrier of SCM

AddTo (s1,d) is Element of the InstructionsF of SCM

<*s1,d*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set

[2,0,<*s1,d*>] is V1() V2() set

[[2,0],<*s1,d*>] is V1() set

{[2,0],<*s1,d*>} is V4() set

{{[2,0],<*s1,d*>},{[2,0]}} is V4() set

(Comput (s,s,(k + 1))) . s1 is V59() integer V98() ext-real set

(Comput (s,s,k)) . s1 is V59() integer V98() ext-real set

(Comput (s,s,k)) . d is V59() integer V98() ext-real set

((Comput (s,s,k)) . s1) + ((Comput (s,s,k)) . d) is V59() integer V98() ext-real set

Exec ((AddTo (s1,d)),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(AddTo (s1,d))) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(AddTo (s1,d))) . (Comput (s,s,k)) is set

d is V61() Element of the carrier of SCM

(Comput (s,s,(k + 1))) . d is V59() integer V98() ext-real set

(Comput (s,s,k)) . d is V59() integer V98() ext-real set

s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set

k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

i2 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s . i2 is Element of the InstructionsF of SCM

k + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

i2 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

Comput (s,s,k) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,k)) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,k)) . (IC ) is set

Comput (s,s,(k + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,(k + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,(k + 1))) . (IC ) is set

s1 is V61() Element of the carrier of SCM

d is V61() Element of the carrier of SCM

SubFrom (s1,d) is Element of the InstructionsF of SCM

<*s1,d*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set

[3,0,<*s1,d*>] is V1() V2() set

[[3,0],<*s1,d*>] is V1() set

{[3,0],<*s1,d*>} is V4() set

{{[3,0],<*s1,d*>},{[3,0]}} is V4() set

(Comput (s,s,(k + 1))) . s1 is V59() integer V98() ext-real set

(Comput (s,s,k)) . s1 is V59() integer V98() ext-real set

(Comput (s,s,k)) . d is V59() integer V98() ext-real set

((Comput (s,s,k)) . s1) - ((Comput (s,s,k)) . d) is V59() integer V98() ext-real set

Exec ((SubFrom (s1,d)),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(SubFrom (s1,d))) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(SubFrom (s1,d))) . (Comput (s,s,k)) is set

d is V61() Element of the carrier of SCM

(Comput (s,s,(k + 1))) . d is V59() integer V98() ext-real set

(Comput (s,s,k)) . d is V59() integer V98() ext-real set

s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set

k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

i2 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s . i2 is Element of the InstructionsF of SCM

k + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

i2 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

Comput (s,s,k) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,k)) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,k)) . (IC ) is set

Comput (s,s,(k + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,(k + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,(k + 1))) . (IC ) is set

s1 is V61() Element of the carrier of SCM

d is V61() Element of the carrier of SCM

MultBy (s1,d) is Element of the InstructionsF of SCM

<*s1,d*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set

[4,0,<*s1,d*>] is V1() V2() set

[[4,0],<*s1,d*>] is V1() set

{[4,0],<*s1,d*>} is V4() set

{{[4,0],<*s1,d*>},{[4,0]}} is V4() set

(Comput (s,s,(k + 1))) . s1 is V59() integer V98() ext-real set

(Comput (s,s,k)) . s1 is V59() integer V98() ext-real set

(Comput (s,s,k)) . d is V59() integer V98() ext-real set

((Comput (s,s,k)) . s1) * ((Comput (s,s,k)) . d) is V59() integer V98() ext-real set

Exec ((MultBy (s1,d)),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(MultBy (s1,d))) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(MultBy (s1,d))) . (Comput (s,s,k)) is set

d is V61() Element of the carrier of SCM

(Comput (s,s,(k + 1))) . d is V59() integer V98() ext-real set

(Comput (s,s,k)) . d is V59() integer V98() ext-real set

s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set

k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

i2 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s . i2 is Element of the InstructionsF of SCM

k + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

i2 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

Comput (s,s,k) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,k)) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,k)) . (IC ) is set

Comput (s,s,(k + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,(k + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,(k + 1))) . (IC ) is set

s1 is V61() Element of the carrier of SCM

d is V61() Element of the carrier of SCM

Divide (s1,d) is Element of the InstructionsF of SCM

<*s1,d*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set

[5,0,<*s1,d*>] is V1() V2() set

[[5,0],<*s1,d*>] is V1() set

{[5,0],<*s1,d*>} is V4() set

{{[5,0],<*s1,d*>},{[5,0]}} is V4() set

(Comput (s,s,(k + 1))) . s1 is V59() integer V98() ext-real set

(Comput (s,s,k)) . s1 is V59() integer V98() ext-real set

(Comput (s,s,k)) . d is V59() integer V98() ext-real set

((Comput (s,s,k)) . s1) div ((Comput (s,s,k)) . d) is V59() integer V98() ext-real set

(Comput (s,s,(k + 1))) . d is V59() integer V98() ext-real set

((Comput (s,s,k)) . s1) mod ((Comput (s,s,k)) . d) is V59() integer V98() ext-real set

Exec ((Divide (s1,d)),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(Divide (s1,d))) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(Divide (s1,d))) . (Comput (s,s,k)) is set

d is V61() Element of the carrier of SCM

(Comput (s,s,(k + 1))) . d is V59() integer V98() ext-real set

(Comput (s,s,k)) . d is V59() integer V98() ext-real set

s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set

k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

i2 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s . i2 is Element of the InstructionsF of SCM

k + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

Comput (s,s,k) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,k)) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,k)) . (IC ) is set

Comput (s,s,(k + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,(k + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,(k + 1))) . (IC ) is set

s1 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

SCM-goto s1 is Element of the InstructionsF of SCM

6 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

<*s1*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set

[6,<*s1*>,0] is V1() V2() set

[6,<*s1*>] is V1() set

{6,<*s1*>} is V4() set

{6} is V4() set

{{6,<*s1*>},{6}} is V4() set

[[6,<*s1*>],0] is V1() set

{[6,<*s1*>],0} is V4() set

{[6,<*s1*>]} is V4() Relation-like set

{{[6,<*s1*>],0},{[6,<*s1*>]}} is V4() set

proj1 s is V4() set

CurInstr (s,(Comput (s,s,k))) is Element of the InstructionsF of SCM

s /. (IC (Comput (s,s,k))) is Element of the InstructionsF of SCM

Exec ((CurInstr (s,(Comput (s,s,k)))),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(CurInstr (s,(Comput (s,s,k))))) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(CurInstr (s,(Comput (s,s,k))))) . (Comput (s,s,k)) is set

Exec ((SCM-goto s1),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(SCM-goto s1)) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(SCM-goto s1)) . (Comput (s,s,k)) is set

csk is V61() Element of the carrier of SCM

(Comput (s,s,(k + 1))) . csk is V59() integer V98() ext-real set

(Comput (s,s,k)) . csk is V59() integer V98() ext-real set

s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set

k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

i2 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s . i2 is Element of the InstructionsF of SCM

k + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

i2 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

Comput (s,s,k) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,k)) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,k)) . (IC ) is set

Comput (s,s,(k + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,(k + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,(k + 1))) . (IC ) is set

s1 is V61() Element of the carrier of SCM

(Comput (s,s,k)) . s1 is V59() integer V98() ext-real set

d is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s1 =0_goto d is Element of the InstructionsF of SCM

7 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

<*d*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set

<*s1*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set

[7,<*d*>,<*s1*>] is V1() V2() set

[7,<*d*>] is V1() set

{7,<*d*>} is V4() set

{7} is V4() set

{{7,<*d*>},{7}} is V4() set

[[7,<*d*>],<*s1*>] is V1() set

{[7,<*d*>],<*s1*>} is V4() set

{[7,<*d*>]} is V4() Relation-like set

{{[7,<*d*>],<*s1*>},{[7,<*d*>]}} is V4() set

proj1 s is V4() set

CurInstr (s,(Comput (s,s,k))) is Element of the InstructionsF of SCM

s /. (IC (Comput (s,s,k))) is Element of the InstructionsF of SCM

Exec ((CurInstr (s,(Comput (s,s,k)))),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(CurInstr (s,(Comput (s,s,k))))) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(CurInstr (s,(Comput (s,s,k))))) . (Comput (s,s,k)) is set

Exec ((s1 =0_goto d),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(s1 =0_goto d)) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(s1 =0_goto d)) . (Comput (s,s,k)) is set

succ i2 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative set

i2 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

c

(Comput (s,s,(k + 1))) . c

(Comput (s,s,k)) . c

s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set

k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

i2 is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s . i2 is Element of the InstructionsF of SCM

k + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

i2 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

Comput (s,s,k) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,k)) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,k)) . (IC ) is set

Comput (s,s,(k + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

IC (Comput (s,s,(k + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

(Comput (s,s,(k + 1))) . (IC ) is set

s1 is V61() Element of the carrier of SCM

(Comput (s,s,k)) . s1 is V59() integer V98() ext-real set

d is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT

s1 >0_goto d is Element of the InstructionsF of SCM

8 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

<*d*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set

<*s1*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set

[8,<*d*>,<*s1*>] is V1() V2() set

[8,<*d*>] is V1() set

{8,<*d*>} is V4() set

{8} is V4() set

{{8,<*d*>},{8}} is V4() set

[[8,<*d*>],<*s1*>] is V1() set

{[8,<*d*>],<*s1*>} is V4() set

{[8,<*d*>]} is V4() Relation-like set

{{[8,<*d*>],<*s1*>},{[8,<*d*>]}} is V4() set

proj1 s is V4() set

CurInstr (s,(Comput (s,s,k))) is Element of the InstructionsF of SCM

s /. (IC (Comput (s,s,k))) is Element of the InstructionsF of SCM

Exec ((CurInstr (s,(Comput (s,s,k)))),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(CurInstr (s,(Comput (s,s,k))))) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(CurInstr (s,(Comput (s,s,k))))) . (Comput (s,s,k)) is set

Exec ((s1 >0_goto d),(Comput (s,s,k))) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(s1 >0_goto d)) is Element of K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM)))

K112( the InstructionsF of SCM,K110(K138(( the Object-Kind of SCM * the ValuesF of SCM)),K138(( the Object-Kind of SCM * the ValuesF of SCM))), the Execution of SCM,(s1 >0_goto d)) . (Comput (s,s,k)) is set

succ i2 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative set

i2 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

c

(Comput (s,s,(k + 1))) . c

(Comput (s,s,k)) . c

(halt SCM) `1_3 is V17() V18() V19() V23() V59() integer V98() ext-real non negative set

K5((halt SCM)) is set

K5(K5((halt SCM))) is set

6 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

7 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

8 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT

s is V61() Element of the carrier of SCM

k is V61() Element of the carrier of SCM

s := k is Element of the InstructionsF of SCM

<*s,k*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set

[1,0,<*s,k*>] is V1() V2() set

[[1,0],<*s,k*>] is V1() set

{[1,0],<*s,k*>} is V4() set

{{[1,0],<*s,k*>},{[1,0]}} is V4() set

(s := k) `1_3 is V17() V18() V19() V23() V59() integer V98() ext-real non negative set

K5((s := k)) is set

K5(K5((s := k))) is set

i2 is V61() Element of the carrier of SCM

s is V61() Element of the carrier of SCM

AddTo (i2,s) is Element of the InstructionsF of SCM

<*i2,s*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set

[2,0,<*i2,s*>] is V1() V2() set

[[2,0],<*i2,s*>] is V1() set

{[2,0],<*i2,s*>} is V4() set

{{[2,0],<*i2,s*>},{[2,0]}} is V4() set

(AddTo (i2,s)) `1_3 is V17() V18() V19() V23() V59() integer V98() ext-real non negative set

K5((AddTo (i2,s))) is set

K5(K5((AddTo (i2,s)))) is set

s1 is V61() Element of the carrier of SCM

d is V61() Element of the carrier of SCM

SubFrom (s1,d) is Element of the InstructionsF of SCM

<*s1,d*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set

[3,0,<*s1,d*>] is V1() V2() set

[[3,0],<*s1,d*>] is V1() set

{[3,0],<*s1,d*>} is V4() set

{{[3,0],<*s1,d*>},{[3,0]}} is V4() set

(SubFrom (s1,d)) `1_3 is V17() V18() V19() V23() V59() integer V98() ext-real non negative set

K5((SubFrom (s1,d))) is set

K5(K5((SubFrom (s1,d)))) is set

d is V61() Element of the carrier of SCM

csk is V61() Element of the carrier of SCM

MultBy (d,csk) is Element of the InstructionsF of SCM

<*d,csk*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set

[4,0,<*d,csk*>] is V1() V2() set

[[4,0],<*d,csk*>] is V1() set

{[4,0],<*d,csk*>} is V4() set

{{[4,0],<*d,csk*>},{[4,0]}} is V4() set

(MultBy (d,csk)) `1_3 is V17() V18() V19() V23() V59() integer V98() ext-real non negative set

K5((MultBy (d,csk))) is set

K5(K5((MultBy (d,csk)))) is set

c

c

Divide (c

<*c

[5,0,<*c

[[5,0],<*c

{[5,0],<*c

{{[5,0],<*c

(Divide (c

K5((Divide (c

K5(K5((Divide (c

c

SCM-goto c

<*c

[6,<*c

[6,<*c

{6,<*c

{6} is V4() set

{{6,<*c

[[6,<*c

{[6,<*c

{[6,<*c

{{[6,<*c

(SCM-goto c

K5((SCM-goto c

K5(K5((SCM-goto c

c

c

c

<*c

<*c