REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)
K6(REAL) is set
COMPLEX is set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
K6(NAT) is set
9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Segm 9 is Element of K6(NAT)
K161() is set
SCM-Memory is set
K6(SCM-Memory) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
K7(SCM-Memory,2) is Relation-like set
K6(K7(SCM-Memory,2)) is set
SCM-OK is Relation-like Function-like V29( SCM-Memory ,2) Element of K6(K7(SCM-Memory,2))
SCM-VAL is Relation-like 2 -defined Function-like total set
SCM-OK (#) SCM-VAL is Relation-like set
K150((SCM-OK (#) SCM-VAL)) is set
K162() is non empty set
K130(K150((SCM-OK (#) SCM-VAL)),K150((SCM-OK (#) SCM-VAL))) is set
K7(K162(),K130(K150((SCM-OK (#) SCM-VAL)),K150((SCM-OK (#) SCM-VAL)))) is Relation-like set
K6(K7(K162(),K130(K150((SCM-OK (#) SCM-VAL)),K150((SCM-OK (#) SCM-VAL))))) is set
K6(NAT) is set
SCMPDS is non empty V83(2) IC-Ins-separated strict strict V91(2) AMI-Struct over 2
the carrier of SCMPDS is set
the InstructionsF of SCMPDS is non empty Relation-like standard-ins V73() J/A-independent V76() set
K282(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 V29( the carrier of SCMPDS,2) Element of K6(K7( the carrier of SCMPDS,2))
K7( the carrier of SCMPDS,2) is Relation-like set
K6(K7( 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 set
RAT is set
INT is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding ext-real non positive non negative Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
6 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
IC is Element of the carrier of SCMPDS
K503(NAT,0) is non empty Element of K6(NAT)
SCM-Data-Loc is Element of K6(SCM-Memory)
Stop SCMPDS is non empty V2() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() V71() non halt-free V80( SCMPDS ) V81( SCMPDS ) paraclosed parahalting shiftable set
halt SCMPDS is parahalting Element of the InstructionsF of SCMPDS
halt the InstructionsF of SCMPDS is ins-loc-free Element of the InstructionsF of SCMPDS
Load is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set
(Stop SCMPDS) . 0 is set
dom (Stop SCMPDS) is non empty V2() epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
P is Element of the InstructionsF of SCMPDS
s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
P ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
Load P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set
(Load P) ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card (Load P) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (Load P) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift (s,(card (Load P))) is Relation-like Function-like set
(Load P) +* (Shift (s,(card (Load P)))) is non empty Relation-like Function-like set
card (P ';' s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (P ';' s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
card s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom s is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
(card s) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
card ((Load P) ';' s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((Load P) ';' s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
(card (Load P)) + (card s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P is Element of the InstructionsF of SCMPDS
s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
P ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
Load P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set
(Load P) ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card (Load P) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (Load P) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift (s,(card (Load P))) is Relation-like Function-like set
(Load P) +* (Shift (s,(card (Load P)))) is non empty Relation-like Function-like set
(P ';' s) . 0 is set
(Load P) . 0 is set
P is Element of the InstructionsF of SCMPDS
s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set
K332((IC ),0) is V2() set
{(IC )} is non empty set
K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))
{0} is non empty set
K7({(IC )},{0}) is Relation-like set
K6(K7({(IC )},{0})) is set
s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(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 V32() V71() set
P ';' I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
Load P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set
(Load P) ';' I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card (Load P) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (Load P) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift (I,(card (Load P))) is Relation-like Function-like set
(Load P) +* (Shift (I,(card (Load P)))) is non empty Relation-like Function-like set
stop (P ';' I) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
(P ';' I) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card (P ';' I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (P ';' I) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card (P ';' I))) is Relation-like Function-like set
(P ';' I) +* (Shift ((Stop SCMPDS),(card (P ';' I)))) is non empty Relation-like Function-like set
a is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
a +* (stop (P ';' I)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
CurInstr ((a +* (stop (P ';' I))),(Initialize s)) is Element of the InstructionsF of SCMPDS
IC (Initialize s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Initialize s) . (IC ) is set
(a +* (stop (P ';' I))) /. (IC (Initialize s)) is Element of the InstructionsF of SCMPDS
card I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom I is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
(card I) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
dom (stop (P ';' I)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
(a +* (stop (P ';' I))) . (IC (Initialize s)) is Element of the InstructionsF of SCMPDS
(a +* (stop (P ';' I))) . 0 is Element of the InstructionsF of SCMPDS
(stop (P ';' I)) . 0 is set
(P ';' I) . 0 is set
((Load P) ';' I) . 0 is set
(Load P) . 0 is set
P is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IC P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P . (IC ) is set
s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
ICplusConst (P,I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
s + I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
a + I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
abs (a + I) is V11() V12() ext-real Element of REAL
s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
stop s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
s ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom s is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card s)) is Relation-like Function-like set
s +* (Shift ((Stop SCMPDS),(card s))) is non empty Relation-like Function-like set
P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom P is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((stop s),(card P)) is Relation-like Function-like set
P ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
Shift (s,(card P)) is Relation-like Function-like set
P +* (Shift (s,(card P))) is non empty Relation-like Function-like set
stop (P ';' s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
(P ';' s) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card (P ';' s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (P ';' s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card (P ';' s))) is Relation-like Function-like set
(P ';' s) +* (Shift ((Stop SCMPDS),(card (P ';' s)))) is non empty Relation-like Function-like set
(P ';' s) ';' (Stop SCMPDS) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
s ';' (Stop SCMPDS) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
P ';' (s ';' (Stop SCMPDS)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
Shift ((s ';' (Stop SCMPDS)),(card P)) is Relation-like Function-like set
P +* (Shift ((s ';' (Stop SCMPDS)),(card P))) is non empty Relation-like Function-like set
P ';' (stop s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
P +* (Shift ((stop s),(card P))) is non empty Relation-like Function-like 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 K282(2,SCMPDS) -compatible total 0 -started set
I is No-StopCode parahalting Element of the InstructionsF of SCMPDS
Exec (I,s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set
K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))
K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set
K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set
K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,I) is Element of K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,I) . s is set
Initialize (Exec (I,s)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set
K332((IC ),0) is V2() set
{(IC )} is non empty set
K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))
{0} is non empty set
K7({(IC )},{0}) is Relation-like set
K6(K7({(IC )},{0})) is set
(Exec (I,s)) +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set
a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() paraclosed parahalting shiftable set
I ';' a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() paraclosed parahalting set
Load I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() halt-free V81( SCMPDS ) set
(Load I) ';' a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card (Load I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (Load I) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift (a,(card (Load I))) is Relation-like Function-like set
(Load I) +* (Shift (a,(card (Load I)))) is non empty Relation-like Function-like set
IExec ((I ';' a),P,s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
stop (I ';' a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
(I ';' a) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card (I ';' a) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (I ';' a) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card (I ';' a))) is Relation-like Function-like set
(I ';' a) +* (Shift ((Stop SCMPDS),(card (I ';' a)))) is non empty Relation-like Function-like set
P +* (stop (I ';' a)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Result ((P +* (stop (I ';' a))),s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IExec (a,P,(Initialize (Exec (I,s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
stop a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() V71() shiftable set
a ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom a is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card a)) is Relation-like Function-like set
a +* (Shift ((Stop SCMPDS),(card a))) is non empty Relation-like Function-like set
P +* (stop a) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Result ((P +* (stop a)),(Initialize (Exec (I,s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
b is Int-like Element of the carrier of SCMPDS
(IExec ((I ';' a),P,s)) . b is V11() V12() integer ext-real set
(IExec (a,P,(Initialize (Exec (I,s))))) . b is V11() V12() integer ext-real set
IExec (((Load I) ';' a),P,s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
stop ((Load I) ';' a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
((Load I) ';' a) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card ((Load I) ';' a) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((Load I) ';' a) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card ((Load I) ';' a))) is Relation-like Function-like set
((Load I) ';' a) +* (Shift ((Stop SCMPDS),(card ((Load I) ';' a)))) is non empty Relation-like Function-like set
P +* (stop ((Load I) ';' a)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Result ((P +* (stop ((Load I) ';' a))),s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
(IExec (((Load I) ';' a),P,s)) . b is V11() V12() integer ext-real set
IExec ((Load I),P,s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
stop (Load I) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() V81( SCMPDS ) set
(Load I) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
Shift ((Stop SCMPDS),(card (Load I))) is Relation-like Function-like set
(Load I) +* (Shift ((Stop SCMPDS),(card (Load I)))) is non empty Relation-like Function-like set
P +* (stop (Load I)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Result ((P +* (stop (Load I))),s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Initialize (IExec ((Load I),P,s)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
(IExec ((Load I),P,s)) +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set
IExec (a,P,(Initialize (IExec ((Load I),P,s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Result ((P +* (stop a)),(Initialize (IExec ((Load I),P,s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
(IExec (a,P,(Initialize (IExec ((Load I),P,s))))) . b is V11() V12() integer ext-real set
InsCode (halt SCMPDS) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
P is Int-like Element of the carrier of SCMPDS
s is V11() V12() integer ext-real set
I is V11() V12() integer ext-real set
(P,s) <>0_goto I is No-StopCode Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
P is Int-like Element of the carrier of SCMPDS
s is V11() V12() integer ext-real set
I is V11() V12() integer ext-real set
(P,s) <=0_goto I is No-StopCode Element of the InstructionsF of SCMPDS
InsCode (halt SCMPDS) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
P is Int-like Element of the carrier of SCMPDS
s is V11() V12() integer ext-real set
I is V11() V12() integer ext-real set
(P,s) >=0_goto I is No-StopCode Element of the InstructionsF of SCMPDS
P is V11() V12() integer ext-real set
goto P is Element of the InstructionsF of SCMPDS
Load (goto P) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set
P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
goto (P + 1) is Element of the InstructionsF of SCMPDS
- (P + 1) is V11() V12() integer ext-real non positive set
goto (- (P + 1)) is Element of the InstructionsF of SCMPDS
P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
((P + 1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
goto (P + 1) is No-StopCode Element of the InstructionsF of SCMPDS
Load (goto (P + 1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() halt-free V81( SCMPDS ) set
- (P + 1) is V11() V12() integer ext-real non positive set
((- (P + 1))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
goto (- (P + 1)) is No-StopCode Element of the InstructionsF of SCMPDS
Load (goto (- (P + 1))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() halt-free V81( SCMPDS ) set
P is V11() V12() integer ext-real set
(P) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
goto P is Element of the InstructionsF of SCMPDS
Load (goto P) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set
dom (P) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
s is V11() V12() integer ext-real set
(s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
goto s is Element of the InstructionsF of SCMPDS
Load (goto s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set
(s) . 0 is set
P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
stop P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
P ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom P is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card P)) is Relation-like Function-like set
P +* (Shift ((Stop SCMPDS),(card P))) is non empty Relation-like Function-like set
I is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
I +* (stop P) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set
K332((IC ),0) is V2() set
{(IC )} is non empty set
K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))
{0} is non empty set
K7({(IC )},{0}) is Relation-like set
K6(K7({(IC )},{0})) is set
s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set
dom (stop P) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput ((I +* (stop P)),(Initialize s),a) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IC (Comput ((I +* (stop P)),(Initialize s),a)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((I +* (stop P)),(Initialize s),a)) . (IC ) is set
s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
K249((stop P)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of K6(NAT)
I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
a is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Comput (a,s,I) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IC (Comput (a,s,I)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (a,s,I)) . (IC ) is set
Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set
a +* (stop P) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
stop P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
P ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom P is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card P)) is Relation-like Function-like set
P +* (Shift ((Stop SCMPDS),(card P))) is non empty Relation-like Function-like set
I is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
I +* (stop P) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set
K332((IC ),0) is V2() set
{(IC )} is non empty set
K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))
{0} is non empty set
K7({(IC )},{0}) is Relation-like set
K6(K7({(IC )},{0})) is set
s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set
s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
I is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set
I +* (stop P) is non empty 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 NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
DataPart I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
NonZero SCMPDS is Element of K6( the carrier of SCMPDS)
K6( the carrier of SCMPDS) is set
I | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
DataPart a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
a | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
b is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
stop b is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
b ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card b is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom b is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card b)) is Relation-like Function-like set
b +* (Shift ((Stop SCMPDS),(card b))) is non empty Relation-like Function-like set
Initialize I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set
K332((IC ),0) is V2() set
{(IC )} is non empty set
K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))
{0} is non empty set
K7({(IC )},{0}) is Relation-like set
K6(K7({(IC )},{0})) is set
I +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set
Initialize a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
a +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set
P +* (stop b) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s +* (stop b) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Comput ((s +* (stop b)),(Initialize a),0) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Comput ((P +* (stop b)),(Initialize I),0) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
DataPart (Comput ((P +* (stop b)),(Initialize I),0)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((P +* (stop b)),(Initialize I),0)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
DataPart (Comput ((s +* (stop b)),(Initialize a),0)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((s +* (stop b)),(Initialize a),0)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
dom (stop b) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
s4 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput ((s +* (stop b)),(Initialize a),(s4 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Comput ((s +* (stop b)),(Initialize a),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Following ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS
IC (Comput ((s +* (stop b)),(Initialize a),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((s +* (stop b)),(Initialize a),s4)) . (IC ) is set
(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4)))),(Comput ((s +* (stop b)),(Initialize a),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set
K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))
K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set
K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set
K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))))) is Element of K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))))) . (Comput ((s +* (stop b)),(Initialize a),s4)) is set
Comput ((P +* (stop b)),(Initialize I),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IC (Comput ((P +* (stop b)),(Initialize I),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((P +* (stop b)),(Initialize I),s4)) . (IC ) is set
CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS
(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS
DataPart (Comput ((P +* (stop b)),(Initialize I),s4)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((P +* (stop b)),(Initialize I),s4)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
DataPart (Comput ((s +* (stop b)),(Initialize a),s4)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((s +* (stop b)),(Initialize a),s4)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
s5 is Int-like Element of the carrier of SCMPDS
(Comput ((P +* (stop b)),(Initialize I),s4)) . s5 is V11() V12() integer ext-real set
(Comput ((s +* (stop b)),(Initialize a),s4)) . s5 is V11() V12() integer ext-real set
Comput ((P +* (stop b)),(Initialize I),(s4 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) . (IC ) is set
Following ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Exec ((CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4)))),(Comput ((P +* (stop b)),(Initialize I),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))))) is Element of K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))))) . (Comput ((P +* (stop b)),(Initialize I),s4)) is set
IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) . (IC ) is set
(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
(P +* (stop b)) . (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
(s +* (stop b)) . (IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
(stop b) . (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is set
CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
DataPart (Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
DataPart (Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
IC (Comput ((s +* (stop b)),(Initialize a),0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((s +* (stop b)),(Initialize a),0)) . (IC ) is set
IC (Initialize a) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Initialize a) . (IC ) is set
IC (Comput ((P +* (stop b)),(Initialize I),0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((P +* (stop b)),(Initialize I),0)) . (IC ) is set
(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS
(P +* (stop b)) . (IC (Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS
(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS
(s +* (stop b)) . (IC (Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS
IC (Initialize I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Initialize I) . (IC ) is set
CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS
(stop b) . 0 is set
CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS
s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput ((P +* (stop b)),(Initialize I),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IC (Comput ((P +* (stop b)),(Initialize I),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((P +* (stop b)),(Initialize I),s4)) . (IC ) is set
Comput ((s +* (stop b)),(Initialize a),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IC (Comput ((s +* (stop b)),(Initialize a),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((s +* (stop b)),(Initialize a),s4)) . (IC ) is set
P is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
DataPart I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
NonZero SCMPDS is Element of K6( the carrier of SCMPDS)
K6( the carrier of SCMPDS) is set
I | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
DataPart a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
a | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
b is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
stop b is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
b ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card b is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom b is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card b)) is Relation-like Function-like set
b +* (Shift ((Stop SCMPDS),(card b))) is non empty Relation-like Function-like set
Initialize I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set
K332((IC ),0) is V2() set
{(IC )} is non empty set
K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))
{0} is non empty set
K7({(IC )},{0}) is Relation-like set
K6(K7({(IC )},{0})) is set
I +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set
Initialize a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
a +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set
P +* (stop b) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s +* (stop b) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Comput ((P +* (stop b)),(Initialize I),0) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Comput ((s +* (stop b)),(Initialize a),0) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
dom (stop b) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
s4 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput ((s +* (stop b)),(Initialize a),(s4 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Comput ((s +* (stop b)),(Initialize a),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Following ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS
IC (Comput ((s +* (stop b)),(Initialize a),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((s +* (stop b)),(Initialize a),s4)) . (IC ) is set
(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4)))),(Comput ((s +* (stop b)),(Initialize a),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set
K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))
K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set
K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set
K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))))) is Element of K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))))) . (Comput ((s +* (stop b)),(Initialize a),s4)) is set
Comput ((P +* (stop b)),(Initialize I),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IC (Comput ((P +* (stop b)),(Initialize I),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((P +* (stop b)),(Initialize I),s4)) . (IC ) is set
CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS
(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS
DataPart (Comput ((P +* (stop b)),(Initialize I),s4)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((P +* (stop b)),(Initialize I),s4)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
DataPart (Comput ((s +* (stop b)),(Initialize a),s4)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((s +* (stop b)),(Initialize a),s4)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
s5 is Int-like Element of the carrier of SCMPDS
(Comput ((P +* (stop b)),(Initialize I),s4)) . s5 is V11() V12() integer ext-real set
(Comput ((s +* (stop b)),(Initialize a),s4)) . s5 is V11() V12() integer ext-real set
Comput ((P +* (stop b)),(Initialize I),(s4 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) . (IC ) is set
Following ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
Exec ((CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4)))),(Comput ((P +* (stop b)),(Initialize I),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))))) is Element of K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))))) . (Comput ((P +* (stop b)),(Initialize I),s4)) is set
IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) . (IC ) is set
(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
(P +* (stop b)) . (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
(s +* (stop b)) . (IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
(stop b) . (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is set
CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS
DataPart (Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
DataPart (Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
IC (Comput ((s +* (stop b)),(Initialize a),0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((s +* (stop b)),(Initialize a),0)) . (IC ) is set
IC (Initialize a) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Initialize a) . (IC ) is set
s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput ((P +* (stop b)),(Initialize I),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS
IC (Comput ((P +* (stop b)),(Initialize I),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((P +* (stop b)),(Initialize I),s4)) . (IC ) is set
(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS
IC (Comput ((P +* (stop b)),(Initialize I),0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((P +* (stop b)),(Initialize I),0)) . (IC ) is set
(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS
(P +* (stop b)) . (IC (Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS
(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS
(s +* (stop b)) . (IC (Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS
IC (Initialize I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Initialize I) . (IC ) is set
CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS
(stop b) . 0 is set
CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS
DataPart (Comput ((P +* (stop b)),(Initialize I),0)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((P +* (stop b)),(Initialize I),0)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
DataPart (Comput ((s +* (stop b)),(Initialize a),0)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((s +* (stop b)),(Initialize a),0)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
s5 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput ((P +* (stop b)),(Initialize I),s5) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IC (Comput ((P +* (stop b)),(Initialize I),s5)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((P +* (stop b)),(Initialize I),s5)) . (IC ) is set
Comput ((s +* (stop b)),(Initialize a),s5) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
IC (Comput ((s +* (stop b)),(Initialize a),s5)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((s +* (stop b)),(Initialize a),s5)) . (IC ) is set
Comput ((s +* (stop b)),(Initialize a),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS
IC (Comput ((s +* (stop b)),(Initialize a),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput ((s +* (stop b)),(Initialize a),s4)) . (IC ) is set
(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS
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 K282(2,SCMPDS) -compatible total set
Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set
K332((IC ),0) is V2() set
{(IC )} is non empty set
K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))
{0} is non empty set
K7({(IC )},{0}) is Relation-like set
K6(K7({(IC )},{0})) is set
s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(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 V32() V71() set
a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
P +* a is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
DataPart s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
NonZero SCMPDS is Element of K6( the carrier of SCMPDS)
K6( the carrier of SCMPDS) is set
s | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
DataPart (Initialize s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Initialize s) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined 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 K282(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 V32() V71() set
stop I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
I ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom I is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card I)) is Relation-like Function-like set
I +* (Shift ((Stop SCMPDS),(card I))) is non empty Relation-like Function-like set
P +* (stop I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
LifeSpan ((P +* (stop I)),s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
I ';' a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
Shift (a,(card I)) is Relation-like Function-like set
I +* (Shift (a,(card I))) is non empty Relation-like Function-like set
stop (I ';' a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
(I ';' a) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set
card (I ';' a) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (I ';' a) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
Shift ((Stop SCMPDS),(card (I ';' a))) is Relation-like Function-like set
(I ';' a) +* (Shift ((Stop SCMPDS),(card (I ';' a)))) is non empty Relation-like Function-like set
P +* (stop (I ';' a)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
NonZero SCMPDS is Element of K6( the carrier of SCMPDS)
K6( the carrier of SCMPDS) is set
(Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
Comput ((P +* (stop (I ';' a))),s,(LifeSpan ((P +* (stop I)),s))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set
DataPart (Comput ((P +* (stop (I ';' a))),s,(LifeSpan ((P +* (stop I)),s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set
(Comput ((P +* (stop (I ';' a))),s,(LifeSpan ((P +* (stop I)),s)))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set
Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0