:: 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₉ is V61() Element of the carrier of SCM
(Comput (s,s,(k + 1))) . c₉ is V59() integer V98() ext-real set
(Comput (s,s,k)) . c₉ 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
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₉ is V61() Element of the carrier of SCM
(Comput (s,s,(k + 1))) . c₉ is V59() integer V98() ext-real set
(Comput (s,s,k)) . c₉ is V59() integer V98() ext-real set
(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<sub>9</sub> is V61() Element of the carrier of SCM
c<sub>10</sub> is V61() Element of the carrier of SCM
Divide (c<sub>9</sub>,c<sub>10</sub>) is Element of the InstructionsF of SCM
<*c<sub>9</sub>,c<sub>10</sub>*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set
[5,0,<*c<sub>9</sub>,c<sub>10</sub>*>] is V1() V2() set
[[5,0],<*c<sub>9</sub>,c<sub>10</sub>*>] is V1() set
{[5,0],<*c<sub>9</sub>,c<sub>10</sub>*>} is V4() set
{{[5,0],<*c<sub>9</sub>,c<sub>10</sub>*>},{[5,0]}} is V4() set
(Divide (c<sub>9</sub>,c<sub>10</sub>)) `1_3 is V17() V18() V19() V23() V59() integer V98() ext-real non negative set
K5((Divide (c₉,c₁₀))) is set
K5(K5((Divide (c₉,c₁₀)))) is set
c₁₁ is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
SCM-goto c₁₁ is Element of the InstructionsF of SCM
<*c₁₁*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set
[6,<*c₁₁*>,0] is V1() V2() set
[6,<*c₁₁*>] is V1() set
{6,<*c₁₁*>} is V4() set
{6} is V4() set
{{6,<*c₁₁*>},{6}} is V4() set
[[6,<*c₁₁*>],0] is V1() set
{[6,<*c₁₁*>],0} is V4() set
{[6,<*c₁₁*>]} is V4() Relation-like set
{{[6,<*c₁₁*>],0},{[6,<*c₁₁*>]}} is V4() set
(SCM-goto c₁₁) `1_3 is V17() V18() V19() V23() V59() integer V98() ext-real non negative set
K5((SCM-goto c<sub>11</sub>)) is set
K5(K5((SCM-goto c<sub>11</sub>))) is set
c<sub>13</sub> is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
c<sub>12</sub> is V61() Element of the carrier of SCM
c<sub>12</sub> =0_goto c<sub>13</sub> is Element of the InstructionsF of SCM
<*c<sub>13</sub>*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set
<*c<sub>12</sub>*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set
[7,<*c<sub>13</sub>*>,<*c<sub>12</sub>*>] is V1() V2() set
[7,<*c<sub>13</sub>*>] is V1() set
{7,<*c<sub>13</sub>*>} is V4() set
{7} is V4() set
{{7,<*c<sub>13</sub>*>},{7}} is V4() set
[[7,<*c<sub>13</sub>*>],<*c<sub>12</sub>*>] is V1() set
{[7,<*c<sub>13</sub>*>],<*c<sub>12</sub>*>} is V4() set
{[7,<*c<sub>13</sub>*>]} is V4() Relation-like set
{{[7,<*c<sub>13</sub>*>],<*c<sub>12</sub>*>},{[7,<*c<sub>13</sub>*>]}} is V4() set
(c<sub>12</sub> =0_goto c<sub>13</sub>) `1_3 is V17() V18() V19() V23() V59() integer V98() ext-real non negative set
K5((c₁₂ =0_goto c₁₃)) is set
K5(K5((c₁₂ =0_goto c₁₃))) is set
c₁₅ is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
c₁₄ is V61() Element of the carrier of SCM
c₁₄ >0_goto c₁₅ is Element of the InstructionsF of SCM
<*c₁₅*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set
<*c₁₄*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set
[8,<*c₁₅*>,<*c₁₄*>] is V1() V2() set
[8,<*c₁₅*>] is V1() set
{8,<*c₁₅*>} is V4() set
{8} is V4() set
{{8,<*c₁₅*>},{8}} is V4() set
[[8,<*c₁₅*>],<*c₁₄*>] is V1() set
{[8,<*c₁₅*>],<*c₁₄*>} is V4() set
{[8,<*c₁₅*>]} is V4() Relation-like set
{{[8,<*c₁₅*>],<*c₁₄*>},{[8,<*c₁₅*>]}} is V4() set
(c₁₄ >0_goto c₁₅) `1_3 is V17() V18() V19() V23() V59() integer V98() ext-real non negative set
K5((c₁₄ >0_goto c₁₅)) is set
K5(K5((c₁₄ >0_goto c₁₅))) is 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 V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s1 . (dl. 0) is V59() integer V98() ext-real set
s1 . (dl. 1) is V59() integer V98() ext-real set
s1 . (dl. 2) is V59() integer V98() ext-real set
s1 . (dl. 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
3 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT
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
s1 . (dl. d) is V59() integer V98() ext-real set
<%s,k,i2,s%> . d is V59() integer V98() ext-real set
<%(halt SCM)%> is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(1) initial set
K284(0,(halt SCM)) is V5() set
K275({0},(halt SCM)) is Relation-like Function-like V36({0},{(halt SCM)}) Element of K24(K25({0},{(halt SCM)}))
{(halt SCM)} is V4() set
K25({0},{(halt SCM)}) is Relation-like set
K24(K25({0},{(halt SCM)})) is set
<*> INT is V4() Relation-like non-empty empty-yielding NAT -defined INT -valued Function-like functional V17() V18() V19() V21() V22() V23() V24() FinSequence-like FinSubsequence-like FinSequence-membered V59() integer initial V98() ext-real non positive non negative V103() V104() V105() V106() FinSequence of INT
s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
k is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total 0 -started ( <*> INT)
LifeSpan (s,k) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
Result (s,k) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
dom <%(halt SCM)%> is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of K24(NAT)
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 . (0 + 0) is Element of the InstructionsF of SCM
<%(halt SCM)%> . 0 is set
Comput (s,k,0) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
IC k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
k . (IC ) is set
s . (IC k) is Element of the InstructionsF of SCM
proj1 s is V4() set
CurInstr (s,k) is Element of the InstructionsF of SCM
s /. (IC k) is Element of the InstructionsF of SCM
(dl. 0) := (dl. 1) is Element of the InstructionsF of SCM
<*(dl. 0),(dl. 1)*> is V4() Relation-like NAT -defined Function-like V24() V31(2) FinSequence-like FinSubsequence-like set
[1,0,<*(dl. 0),(dl. 1)*>] is V1() V2() set
[[1,0],<*(dl. 0),(dl. 1)*>] is V1() set
{[1,0],<*(dl. 0),(dl. 1)*>} is V4() set
{{[1,0],<*(dl. 0),(dl. 1)*>},{[1,0]}} is V4() set
<%((dl. 0) := (dl. 1))%> is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(1) initial set
K284(0,((dl. 0) := (dl. 1))) is V5() set
K275({0},((dl. 0) := (dl. 1))) is Relation-like Function-like V36({0},{((dl. 0) := (dl. 1))}) Element of K24(K25({0},{((dl. 0) := (dl. 1))}))
{((dl. 0) := (dl. 1))} is V4() set
K25({0},{((dl. 0) := (dl. 1))}) is Relation-like set
K24(K25({0},{((dl. 0) := (dl. 1))})) is set
<%((dl. 0) := (dl. 1))%> ^ <%(halt SCM)%> is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() initial set
s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
k is V59() integer V98() ext-real set
i2 is V59() integer V98() ext-real set
<%k,i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() V31(2) initial V103() V104() V105() 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
<%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
<%k%> ^ <%i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set
s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total 0 -started (<%k,i2%>)
LifeSpan (s,s) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
Result (s,s) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
(Result (s,s)) . (dl. 0) is V59() integer V98() ext-real set
0 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT
Comput (s,s,(0 + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s . (dl. 1) is V59() integer V98() ext-real set
IC s is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
s . (IC ) is set
Comput (s,s,0) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s . 0 is Element of the InstructionsF of SCM
IC (Comput (s,s,(0 + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
(Comput (s,s,(0 + 1))) . (IC ) is set
s . 1 is Element of the InstructionsF of SCM
(Comput (s,s,(0 + 1))) . (dl. 0) is V59() integer V98() ext-real set
d is V61() Element of the carrier of SCM
(Result (s,s)) . d is V59() integer V98() ext-real set
s . d is V59() integer V98() ext-real set
(Comput (s,s,(0 + 1))) . d is V59() integer V98() ext-real set
AddTo ((dl. 0),(dl. 1)) is Element of the InstructionsF of SCM
[2,0,<*(dl. 0),(dl. 1)*>] is V1() V2() set
[[2,0],<*(dl. 0),(dl. 1)*>] is V1() set
{[2,0],<*(dl. 0),(dl. 1)*>} is V4() set
{{[2,0],<*(dl. 0),(dl. 1)*>},{[2,0]}} is V4() set
<%(AddTo ((dl. 0),(dl. 1)))%> is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(1) initial set
K284(0,(AddTo ((dl. 0),(dl. 1)))) is V5() set
K275({0},(AddTo ((dl. 0),(dl. 1)))) is Relation-like Function-like V36({0},{(AddTo ((dl. 0),(dl. 1)))}) Element of K24(K25({0},{(AddTo ((dl. 0),(dl. 1)))}))
{(AddTo ((dl. 0),(dl. 1)))} is V4() set
K25({0},{(AddTo ((dl. 0),(dl. 1)))}) is Relation-like set
K24(K25({0},{(AddTo ((dl. 0),(dl. 1)))})) is set
<%(AddTo ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() initial set
s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
k is V59() integer V98() ext-real set
i2 is V59() integer V98() ext-real set
<%k,i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() V31(2) initial V103() V104() V105() 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
<%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
<%k%> ^ <%i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set
k + i2 is V59() integer V98() ext-real set
s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total 0 -started (<%k,i2%>)
LifeSpan (s,s) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
Result (s,s) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
(Result (s,s)) . (dl. 0) is V59() integer V98() ext-real set
Comput (s,s,0) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
0 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT
Comput (s,s,(0 + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s . (dl. 0) is V59() integer V98() ext-real set
s . (dl. 1) is V59() integer V98() ext-real set
IC s is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
s . (IC ) is set
s . 0 is Element of the InstructionsF of SCM
IC (Comput (s,s,(0 + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
(Comput (s,s,(0 + 1))) . (IC ) is set
s . 1 is Element of the InstructionsF of SCM
(Comput (s,s,(0 + 1))) . (dl. 0) is V59() integer V98() ext-real set
(Comput (s,s,0)) . (dl. 0) is V59() integer V98() ext-real set
(Comput (s,s,0)) . (dl. 1) is V59() integer V98() ext-real set
((Comput (s,s,0)) . (dl. 0)) + ((Comput (s,s,0)) . (dl. 1)) is V59() integer V98() ext-real set
d is V61() Element of the carrier of SCM
(Result (s,s)) . d is V59() integer V98() ext-real set
s . d is V59() integer V98() ext-real set
(Comput (s,s,(0 + 1))) . d is V59() integer V98() ext-real set
SubFrom ((dl. 0),(dl. 1)) is Element of the InstructionsF of SCM
[3,0,<*(dl. 0),(dl. 1)*>] is V1() V2() set
[[3,0],<*(dl. 0),(dl. 1)*>] is V1() set
{[3,0],<*(dl. 0),(dl. 1)*>} is V4() set
{{[3,0],<*(dl. 0),(dl. 1)*>},{[3,0]}} is V4() set
<%(SubFrom ((dl. 0),(dl. 1)))%> is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(1) initial set
K284(0,(SubFrom ((dl. 0),(dl. 1)))) is V5() set
K275({0},(SubFrom ((dl. 0),(dl. 1)))) is Relation-like Function-like V36({0},{(SubFrom ((dl. 0),(dl. 1)))}) Element of K24(K25({0},{(SubFrom ((dl. 0),(dl. 1)))}))
{(SubFrom ((dl. 0),(dl. 1)))} is V4() set
K25({0},{(SubFrom ((dl. 0),(dl. 1)))}) is Relation-like set
K24(K25({0},{(SubFrom ((dl. 0),(dl. 1)))})) is set
<%(SubFrom ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() initial set
s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
k is V59() integer V98() ext-real set
i2 is V59() integer V98() ext-real set
<%k,i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() V31(2) initial V103() V104() V105() 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
<%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
<%k%> ^ <%i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set
k - i2 is V59() integer V98() ext-real set
s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total 0 -started (<%k,i2%>)
LifeSpan (s,s) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
Result (s,s) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
(Result (s,s)) . (dl. 0) is V59() integer V98() ext-real set
Comput (s,s,0) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
0 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT
Comput (s,s,(0 + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s . (dl. 0) is V59() integer V98() ext-real set
s . (dl. 1) is V59() integer V98() ext-real set
IC s is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
s . (IC ) is set
s . 0 is Element of the InstructionsF of SCM
IC (Comput (s,s,(0 + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
(Comput (s,s,(0 + 1))) . (IC ) is set
s . 1 is Element of the InstructionsF of SCM
(Comput (s,s,(0 + 1))) . (dl. 0) is V59() integer V98() ext-real set
(Comput (s,s,0)) . (dl. 0) is V59() integer V98() ext-real set
(Comput (s,s,0)) . (dl. 1) is V59() integer V98() ext-real set
((Comput (s,s,0)) . (dl. 0)) - ((Comput (s,s,0)) . (dl. 1)) is V59() integer V98() ext-real set
d is V61() Element of the carrier of SCM
(Result (s,s)) . d is V59() integer V98() ext-real set
s . d is V59() integer V98() ext-real set
(Comput (s,s,(0 + 1))) . d is V59() integer V98() ext-real set
MultBy ((dl. 0),(dl. 1)) is Element of the InstructionsF of SCM
[4,0,<*(dl. 0),(dl. 1)*>] is V1() V2() set
[[4,0],<*(dl. 0),(dl. 1)*>] is V1() set
{[4,0],<*(dl. 0),(dl. 1)*>} is V4() set
{{[4,0],<*(dl. 0),(dl. 1)*>},{[4,0]}} is V4() set
<%(MultBy ((dl. 0),(dl. 1)))%> is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(1) initial set
K284(0,(MultBy ((dl. 0),(dl. 1)))) is V5() set
K275({0},(MultBy ((dl. 0),(dl. 1)))) is Relation-like Function-like V36({0},{(MultBy ((dl. 0),(dl. 1)))}) Element of K24(K25({0},{(MultBy ((dl. 0),(dl. 1)))}))
{(MultBy ((dl. 0),(dl. 1)))} is V4() set
K25({0},{(MultBy ((dl. 0),(dl. 1)))}) is Relation-like set
K24(K25({0},{(MultBy ((dl. 0),(dl. 1)))})) is set
<%(MultBy ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() initial set
s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
k is V59() integer V98() ext-real set
i2 is V59() integer V98() ext-real set
<%k,i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() V31(2) initial V103() V104() V105() 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
<%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
<%k%> ^ <%i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set
k * i2 is V59() integer V98() ext-real set
s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total 0 -started (<%k,i2%>)
LifeSpan (s,s) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
Result (s,s) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
(Result (s,s)) . (dl. 0) is V59() integer V98() ext-real set
Comput (s,s,0) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
0 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT
Comput (s,s,(0 + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s . (dl. 0) is V59() integer V98() ext-real set
s . (dl. 1) is V59() integer V98() ext-real set
IC s is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
s . (IC ) is set
s . 0 is Element of the InstructionsF of SCM
IC (Comput (s,s,(0 + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
(Comput (s,s,(0 + 1))) . (IC ) is set
s . 1 is Element of the InstructionsF of SCM
(Comput (s,s,(0 + 1))) . (dl. 0) is V59() integer V98() ext-real set
(Comput (s,s,0)) . (dl. 0) is V59() integer V98() ext-real set
(Comput (s,s,0)) . (dl. 1) is V59() integer V98() ext-real set
((Comput (s,s,0)) . (dl. 0)) * ((Comput (s,s,0)) . (dl. 1)) is V59() integer V98() ext-real set
d is V61() Element of the carrier of SCM
(Result (s,s)) . d is V59() integer V98() ext-real set
s . d is V59() integer V98() ext-real set
(Comput (s,s,(0 + 1))) . d is V59() integer V98() ext-real set
Divide ((dl. 0),(dl. 1)) is Element of the InstructionsF of SCM
[5,0,<*(dl. 0),(dl. 1)*>] is V1() V2() set
[[5,0],<*(dl. 0),(dl. 1)*>] is V1() set
{[5,0],<*(dl. 0),(dl. 1)*>} is V4() set
{{[5,0],<*(dl. 0),(dl. 1)*>},{[5,0]}} is V4() set
<%(Divide ((dl. 0),(dl. 1)))%> is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(1) initial set
K284(0,(Divide ((dl. 0),(dl. 1)))) is V5() set
K275({0},(Divide ((dl. 0),(dl. 1)))) is Relation-like Function-like V36({0},{(Divide ((dl. 0),(dl. 1)))}) Element of K24(K25({0},{(Divide ((dl. 0),(dl. 1)))}))
{(Divide ((dl. 0),(dl. 1)))} is V4() set
K25({0},{(Divide ((dl. 0),(dl. 1)))}) is Relation-like set
K24(K25({0},{(Divide ((dl. 0),(dl. 1)))})) is set
<%(Divide ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() initial set
s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
k is V59() integer V98() ext-real set
i2 is V59() integer V98() ext-real set
<%k,i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() V31(2) initial V103() V104() V105() 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
<%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
<%k%> ^ <%i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set
k div i2 is V59() integer V98() ext-real set
k mod i2 is V59() integer V98() ext-real set
s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total 0 -started (<%k,i2%>)
LifeSpan (s,s) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
Result (s,s) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
(Result (s,s)) . (dl. 0) is V59() integer V98() ext-real set
(Result (s,s)) . (dl. 1) is V59() integer V98() ext-real set
0 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT
Comput (s,s,(0 + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
IC s is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
s . (IC ) is set
s . 0 is Element of the InstructionsF of SCM
s . (dl. 0) is V59() integer V98() ext-real set
s . (dl. 1) is V59() integer V98() ext-real set
Comput (s,s,0) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s . 1 is Element of the InstructionsF of SCM
IC (Comput (s,s,(0 + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
(Comput (s,s,(0 + 1))) . (IC ) is set
s . (IC (Comput (s,s,(0 + 1)))) is Element of the InstructionsF of SCM
(Comput (s,s,(0 + 1))) . (dl. 0) is V59() integer V98() ext-real set
(Comput (s,s,(0 + 1))) . (dl. 1) is V59() integer V98() ext-real set
d is V61() Element of the carrier of SCM
(Result (s,s)) . d is V59() integer V98() ext-real set
s . d is V59() integer V98() ext-real set
(Comput (s,s,(0 + 1))) . d is V59() integer V98() ext-real set
SCM-goto 1 is Element of the InstructionsF of SCM
<*1*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set
[6,<*1*>,0] is V1() V2() set
[6,<*1*>] is V1() set
{6,<*1*>} is V4() set
{6} is V4() set
{{6,<*1*>},{6}} is V4() set
[[6,<*1*>],0] is V1() set
{[6,<*1*>],0} is V4() set
{[6,<*1*>]} is V4() Relation-like set
{{[6,<*1*>],0},{[6,<*1*>]}} is V4() set
<%(SCM-goto 1)%> is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(1) initial set
K284(0,(SCM-goto 1)) is V5() set
K275({0},(SCM-goto 1)) is Relation-like Function-like V36({0},{(SCM-goto 1)}) Element of K24(K25({0},{(SCM-goto 1)}))
{(SCM-goto 1)} is V4() set
K25({0},{(SCM-goto 1)}) is Relation-like set
K24(K25({0},{(SCM-goto 1)})) is set
<%(SCM-goto 1)%> ^ <%(halt SCM)%> is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() initial set
s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
k is V59() integer V98() ext-real set
i2 is V59() integer V98() ext-real set
<%k,i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() V31(2) initial V103() V104() V105() 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
<%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
<%k%> ^ <%i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set
s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total 0 -started (<%k,i2%>)
LifeSpan (s,s) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
Result (s,s) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
0 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT
Comput (s,s,(0 + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
IC s is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
s . (IC ) is set
Comput (s,s,0) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s . 0 is Element of the InstructionsF of SCM
IC (Comput (s,s,(0 + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
(Comput (s,s,(0 + 1))) . (IC ) is set
s . 1 is Element of the InstructionsF of SCM
d is V61() Element of the carrier of SCM
(Result (s,s)) . d is V59() integer V98() ext-real set
s . d is V59() integer V98() ext-real set
(Comput (s,s,(0 + 1))) . d is V59() integer V98() ext-real set
(dl. 0) =0_goto 1 is Element of the InstructionsF of SCM
<*(dl. 0)*> is V4() Relation-like NAT -defined Function-like V24() V31(1) FinSequence-like FinSubsequence-like set
[7,<*1*>,<*(dl. 0)*>] is V1() V2() set
[7,<*1*>] is V1() set
{7,<*1*>} is V4() set
{7} is V4() set
{{7,<*1*>},{7}} is V4() set
[[7,<*1*>],<*(dl. 0)*>] is V1() set
{[7,<*1*>],<*(dl. 0)*>} is V4() set
{[7,<*1*>]} is V4() Relation-like set
{{[7,<*1*>],<*(dl. 0)*>},{[7,<*1*>]}} is V4() set
<%((dl. 0) =0_goto 1)%> is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(1) initial set
K284(0,((dl. 0) =0_goto 1)) is V5() set
K275({0},((dl. 0) =0_goto 1)) is Relation-like Function-like V36({0},{((dl. 0) =0_goto 1)}) Element of K24(K25({0},{((dl. 0) =0_goto 1)}))
{((dl. 0) =0_goto 1)} is V4() set
K25({0},{((dl. 0) =0_goto 1)}) is Relation-like set
K24(K25({0},{((dl. 0) =0_goto 1)})) is set
<%((dl. 0) =0_goto 1)%> ^ <%(halt SCM)%> is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() initial set
s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
k is V59() integer V98() ext-real set
i2 is V59() integer V98() ext-real set
<%k,i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() V31(2) initial V103() V104() V105() 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
<%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
<%k%> ^ <%i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set
s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total 0 -started (<%k,i2%>)
LifeSpan (s,s) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
Result (s,s) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
0 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT
Comput (s,s,(0 + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s . 0 is Element of the InstructionsF of SCM
s . 1 is Element of the InstructionsF of SCM
IC s is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
s . (IC ) is set
Comput (s,s,0) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s . (dl. 0) is V59() integer V98() ext-real set
IC (Comput (s,s,(0 + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
(Comput (s,s,(0 + 1))) . (IC ) is set
d is V61() Element of the carrier of SCM
(Result (s,s)) . d is V59() integer V98() ext-real set
s . d is V59() integer V98() ext-real set
(Comput (s,s,(0 + 1))) . d is V59() integer V98() ext-real set
(dl. 0) >0_goto 1 is Element of the InstructionsF of SCM
[8,<*1*>,<*(dl. 0)*>] is V1() V2() set
[8,<*1*>] is V1() set
{8,<*1*>} is V4() set
{8} is V4() set
{{8,<*1*>},{8}} is V4() set
[[8,<*1*>],<*(dl. 0)*>] is V1() set
{[8,<*1*>],<*(dl. 0)*>} is V4() set
{[8,<*1*>]} is V4() Relation-like set
{{[8,<*1*>],<*(dl. 0)*>},{[8,<*1*>]}} is V4() set
<%((dl. 0) >0_goto 1)%> is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() V31(1) initial set
K284(0,((dl. 0) >0_goto 1)) is V5() set
K275({0},((dl. 0) >0_goto 1)) is Relation-like Function-like V36({0},{((dl. 0) >0_goto 1)}) Element of K24(K25({0},{((dl. 0) >0_goto 1)}))
{((dl. 0) >0_goto 1)} is V4() set
K25({0},{((dl. 0) >0_goto 1)}) is Relation-like set
K24(K25({0},{((dl. 0) >0_goto 1)})) is set
<%((dl. 0) >0_goto 1)%> ^ <%(halt SCM)%> is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like V21() V24() initial set
s is V4() Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
k is V59() integer V98() ext-real set
i2 is V59() integer V98() ext-real set
<%k,i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() V31(2) initial V103() V104() V105() 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
<%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
<%k%> ^ <%i2%> is Relation-like NAT -defined INT -valued Function-like V21() V24() initial V103() V104() V105() set
s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total 0 -started (<%k,i2%>)
LifeSpan (s,s) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
Result (s,s) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
0 + 1 is V4() V17() V18() V19() V23() V59() integer V62() V98() ext-real positive non negative Element of NAT
Comput (s,s,(0 + 1)) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s . 0 is Element of the InstructionsF of SCM
s . 1 is Element of the InstructionsF of SCM
IC s is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
s . (IC ) is set
Comput (s,s,0) is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
s . (dl. 0) is V59() integer V98() ext-real set
IC (Comput (s,s,(0 + 1))) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
(Comput (s,s,(0 + 1))) . (IC ) is set
d is V61() Element of the carrier of SCM
(Result (s,s)) . d is V59() integer V98() ext-real set
s . d is V59() integer V98() ext-real set
(Comput (s,s,(0 + 1))) . d is V59() integer V98() ext-real set
s is V4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total set
len (<*> INT) is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
proj1 (<*> INT) 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
k is V17() V18() V19() V23() V59() integer V98() ext-real non negative Element of NAT
dl. k is V61() Element of the carrier of SCM
[1,k] is V1() set
{1,k} is V4() set
{{1,k},{1}} is V4() set
s . (dl. k) is V59() integer V98() ext-real set
(<*> INT) . k is V17() V18() V19() V23() V59() integer V98() ext-real non negative set