REAL is non empty V35() set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V35() set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
K19(NAT) is set
9 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
Segm 9 is Element of K19(NAT)
K174() is set
SCM-Memory is set
K19(SCM-Memory) is set
2 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
K20(SCM-Memory,2) is Relation-like set
K19(K20(SCM-Memory,2)) is set
SCM-OK is Relation-like Function-like V32( SCM-Memory ,2) Element of K19(K20(SCM-Memory,2))
SCM-VAL is Relation-like 2 -defined Function-like total set
SCM-OK (#) SCM-VAL is Relation-like Function-like set
K163((SCM-OK (#) SCM-VAL)) is set
K175() is non empty set
K143(K163((SCM-OK (#) SCM-VAL)),K163((SCM-OK (#) SCM-VAL))) is set
K20(K175(),K143(K163((SCM-OK (#) SCM-VAL)),K163((SCM-OK (#) SCM-VAL)))) is Relation-like set
K19(K20(K175(),K143(K163((SCM-OK (#) SCM-VAL)),K163((SCM-OK (#) SCM-VAL))))) is set
K19(NAT) is set
INT is non empty V35() set
K174() \/ INT is non empty set
SCM-Data-Loc is Element of K19(SCM-Memory)
SCM-Data-Loc \/ INT is non empty set
SCMPDS-Instr is set
K20(SCMPDS-Instr,K143(K163((SCM-OK (#) SCM-VAL)),K163((SCM-OK (#) SCM-VAL)))) is Relation-like set
K19(K20(SCMPDS-Instr,K143(K163((SCM-OK (#) SCM-VAL)),K163((SCM-OK (#) SCM-VAL))))) is set
SCMPDS is non empty V86(2) IC-Ins-separated strict strict V94(2) AMI-Struct over 2
the carrier of SCMPDS is set
the InstructionsF of SCMPDS is non empty Relation-like standard-ins V76() J/A-independent V79() set
K316(2,SCMPDS) is Relation-like non-empty the carrier of SCMPDS -defined Function-like total set
the Object-Kind of SCMPDS is Relation-like Function-like V32( the carrier of SCMPDS,2) Element of K19(K20( the carrier of SCMPDS,2))
K20( the carrier of SCMPDS,2) is Relation-like set
K19(K20( the carrier of SCMPDS,2)) is set
the U7 of SCMPDS is Relation-like 2 -defined Function-like total set
the Object-Kind of SCMPDS (#) the U7 of SCMPDS is Relation-like Function-like set
RAT is non empty V35() set
K528() is non empty V86(2) IC-Ins-separated strict strict V94(2) AMI-Struct over 2
the InstructionsF of K528() is non empty Relation-like standard-ins V76() J/A-independent V79() set
the carrier of K528() is set
K316(2,K528()) is Relation-like non-empty the carrier of K528() -defined Function-like total set
the Object-Kind of K528() is Relation-like Function-like V32( the carrier of K528(),2) Element of K19(K20( the carrier of K528(),2))
K20( the carrier of K528(),2) is Relation-like set
K19(K20( the carrier of K528(),2)) is set
the U7 of K528() is Relation-like 2 -defined Function-like total set
the Object-Kind of K528() (#) the U7 of K528() is Relation-like Function-like set
1 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
3 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
0 is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional V74() Element of NAT
14 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
4 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
5 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
6 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
7 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
8 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
10 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
11 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
12 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
13 is ext-real positive non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements Element of NAT
IC is Element of the carrier of SCMPDS
RetIC is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
RetSP is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
NonZero SCMPDS is Element of K19( the carrier of SCMPDS)
K19( the carrier of SCMPDS) is set
{0,1,4,5,6,14} is set
Stop SCMPDS is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V35() V74() non halt-free V83( SCMPDS ) V84( SCMPDS ) paraclosed parahalting shiftable set
halt SCMPDS is V93(2, SCMPDS ) Element of the InstructionsF of SCMPDS
halt the InstructionsF of SCMPDS is ins-loc-free Element of the InstructionsF of SCMPDS
{} is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() integer Relation-like non-empty empty-yielding Function-like one-to-one constant functional V74() set
[0,{},{}] is V29() V30() set
[0,{}] is V29() set
[[0,{}],{}] is V29() set
Load is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() 1 -element V74() set
K366(0,(halt SCMPDS)) is V5() set
{0} is non empty functional set
K357({0},(halt SCMPDS)) is Relation-like Function-like V32({0},{(halt SCMPDS)}) Element of K19(K20({0},{(halt SCMPDS)}))
{(halt SCMPDS)} is non empty set
K20({0},{(halt SCMPDS)}) is Relation-like set
K19(K20({0},{(halt SCMPDS)})) is set
card (Stop SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 (Stop SCMPDS) is ext-real non empty V5() epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
SA0 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
SA0 ';' a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card SA0 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 SA0 is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift (a,(card SA0)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
SA0 +* (Shift (a,(card SA0))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
stop (SA0 ';' a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
(SA0 ';' a) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card (SA0 ';' a) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 (SA0 ';' a) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card (SA0 ';' a))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
(SA0 ';' a) +* (Shift ((Stop SCMPDS),(card (SA0 ';' a)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
a ';' (Stop SCMPDS) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card a is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 a is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card a)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
a +* (Shift ((Stop SCMPDS),(card a))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
SA0 ';' (a ';' (Stop SCMPDS)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
Shift ((a ';' (Stop SCMPDS)),(card SA0)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
SA0 +* (Shift ((a ';' (Stop SCMPDS)),(card SA0))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
SA0 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
stop SA0 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
SA0 ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card SA0 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 SA0 is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card SA0)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
SA0 +* (Shift ((Stop SCMPDS),(card SA0))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
proj1 (stop SA0) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
SA0 ';' a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
Shift (a,(card SA0)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
SA0 +* (Shift (a,(card SA0))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
stop (SA0 ';' a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
(SA0 ';' a) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card (SA0 ';' a) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 (SA0 ';' a) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card (SA0 ';' a))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
(SA0 ';' a) +* (Shift ((Stop SCMPDS),(card (SA0 ';' a)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
proj1 (stop (SA0 ';' a)) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
card (stop (SA0 ';' a)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(card (SA0 ';' a)) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
card a is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 a is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
(card SA0) + (card a) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
((card SA0) + (card a)) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(card SA0) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
((card SA0) + 1) + (card a) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
card (stop SA0) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
j is set
Mi is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
SA is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
SA0 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
stop SA0 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
SA0 ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card SA0 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 SA0 is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card SA0)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
SA0 +* (Shift ((Stop SCMPDS),(card SA0))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
SA0 ';' a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
Shift (a,(card SA0)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
SA0 +* (Shift (a,(card SA0))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
stop (SA0 ';' a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
(SA0 ';' a) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card (SA0 ';' a) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 (SA0 ';' a) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card (SA0 ';' a))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
(SA0 ';' a) +* (Shift ((Stop SCMPDS),(card (SA0 ';' a)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
(stop SA0) +* (stop (SA0 ';' a)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
proj1 (stop SA0) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
proj1 (stop (SA0 ';' a)) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible V35() 0 -started set
K366((IC ),0) is V5() set
{(IC )} is non empty set
K357({(IC )},0) is Relation-like Function-like V32({(IC )},{0}) Element of K19(K20({(IC )},{0}))
K20({(IC )},{0}) is Relation-like set
K19(K20({(IC )},{0})) is set
a is Int-like Element of the carrier of SCMPDS
P is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Initialize P is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total 0 -started set
P +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible K316(2,SCMPDS) -compatible total 0 -started set
(Initialize P) . a is ext-real V14() V15() integer set
P . a is ext-real V14() V15() integer set
proj1 (Start-At (0,SCMPDS)) is non empty set
a is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
P is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total 0 -started set
i is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() paraclosed parahalting set
stop i is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
i ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card i is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 i is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card i)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
i +* (Shift ((Stop SCMPDS),(card i))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
Mi is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Comput (a,s,Mi) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Comput (P,s,Mi) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
CurInstr (a,(Comput (a,s,Mi))) is Element of the InstructionsF of SCMPDS
IC (Comput (a,s,Mi)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (a,s,Mi)) . (IC ) is set
a /. (IC (Comput (a,s,Mi))) is Element of the InstructionsF of SCMPDS
CurInstr (P,(Comput (P,s,Mi))) is Element of the InstructionsF of SCMPDS
IC (Comput (P,s,Mi)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (P,s,Mi)) . (IC ) is set
P /. (IC (Comput (P,s,Mi))) is Element of the InstructionsF of SCMPDS
proj1 (stop i) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
SA is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Comput (P,s,SA) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
IC (Comput (P,s,SA)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (P,s,SA)) . (IC ) is set
P . (IC (Comput (P,s,Mi))) is Element of the InstructionsF of SCMPDS
(stop i) . (IC (Comput (P,s,Mi))) is set
a . (IC (Comput (a,s,Mi))) is Element of the InstructionsF of SCMPDS
a is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
P is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total 0 -started set
LifeSpan (a,s) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
LifeSpan (P,s) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Result (a,s) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Result (P,s) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
i is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() paraclosed parahalting set
stop i is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
i ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card i is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 i is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card i)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
i +* (Shift ((Stop SCMPDS),(card i))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
Mi is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Comput (P,s,Mi) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
CurInstr (P,(Comput (P,s,Mi))) is Element of the InstructionsF of SCMPDS
IC (Comput (P,s,Mi)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (P,s,Mi)) . (IC ) is set
P /. (IC (Comput (P,s,Mi))) is Element of the InstructionsF of SCMPDS
Comput (a,s,Mi) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
CurInstr (a,(Comput (a,s,Mi))) is Element of the InstructionsF of SCMPDS
IC (Comput (a,s,Mi)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (a,s,Mi)) . (IC ) is set
a /. (IC (Comput (a,s,Mi))) is Element of the InstructionsF of SCMPDS
Comput (P,s,(LifeSpan (a,s))) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
CurInstr (P,(Comput (P,s,(LifeSpan (a,s))))) is Element of the InstructionsF of SCMPDS
IC (Comput (P,s,(LifeSpan (a,s)))) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (P,s,(LifeSpan (a,s)))) . (IC ) is set
P /. (IC (Comput (P,s,(LifeSpan (a,s))))) is Element of the InstructionsF of SCMPDS
Comput (a,s,(LifeSpan (a,s))) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
CurInstr (a,(Comput (a,s,(LifeSpan (a,s))))) is Element of the InstructionsF of SCMPDS
IC (Comput (a,s,(LifeSpan (a,s)))) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (a,s,(LifeSpan (a,s)))) . (IC ) is set
a /. (IC (Comput (a,s,(LifeSpan (a,s))))) is Element of the InstructionsF of SCMPDS
a is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
P is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total 0 -started set
LifeSpan (a,P) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() paraclosed parahalting set
stop s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
s ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card s is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 s is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card s)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
s +* (Shift ((Stop SCMPDS),(card s))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
i is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
s ';' i is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
Shift (i,(card s)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
s +* (Shift (i,(card s))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
a +* (s ';' i) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
proj1 (s ';' i) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
proj1 (Shift (i,(card s))) is non empty V124() set
(proj1 s) \/ (proj1 (Shift (i,(card s)))) is non empty set
Mi is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Comput (a,P,Mi) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Comput ((a +* (s ';' i)),P,Mi) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Mi + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Comput (a,P,(Mi + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Comput ((a +* (s ';' i)),P,(Mi + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Following ((a +* (s ';' i)),(Comput ((a +* (s ';' i)),P,Mi))) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
CurInstr ((a +* (s ';' i)),(Comput ((a +* (s ';' i)),P,Mi))) is Element of the InstructionsF of SCMPDS
IC (Comput ((a +* (s ';' i)),P,Mi)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput ((a +* (s ';' i)),P,Mi)) . (IC ) is set
(a +* (s ';' i)) /. (IC (Comput ((a +* (s ';' i)),P,Mi))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr ((a +* (s ';' i)),(Comput ((a +* (s ';' i)),P,Mi)))),(Comput ((a +* (s ';' i)),P,Mi))) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set
K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V32( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))
K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set
K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((a +* (s ';' i)),(Comput ((a +* (s ';' i)),P,Mi))))) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((a +* (s ';' i)),(Comput ((a +* (s ';' i)),P,Mi))))) . (Comput ((a +* (s ';' i)),P,Mi)) is set
Following (a,(Comput (a,P,Mi))) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
CurInstr (a,(Comput (a,P,Mi))) is Element of the InstructionsF of SCMPDS
IC (Comput (a,P,Mi)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (a,P,Mi)) . (IC ) is set
a /. (IC (Comput (a,P,Mi))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (a,(Comput (a,P,Mi)))),(Comput (a,P,Mi))) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (a,(Comput (a,P,Mi))))) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (a,(Comput (a,P,Mi))))) . (Comput (a,P,Mi)) is set
proj1 (stop s) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
a . (IC (Comput (a,P,Mi))) is Element of the InstructionsF of SCMPDS
(stop s) . (IC (Comput (a,P,Mi))) is set
(a +* (s ';' i)) . (IC (Comput ((a +* (s ';' i)),P,Mi))) is Element of the InstructionsF of SCMPDS
s . (IC (Comput (a,P,Mi))) is set
(s ';' i) . (IC (Comput (a,P,Mi))) is set
Comput (a,P,0) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Comput ((a +* (s ';' i)),P,0) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
a is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
P is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total 0 -started set
LifeSpan (a,P) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() paraclosed parahalting set
stop s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
s ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card s is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 s is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card s)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
s +* (Shift ((Stop SCMPDS),(card s))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
i is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
s ';' i is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
Shift (i,(card s)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
s +* (Shift (i,(card s))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
stop (s ';' i) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
(s ';' i) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card (s ';' i) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 (s ';' i) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card (s ';' i))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
(s ';' i) +* (Shift ((Stop SCMPDS),(card (s ';' i)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
a +* (stop (s ';' i)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
SA is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Comput (a,P,SA) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Comput ((a +* (stop (s ';' i))),P,SA) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
i ';' (Stop SCMPDS) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card i is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 i is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card i)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
i +* (Shift ((Stop SCMPDS),(card i))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
s ';' (i ';' (Stop SCMPDS)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
Shift ((i ';' (Stop SCMPDS)),(card s)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
s +* (Shift ((i ';' (Stop SCMPDS)),(card s))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
a +* (s ';' (i ';' (Stop SCMPDS))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
DataLoc (0,0) is Int-like Element of the carrier of SCMPDS
(DataLoc (0,0)) := 0 is shiftable Element of the InstructionsF of SCMPDS
Load ((DataLoc (0,0)) := 0) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V35() 1 -element V74() set
K366(0,((DataLoc (0,0)) := 0)) is V5() set
K357({0},((DataLoc (0,0)) := 0)) is Relation-like Function-like V32({0},{((DataLoc (0,0)) := 0)}) Element of K19(K20({0},{((DataLoc (0,0)) := 0)}))
{((DataLoc (0,0)) := 0)} is non empty set
K20({0},{((DataLoc (0,0)) := 0)}) is Relation-like set
K19(K20({0},{((DataLoc (0,0)) := 0)})) is set
stop (Load ((DataLoc (0,0)) := 0)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
(Load ((DataLoc (0,0)) := 0)) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card (Load ((DataLoc (0,0)) := 0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 (Load ((DataLoc (0,0)) := 0)) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card (Load ((DataLoc (0,0)) := 0)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
(Load ((DataLoc (0,0)) := 0)) +* (Shift ((Stop SCMPDS),(card (Load ((DataLoc (0,0)) := 0))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
s is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total 0 -started set
i is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Macro ((DataLoc (0,0)) := 0) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
Comput (i,s,1) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
IC (Comput (i,s,1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (i,s,1)) . (IC ) is set
proj1 i is V124() set
CurInstr (i,(Comput (i,s,1))) is Element of the InstructionsF of SCMPDS
i /. (IC (Comput (i,s,1))) is Element of the InstructionsF of SCMPDS
IC s is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
s . (IC ) is set
Exec (((DataLoc (0,0)) := 0),s) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set
K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V32( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))
K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set
K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,((DataLoc (0,0)) := 0)) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,((DataLoc (0,0)) := 0)) . s is set
IC (Exec (((DataLoc (0,0)) := 0),s)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Exec (((DataLoc (0,0)) := 0),s)) . (IC ) is set
succ 0 is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements set
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 (stop (Load ((DataLoc (0,0)) := 0))) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
(stop (Load ((DataLoc (0,0)) := 0))) . 1 is set
i . 1 is Element of the InstructionsF of SCMPDS
(stop (Load ((DataLoc (0,0)) := 0))) . 0 is set
i . 0 is Element of the InstructionsF of SCMPDS
i /. (IC s) is Element of the InstructionsF of SCMPDS
i . (IC s) is Element of the InstructionsF of SCMPDS
Comput (i,s,(0 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Comput (i,s,0) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Following (i,(Comput (i,s,0))) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
CurInstr (i,(Comput (i,s,0))) is Element of the InstructionsF of SCMPDS
IC (Comput (i,s,0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (i,s,0)) . (IC ) is set
i /. (IC (Comput (i,s,0))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (i,(Comput (i,s,0)))),(Comput (i,s,0))) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (i,(Comput (i,s,0))))) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (i,(Comput (i,s,0))))) . (Comput (i,s,0)) is set
Following (i,s) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
CurInstr (i,s) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (i,s)),s) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (i,s))) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (i,s))) . s is set
a is shiftable Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode a is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113(a) is set
K113(K113(a)) is set
a is ext-real V14() V15() integer set
goto a is Element of the InstructionsF of SCMPDS
InsCode (goto a) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((goto a)) is set
K113(K113((goto a))) is set
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
a is Int-like Element of the carrier of SCMPDS
return a is Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode (return a) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113((return a)) is set
K113(K113((return a))) is set
a is Int-like Element of the carrier of SCMPDS
P is ext-real V14() V15() integer set
a := P is shiftable Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode (a := P) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113((a := P)) is set
K113(K113((a := P))) is set
saveIC (a,P) is Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode (saveIC (a,P)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113((saveIC (a,P))) is set
K113(K113((saveIC (a,P)))) is set
a is Int-like Element of the carrier of SCMPDS
P is ext-real V14() V15() integer set
s is ext-real V14() V15() integer set
(a,P) <>0_goto s is Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode ((a,P) <>0_goto s) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113(((a,P) <>0_goto s)) is set
K113(K113(((a,P) <>0_goto s))) is set
(a,P) <=0_goto s is Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode ((a,P) <=0_goto s) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113(((a,P) <=0_goto s)) is set
K113(K113(((a,P) <=0_goto s))) is set
(a,P) >=0_goto s is Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode ((a,P) >=0_goto s) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113(((a,P) >=0_goto s)) is set
K113(K113(((a,P) >=0_goto s))) is set
(a,P) := s is shiftable Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode ((a,P) := s) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113(((a,P) := s)) is set
K113(K113(((a,P) := s))) is set
a is Int-like Element of the carrier of SCMPDS
P is ext-real V14() V15() integer set
s is ext-real V14() V15() integer set
AddTo (a,P,s) is shiftable Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode (AddTo (a,P,s)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113((AddTo (a,P,s))) is set
K113(K113((AddTo (a,P,s)))) is set
a is Int-like Element of the carrier of SCMPDS
P is Int-like Element of the carrier of SCMPDS
s is ext-real V14() V15() integer set
i is ext-real V14() V15() integer set
AddTo (a,s,P,i) is shiftable Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode (AddTo (a,s,P,i)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113((AddTo (a,s,P,i))) is set
K113(K113((AddTo (a,s,P,i)))) is set
SubFrom (a,s,P,i) is shiftable Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode (SubFrom (a,s,P,i)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113((SubFrom (a,s,P,i))) is set
K113(K113((SubFrom (a,s,P,i)))) is set
MultBy (a,s,P,i) is shiftable Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode (MultBy (a,s,P,i)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113((MultBy (a,s,P,i))) is set
K113(K113((MultBy (a,s,P,i)))) is set
Divide (a,s,P,i) is shiftable Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode (Divide (a,s,P,i)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113((Divide (a,s,P,i))) is set
K113(K113((Divide (a,s,P,i)))) is set
(a,s) := (P,i) is shiftable Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
K123( the InstructionsF of SCMPDS) is set
proj1 the InstructionsF of SCMPDS is non empty set
proj1 (proj1 the InstructionsF of SCMPDS) is set
K113((halt SCMPDS)) is set
K113(K113((halt SCMPDS))) is set
InsCode ((a,s) := (P,i)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of InsCodes the InstructionsF of SCMPDS
K113(((a,s) := (P,i))) is set
K113(K113(((a,s) := (P,i)))) is set
Load (halt SCMPDS) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V35() 1 -element V74() set
a is () Element of the InstructionsF of SCMPDS
Load a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V35() 1 -element V74() set
K366(0,a) is V5() set
K357({0},a) is Relation-like Function-like V32({0},{a}) Element of K19(K20({0},{a}))
{a} is non empty set
K20({0},{a}) is Relation-like set
K19(K20({0},{a})) is set
P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
a is Element of the InstructionsF of SCMPDS
Load a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V35() 1 -element V74() set
K366(0,a) is V5() set
K357({0},a) is Relation-like Function-like V32({0},{a}) Element of K19(K20({0},{a}))
{a} is non empty set
K20({0},{a}) is Relation-like set
K19(K20({0},{a})) is set
stop (Load a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
(Load a) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
card (Load a) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 (Load a) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
Shift ((Stop SCMPDS),(card (Load a))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() set
(Load a) +* (Shift ((Stop SCMPDS),(card (Load a)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
s is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total 0 -started set
Macro a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() set
i is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Comput (i,s,1) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
IC (Comput (i,s,1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (i,s,1)) . (IC ) is set
proj1 i is V124() set
CurInstr (i,(Comput (i,s,1))) is Element of the InstructionsF of SCMPDS
i /. (IC (Comput (i,s,1))) is Element of the InstructionsF of SCMPDS
IC s is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
s . (IC ) is set
Exec (a,s) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set
K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V32( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))
K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set
K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,a) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,a) . s is set
IC (Exec (a,s)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Exec (a,s)) . (IC ) is set
succ 0 is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements set
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
proj1 (stop (Load a)) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements V124() set
(stop (Load a)) . 1 is set
i . 1 is Element of the InstructionsF of SCMPDS
(stop (Load a)) . 0 is set
i . 0 is Element of the InstructionsF of SCMPDS
i /. (IC s) is Element of the InstructionsF of SCMPDS
i . (IC s) is Element of the InstructionsF of SCMPDS
Comput (i,s,(0 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Comput (i,s,0) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Following (i,(Comput (i,s,0))) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
CurInstr (i,(Comput (i,s,0))) is Element of the InstructionsF of SCMPDS
IC (Comput (i,s,0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
(Comput (i,s,0)) . (IC ) is set
i /. (IC (Comput (i,s,0))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (i,(Comput (i,s,0)))),(Comput (i,s,0))) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (i,(Comput (i,s,0))))) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (i,(Comput (i,s,0))))) . (Comput (i,s,0)) is set
Following (i,s) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
CurInstr (i,s) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (i,s)),s) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (i,s))) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (i,s))) . s is set
a is Int-like Element of the carrier of SCMPDS
P is ext-real V14() V15() integer set
a := P is No-StopCode shiftable Element of the InstructionsF of SCMPDS
i is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Exec ((a := P),i) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set
K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V32( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))
K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set
K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(a := P)) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(a := P)) . i is set
(Exec ((a := P),i)) . (IC ) is set
IC i is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
i . (IC ) is set
succ (IC i) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements set
(IC i) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Load (a := P) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V35() 1 -element V74() set
K366(0,(a := P)) is V5() set
K357({0},(a := P)) is Relation-like Function-like V32({0},{(a := P)}) Element of K19(K20({0},{(a := P)}))
{(a := P)} is non empty set
K20({0},{(a := P)}) is Relation-like set
K19(K20({0},{(a := P)})) is set
a is Int-like Element of the carrier of SCMPDS
P is ext-real V14() V15() integer set
s is ext-real V14() V15() integer set
(a,P) := s is No-StopCode shiftable Element of the InstructionsF of SCMPDS
j is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Exec (((a,P) := s),j) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set
K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V32( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))
K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set
K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,((a,P) := s)) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,((a,P) := s)) . j is set
(Exec (((a,P) := s),j)) . (IC ) is set
IC j is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
j . (IC ) is set
succ (IC j) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements set
(IC j) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Load ((a,P) := s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V35() 1 -element V74() set
K366(0,((a,P) := s)) is V5() set
K357({0},((a,P) := s)) is Relation-like Function-like V32({0},{((a,P) := s)}) Element of K19(K20({0},{((a,P) := s)}))
{((a,P) := s)} is non empty set
K20({0},{((a,P) := s)}) is Relation-like set
K19(K20({0},{((a,P) := s)})) is set
AddTo (a,P,s) is No-StopCode shiftable Element of the InstructionsF of SCMPDS
j is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Exec ((AddTo (a,P,s)),j) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set
K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V32( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))
K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set
K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(AddTo (a,P,s))) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(AddTo (a,P,s))) . j is set
(Exec ((AddTo (a,P,s)),j)) . (IC ) is set
IC j is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
j . (IC ) is set
succ (IC j) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements set
(IC j) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Load (AddTo (a,P,s)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V35() 1 -element V74() set
K366(0,(AddTo (a,P,s))) is V5() set
K357({0},(AddTo (a,P,s))) is Relation-like Function-like V32({0},{(AddTo (a,P,s))}) Element of K19(K20({0},{(AddTo (a,P,s))}))
{(AddTo (a,P,s))} is non empty set
K20({0},{(AddTo (a,P,s))}) is Relation-like set
K19(K20({0},{(AddTo (a,P,s))})) is set
a is Int-like Element of the carrier of SCMPDS
P is Int-like Element of the carrier of SCMPDS
s is ext-real V14() V15() integer set
i is ext-real V14() V15() integer set
AddTo (a,s,P,i) is No-StopCode shiftable Element of the InstructionsF of SCMPDS
Mi is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
Exec ((AddTo (a,s,P,i)),Mi) is Relation-like the carrier of SCMPDS -defined Function-like K316(2,SCMPDS) -compatible total set
K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set
K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V32( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))
K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set
K19(K20( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(AddTo (a,s,P,i))) is Element of K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K163(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(AddTo (a,s,P,i))) . Mi is set
(Exec ((AddTo (a,s,P,i)),Mi)) . (IC ) is set
IC Mi is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Mi . (IC ) is set
succ (IC Mi) is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer non with_non-empty_elements set
(IC Mi) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() V15() integer Element of NAT
Load (AddTo (a,s,P,i)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V35() 1 -element V74() set
K366(0,(AddTo (a,s,P,i))) is V5() set
K357({0},(AddTo (a,s,P,i))) is Relation-like Function-like V32(