REAL is non empty V36() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V36() cardinal limit_cardinal Element of K19(REAL)
K19(REAL) is V36() set
K532() is non empty V130(2) IC-Ins-separated strict V138(2) AMI-Struct over 2
2 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
SCM-Memory is set
K562(NAT,SCM-Memory) is Element of SCM-Memory
K429() is non empty set
SCM-OK is Relation-like SCM-Memory -defined 2 -valued Function-like V32( SCM-Memory ,2) Element of K19(K20(SCM-Memory,2))
K20(SCM-Memory,2) is Relation-like set
K19(K20(SCM-Memory,2)) is set
SCM-VAL is non empty Relation-like 2 -defined Function-like total set
SCM-Exec is Relation-like K429() -defined K143(K417((SCM-OK (#) SCM-VAL)),K417((SCM-OK (#) SCM-VAL))) -valued Function-like V32(K429(),K143(K417((SCM-OK (#) SCM-VAL)),K417((SCM-OK (#) SCM-VAL)))) Element of K19(K20(K429(),K143(K417((SCM-OK (#) SCM-VAL)),K417((SCM-OK (#) SCM-VAL)))))
SCM-OK (#) SCM-VAL is Relation-like SCM-Memory -defined Function-like total set
K417((SCM-OK (#) SCM-VAL)) is set
K143(K417((SCM-OK (#) SCM-VAL)),K417((SCM-OK (#) SCM-VAL))) is set
K20(K429(),K143(K417((SCM-OK (#) SCM-VAL)),K417((SCM-OK (#) SCM-VAL)))) is Relation-like set
K19(K20(K429(),K143(K417((SCM-OK (#) SCM-VAL)),K417((SCM-OK (#) SCM-VAL))))) is set
AMI-Struct(# SCM-Memory,K562(NAT,SCM-Memory),K429(),SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2
the carrier of K532() is set
K514(2,K532()) is Relation-like non-empty the carrier of K532() -defined Function-like total set
the Object-Kind of K532() is Relation-like the carrier of K532() -defined 2 -valued Function-like V32( the carrier of K532(),2) Element of K19(K20( the carrier of K532(),2))
K20( the carrier of K532(),2) is Relation-like set
K19(K20( the carrier of K532(),2)) is set
the U7 of K532() is non empty Relation-like 2 -defined Function-like total set
the Object-Kind of K532() (#) the U7 of K532() is Relation-like the carrier of K532() -defined Function-like total set
COMPLEX is non empty V36() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V36() cardinal limit_cardinal set
K19(NAT) is V36() set
K19(NAT) is V36() set
RAT is non empty V36() set
INT is non empty V36() set
K20(REAL,REAL) is Relation-like V36() set
K19(K20(REAL,REAL)) is V36() set
{} is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() Function-yielding V81() V118() set
1 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
{{},1} is non empty set
K371() is set
K19(K371()) is set
K372() is Element of K19(K371())
9 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
Segm 9 is Element of K19(NAT)
K428() is set
K19(SCM-Memory) is set
the InstructionsF of K532() is non empty Relation-like standard-ins V120() J/A-independent V123() set
SCMPDS is non empty V130(2) IC-Ins-separated strict strict V138(2) AMI-Struct over 2
the carrier of SCMPDS is set
the InstructionsF of SCMPDS is non empty Relation-like standard-ins V120() J/A-independent V123() set
K514(2,SCMPDS) is Relation-like non-empty the carrier of SCMPDS -defined Function-like total set
the Object-Kind of SCMPDS is Relation-like the carrier of SCMPDS -defined 2 -valued 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 non empty Relation-like 2 -defined Function-like total set
the Object-Kind of SCMPDS (#) the U7 of SCMPDS is Relation-like the carrier of SCMPDS -defined Function-like total set
3 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
0 is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() Function-yielding V81() V118() Element of NAT
K56(1) is ext-real non positive V14() V15() integer Element of REAL
14 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
4 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
5 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
6 is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
IC is Element of the carrier of SCMPDS
NonZero SCMPDS is Element of K19( the carrier of SCMPDS)
K19( the carrier of SCMPDS) is set
SCM-Data-Loc is Element of K19(SCM-Memory)
<*> REAL is ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() V15() integer Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() Function-yielding V81() V118() FinSequence of REAL
K305((<*> REAL)) is ext-real V14() V15() Element of REAL
P is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
IC P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
P . (IC ) is set
s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
sp is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
sp - s is ext-real V14() V15() integer set
ICplusConst (P,(sp - s)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
cv is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
cv + (sp - s) is ext-real V14() V15() integer set
abs (cv + (sp - s)) is ext-real V14() V15() Element of REAL
P is Element of the InstructionsF of SCMPDS
s is Element of the InstructionsF of SCMPDS
sp is Element of the InstructionsF of SCMPDS
cv is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
P ';' cv is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
Load P is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
(Load P) ';' cv is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card (Load P) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom (Load P) is ext-real positive non negative non empty V5() epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal 1 -element V47() V74() set
Shift (cv,(card (Load P))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
(Load P) +* (Shift (cv,(card (Load P)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
(P ';' cv) ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
Load s is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
(P ';' cv) ';' (Load s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card (P ';' cv) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom (P ';' cv) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Load s),(card (P ';' cv))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
(P ';' cv) +* (Shift ((Load s),(card (P ';' cv)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
((P ';' cv) ';' s) ';' sp is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
Load sp is non empty V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
((P ';' cv) ';' s) ';' (Load sp) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card ((P ';' cv) ';' s) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom ((P ';' cv) ';' s) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Load sp),(card ((P ';' cv) ';' s))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
((P ';' cv) ';' s) +* (Shift ((Load sp),(card ((P ';' cv) ';' s)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
cv ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
cv ';' (Load s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card cv is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom cv is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Load s),(card cv)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
cv +* (Shift ((Load s),(card cv))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
(cv ';' s) ';' sp is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
(cv ';' s) ';' (Load sp) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card (cv ';' s) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom (cv ';' s) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Load sp),(card (cv ';' s))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
(cv ';' s) +* (Shift ((Load sp),(card (cv ';' s)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
P ';' ((cv ';' s) ';' sp) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
(Load P) ';' ((cv ';' s) ';' sp) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
Shift (((cv ';' s) ';' sp),(card (Load P))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
(Load P) +* (Shift (((cv ';' s) ';' sp),(card (Load P)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
P ';' (cv ';' s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
(Load P) ';' (cv ';' s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
Shift ((cv ';' s),(card (Load P))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
(Load P) +* (Shift ((cv ';' s),(card (Load P)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
(P ';' (cv ';' s)) ';' sp is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
(P ';' (cv ';' s)) ';' (Load sp) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card (P ';' (cv ';' s)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom (P ';' (cv ';' s)) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Load sp),(card (P ';' (cv ';' s)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
(P ';' (cv ';' s)) +* (Shift ((Load sp),(card (P ';' (cv ';' s))))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card s is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom s is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift (P,(card s)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
s ';' P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
s +* (Shift (P,(card s))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
sp is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
(s ';' P) ';' sp is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card (s ';' P) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom (s ';' P) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift (sp,(card (s ';' P))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
(s ';' P) +* (Shift (sp,(card (s ';' P)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
dom (s ';' P) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() Element of K19(NAT)
dom (Shift (sp,(card (s ';' P)))) is non empty V74() set
P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
P ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card P is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom P is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift (s,(card P)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
P +* (Shift (s,(card P))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
stop (P ';' s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() 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 V36() 1 -element V118() non halt-free V127( SCMPDS ) V128( SCMPDS ) paraclosed parahalting shiftable set
halt SCMPDS is V137(2, SCMPDS ) 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 V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
(P ';' s) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card (P ';' s) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom (P ';' s) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Stop SCMPDS),(card (P ';' s))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
(P ';' s) +* (Shift ((Stop SCMPDS),(card (P ';' s)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
s ';' (Stop SCMPDS) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card s is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom s is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Stop SCMPDS),(card s)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
s +* (Shift ((Stop SCMPDS),(card s))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
P ';' (s ';' (Stop SCMPDS)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
Shift ((s ';' (Stop SCMPDS)),(card P)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
P +* (Shift ((s ';' (Stop SCMPDS)),(card P))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
{0,4,5,6,14} is set
P is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
DataPart P is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible data-only set
P | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible set
s is Element of the InstructionsF of SCMPDS
InsCode s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of InsCodes the InstructionsF of SCMPDS
InsCodes the InstructionsF of SCMPDS is non empty set
Exec (s,P) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set
K143(K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like the InstructionsF of SCMPDS -defined K143(K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) -valued Function-like V32( the InstructionsF of SCMPDS,K143(K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K19(K20( the InstructionsF of SCMPDS,K143(K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))
K20( the InstructionsF of SCMPDS,K143(K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set
K19(K20( the InstructionsF of SCMPDS,K143(K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set
K145( the InstructionsF of SCMPDS,K143(K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,s) is Element of K143(K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))
K145( the InstructionsF of SCMPDS,K143(K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K417(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,s) . P is set
DataPart (Exec (s,P)) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible data-only set
(Exec (s,P)) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible set
sp is Int-like Element of the carrier of SCMPDS
(Exec (s,P)) . sp is ext-real V14() V15() integer set
P . sp is ext-real V14() V15() integer set
sp is Int-like Element of the carrier of SCMPDS
(Exec (s,P)) . sp is ext-real V14() V15() integer set
P . sp is ext-real V14() V15() integer set
cv is ext-real V14() V15() integer set
goto cv is Element of the InstructionsF of SCMPDS
<*cv*> is non empty V5() Relation-like NAT -defined Function-like constant V36() 1 -element FinSequence-like FinSubsequence-like set
K115(14,{},<*cv*>) is set
sp is Int-like Element of the carrier of SCMPDS
(Exec (s,P)) . sp is ext-real V14() V15() integer set
P . sp is ext-real V14() V15() integer set
cv is Int-like Element of the carrier of SCMPDS
fr is ext-real V14() V15() integer set
pp is ext-real V14() V15() integer set
(cv,fr) <>0_goto pp is No-StopCode Element of the InstructionsF of SCMPDS
<*cv,fr,pp*> is non empty Relation-like NAT -defined Function-like V36() 3 -element FinSequence-like FinSubsequence-like set
K115(4,{},<*cv,fr,pp*>) is set
sp is Int-like Element of the carrier of SCMPDS
(Exec (s,P)) . sp is ext-real V14() V15() integer set
P . sp is ext-real V14() V15() integer set
cv is Int-like Element of the carrier of SCMPDS
fr is ext-real V14() V15() integer set
pp is ext-real V14() V15() integer set
(cv,fr) <=0_goto pp is No-StopCode Element of the InstructionsF of SCMPDS
<*cv,fr,pp*> is non empty Relation-like NAT -defined Function-like V36() 3 -element FinSequence-like FinSubsequence-like set
K115(5,{},<*cv,fr,pp*>) is set
sp is Int-like Element of the carrier of SCMPDS
(Exec (s,P)) . sp is ext-real V14() V15() integer set
P . sp is ext-real V14() V15() integer set
cv is Int-like Element of the carrier of SCMPDS
fr is ext-real V14() V15() integer set
pp is ext-real V14() V15() integer set
(cv,fr) >=0_goto pp is No-StopCode Element of the InstructionsF of SCMPDS
<*cv,fr,pp*> is non empty Relation-like NAT -defined Function-like V36() 3 -element FinSequence-like FinSubsequence-like set
K115(6,{},<*cv,fr,pp*>) is set
P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
DataPart sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible data-only set
sp | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible set
cv is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
DataPart cv is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible data-only set
cv | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible set
Initialize sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible V36() 0 -started set
(IC ) .--> 0 is V5() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V59() V60() V61() V62() V63() V64() V65() V66() Function-yielding V81() set
{(IC )} is non empty V5() 1 -element set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total V32({(IC )},{0}) V59() V60() V61() V62() Function-yielding V81() Element of K19(K20({(IC )},{0}))
{0} is non empty V5() functional 1 -element set
K20({(IC )},{0}) is Relation-like set
K19(K20({(IC )},{0})) is set
sp +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible K514(2,SCMPDS) -compatible total 0 -started set
Initialize cv is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
cv +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible K514(2,SCMPDS) -compatible total 0 -started set
fr is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
stop fr is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() 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 V36() 1 -element V118() non halt-free V127( SCMPDS ) V128( SCMPDS ) paraclosed parahalting shiftable set
halt SCMPDS is V137(2, SCMPDS ) 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 V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
fr ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card fr is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom fr is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Stop SCMPDS),(card fr)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
fr +* (Shift ((Stop SCMPDS),(card fr))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
P +* (stop fr) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s +* (stop fr) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
PP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput ((P +* (stop fr)),(Initialize sp),PP) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
Comput ((s +* (stop fr)),(Initialize cv),PP) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr ((P +* (stop fr)),(Comput ((P +* (stop fr)),(Initialize sp),PP))) is Element of the InstructionsF of SCMPDS
IC (Comput ((P +* (stop fr)),(Initialize sp),PP)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput ((P +* (stop fr)),(Initialize sp),PP)) . (IC ) is set
(P +* (stop fr)) /. (IC (Comput ((P +* (stop fr)),(Initialize sp),PP))) is Element of the InstructionsF of SCMPDS
CurInstr ((s +* (stop fr)),(Comput ((s +* (stop fr)),(Initialize cv),PP))) is Element of the InstructionsF of SCMPDS
IC (Comput ((s +* (stop fr)),(Initialize cv),PP)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput ((s +* (stop fr)),(Initialize cv),PP)) . (IC ) is set
(s +* (stop fr)) /. (IC (Comput ((s +* (stop fr)),(Initialize cv),PP))) is Element of the InstructionsF of SCMPDS
dom (stop fr) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() Element of K19(NAT)
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput ((s +* (stop fr)),(Initialize cv),n) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
IC (Comput ((s +* (stop fr)),(Initialize cv),n)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput ((s +* (stop fr)),(Initialize cv),n)) . (IC ) is set
(s +* (stop fr)) . (IC (Comput ((s +* (stop fr)),(Initialize cv),PP))) is Element of the InstructionsF of SCMPDS
(stop fr) . (IC (Comput ((s +* (stop fr)),(Initialize cv),PP))) is set
(P +* (stop fr)) . (IC (Comput ((P +* (stop fr)),(Initialize sp),PP))) is Element of the InstructionsF of SCMPDS
P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
cv is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
stop cv is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() 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 V36() 1 -element V118() non halt-free V127( SCMPDS ) V128( SCMPDS ) paraclosed parahalting shiftable set
halt SCMPDS is V137(2, SCMPDS ) 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 V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
cv ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card cv is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom cv is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Stop SCMPDS),(card cv)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
cv +* (Shift ((Stop SCMPDS),(card cv))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible V36() 0 -started set
(IC ) .--> 0 is V5() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V59() V60() V61() V62() V63() V64() V65() V66() Function-yielding V81() set
{(IC )} is non empty V5() 1 -element set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total V32({(IC )},{0}) V59() V60() V61() V62() Function-yielding V81() Element of K19(K20({(IC )},{0}))
{0} is non empty V5() functional 1 -element set
K20({(IC )},{0}) is Relation-like set
K19(K20({(IC )},{0})) is set
Initialize sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
sp +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible K514(2,SCMPDS) -compatible total 0 -started set
s +* (stop cv) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
DataPart sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible data-only set
sp | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible set
P +* (stop cv) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
pp is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput (P,sp,pp) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
Comput (s,sp,pp) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
pD is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput (P,sp,pD) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr (P,(Comput (P,sp,pD))) is Element of the InstructionsF of SCMPDS
IC (Comput (P,sp,pD)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (P,sp,pD)) . (IC ) is set
P /. (IC (Comput (P,sp,pD))) is Element of the InstructionsF of SCMPDS
Comput (s,sp,pD) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr (s,(Comput (s,sp,pD))) is Element of the InstructionsF of SCMPDS
IC (Comput (s,sp,pD)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (s,sp,pD)) . (IC ) is set
s /. (IC (Comput (s,sp,pD))) is Element of the InstructionsF of SCMPDS
P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
LifeSpan (P,sp) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
LifeSpan (s,sp) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Result (P,sp) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
Result (s,sp) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
cv is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
stop cv is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() 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 V36() 1 -element V118() non halt-free V127( SCMPDS ) V128( SCMPDS ) paraclosed parahalting shiftable set
halt SCMPDS is V137(2, SCMPDS ) 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 V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
cv ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card cv is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom cv is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Stop SCMPDS),(card cv)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
cv +* (Shift ((Stop SCMPDS),(card cv))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible V36() 0 -started set
(IC ) .--> 0 is V5() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V59() V60() V61() V62() V63() V64() V65() V66() Function-yielding V81() set
{(IC )} is non empty V5() 1 -element set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total V32({(IC )},{0}) V59() V60() V61() V62() Function-yielding V81() Element of K19(K20({(IC )},{0}))
{0} is non empty V5() functional 1 -element set
K20({(IC )},{0}) is Relation-like set
K19(K20({(IC )},{0})) is set
DataPart sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible data-only set
sp | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible set
Initialize sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
sp +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible K514(2,SCMPDS) -compatible total 0 -started set
s +* (stop cv) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
P +* (stop cv) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
fr is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput (s,sp,fr) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr (s,(Comput (s,sp,fr))) is Element of the InstructionsF of SCMPDS
IC (Comput (s,sp,fr)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (s,sp,fr)) . (IC ) is set
s /. (IC (Comput (s,sp,fr))) is Element of the InstructionsF of SCMPDS
Comput (P,sp,fr) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr (P,(Comput (P,sp,fr))) is Element of the InstructionsF of SCMPDS
IC (Comput (P,sp,fr)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (P,sp,fr)) . (IC ) is set
P /. (IC (Comput (P,sp,fr))) is Element of the InstructionsF of SCMPDS
Comput (s,sp,(LifeSpan (P,sp))) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr (s,(Comput (s,sp,(LifeSpan (P,sp))))) is Element of the InstructionsF of SCMPDS
IC (Comput (s,sp,(LifeSpan (P,sp)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (s,sp,(LifeSpan (P,sp)))) . (IC ) is set
s /. (IC (Comput (s,sp,(LifeSpan (P,sp))))) is Element of the InstructionsF of SCMPDS
Comput (P,sp,(LifeSpan (P,sp))) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr (P,(Comput (P,sp,(LifeSpan (P,sp))))) is Element of the InstructionsF of SCMPDS
IC (Comput (P,sp,(LifeSpan (P,sp)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (P,sp,(LifeSpan (P,sp)))) . (IC ) is set
P /. (IC (Comput (P,sp,(LifeSpan (P,sp))))) is Element of the InstructionsF of SCMPDS
P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
DataPart sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible data-only set
sp | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible set
cv is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
DataPart cv is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible data-only set
cv | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible set
Initialize sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible V36() 0 -started set
(IC ) .--> 0 is V5() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V59() V60() V61() V62() V63() V64() V65() V66() Function-yielding V81() set
{(IC )} is non empty V5() 1 -element set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total V32({(IC )},{0}) V59() V60() V61() V62() Function-yielding V81() Element of K19(K20({(IC )},{0}))
{0} is non empty V5() functional 1 -element set
K20({(IC )},{0}) is Relation-like set
K19(K20({(IC )},{0})) is set
sp +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible K514(2,SCMPDS) -compatible total 0 -started set
Initialize cv is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
cv +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible K514(2,SCMPDS) -compatible total 0 -started set
fr is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
stop fr is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() 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 V36() 1 -element V118() non halt-free V127( SCMPDS ) V128( SCMPDS ) paraclosed parahalting shiftable set
halt SCMPDS is V137(2, SCMPDS ) 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 V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
fr ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card fr is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom fr is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Stop SCMPDS),(card fr)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
fr +* (Shift ((Stop SCMPDS),(card fr))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
P +* (stop fr) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
LifeSpan ((P +* (stop fr)),(Initialize sp)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
s +* (stop fr) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
LifeSpan ((s +* (stop fr)),(Initialize cv)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Result ((P +* (stop fr)),(Initialize sp)) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
Result ((s +* (stop fr)),(Initialize cv)) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
Comput ((P +* (stop fr)),(Initialize sp),(LifeSpan ((P +* (stop fr)),(Initialize sp)))) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
PD is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput ((s +* (stop fr)),(Initialize cv),PD) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr ((s +* (stop fr)),(Comput ((s +* (stop fr)),(Initialize cv),PD))) is Element of the InstructionsF of SCMPDS
IC (Comput ((s +* (stop fr)),(Initialize cv),PD)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput ((s +* (stop fr)),(Initialize cv),PD)) . (IC ) is set
(s +* (stop fr)) /. (IC (Comput ((s +* (stop fr)),(Initialize cv),PD))) is Element of the InstructionsF of SCMPDS
Comput ((P +* (stop fr)),(Initialize sp),PD) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr ((P +* (stop fr)),(Comput ((P +* (stop fr)),(Initialize sp),PD))) is Element of the InstructionsF of SCMPDS
IC (Comput ((P +* (stop fr)),(Initialize sp),PD)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput ((P +* (stop fr)),(Initialize sp),PD)) . (IC ) is set
(P +* (stop fr)) /. (IC (Comput ((P +* (stop fr)),(Initialize sp),PD))) is Element of the InstructionsF of SCMPDS
Comput ((s +* (stop fr)),(Initialize cv),(LifeSpan ((P +* (stop fr)),(Initialize sp)))) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr ((s +* (stop fr)),(Comput ((s +* (stop fr)),(Initialize cv),(LifeSpan ((P +* (stop fr)),(Initialize sp)))))) is Element of the InstructionsF of SCMPDS
IC (Comput ((s +* (stop fr)),(Initialize cv),(LifeSpan ((P +* (stop fr)),(Initialize sp))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput ((s +* (stop fr)),(Initialize cv),(LifeSpan ((P +* (stop fr)),(Initialize sp))))) . (IC ) is set
(s +* (stop fr)) /. (IC (Comput ((s +* (stop fr)),(Initialize cv),(LifeSpan ((P +* (stop fr)),(Initialize sp)))))) is Element of the InstructionsF of SCMPDS
CurInstr ((P +* (stop fr)),(Comput ((P +* (stop fr)),(Initialize sp),(LifeSpan ((P +* (stop fr)),(Initialize sp)))))) is Element of the InstructionsF of SCMPDS
IC (Comput ((P +* (stop fr)),(Initialize sp),(LifeSpan ((P +* (stop fr)),(Initialize sp))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput ((P +* (stop fr)),(Initialize sp),(LifeSpan ((P +* (stop fr)),(Initialize sp))))) . (IC ) is set
(P +* (stop fr)) /. (IC (Comput ((P +* (stop fr)),(Initialize sp),(LifeSpan ((P +* (stop fr)),(Initialize sp)))))) is Element of the InstructionsF of SCMPDS
P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
cv is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
Result (P,sp) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
Result (s,cv) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
fr is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
stop fr is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() 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 V36() 1 -element V118() non halt-free V127( SCMPDS ) V128( SCMPDS ) paraclosed parahalting shiftable set
halt SCMPDS is V137(2, SCMPDS ) 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 V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
fr ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card fr is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom fr is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Stop SCMPDS),(card fr)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
fr +* (Shift ((Stop SCMPDS),(card fr))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
P +* (stop fr) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s +* (stop fr) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Initialize sp is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible V36() 0 -started set
(IC ) .--> 0 is V5() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V59() V60() V61() V62() V63() V64() V65() V66() Function-yielding V81() set
{(IC )} is non empty V5() 1 -element set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total V32({(IC )},{0}) V59() V60() V61() V62() Function-yielding V81() Element of K19(K20({(IC )},{0}))
{0} is non empty V5() functional 1 -element set
K20({(IC )},{0}) is Relation-like set
K19(K20({(IC )},{0})) is set
sp +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible K514(2,SCMPDS) -compatible total 0 -started set
pD is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput (P,sp,pD) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr (P,(Comput (P,sp,pD))) is Element of the InstructionsF of SCMPDS
IC (Comput (P,sp,pD)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (P,sp,pD)) . (IC ) is set
P /. (IC (Comput (P,sp,pD))) is Element of the InstructionsF of SCMPDS
Initialize cv is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
cv +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible K514(2,SCMPDS) -compatible total 0 -started set
f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput (P,sp,f) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
dom (Comput (P,sp,f)) is set
IC (Comput (P,sp,f)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (P,sp,f)) . (IC ) is set
Initialize (Comput (P,sp,f)) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
(Comput (P,sp,f)) +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible K514(2,SCMPDS) -compatible total 0 -started set
PP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput (P,(Comput (P,sp,f)),PP) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
IC (Comput (P,(Comput (P,sp,f)),PP)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (P,(Comput (P,sp,f)),PP)) . (IC ) is set
f + PP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput (P,sp,(f + PP)) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
IC (Comput (P,sp,(f + PP))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (P,sp,(f + PP))) . (IC ) is set
dom (stop fr) is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() Element of K19(NAT)
Comput (P,(Comput (P,sp,f)),pD) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr (P,(Comput (P,(Comput (P,sp,f)),pD))) is Element of the InstructionsF of SCMPDS
IC (Comput (P,(Comput (P,sp,f)),pD)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (P,(Comput (P,sp,f)),pD)) . (IC ) is set
P /. (IC (Comput (P,(Comput (P,sp,f)),pD))) is Element of the InstructionsF of SCMPDS
f + pD is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput (P,sp,(f + pD)) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr (P,(Comput (P,sp,(f + pD)))) is Element of the InstructionsF of SCMPDS
IC (Comput (P,sp,(f + pD))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (P,sp,(f + pD))) . (IC ) is set
P /. (IC (Comput (P,sp,(f + pD)))) is Element of the InstructionsF of SCMPDS
DataPart (Comput (P,sp,f)) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible data-only set
(Comput (P,sp,f)) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible set
DataPart cv is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible data-only set
cv | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible set
PP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput (P,sp,PP) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
CurInstr (P,(Comput (P,sp,PP))) is Element of the InstructionsF of SCMPDS
IC (Comput (P,sp,PP)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (P,sp,PP)) . (IC ) is set
P /. (IC (Comput (P,sp,PP))) is Element of the InstructionsF of SCMPDS
P . (IC (Comput (P,sp,PP))) is Element of the InstructionsF of SCMPDS
Result (P,(Comput (P,sp,f))) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
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 K514(2,SCMPDS) -compatible total set
Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible V36() 0 -started set
(IC ) .--> 0 is V5() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V59() V60() V61() V62() V63() V64() V65() V66() Function-yielding V81() set
{(IC )} is non empty V5() 1 -element set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total V32({(IC )},{0}) V59() V60() V61() V62() Function-yielding V81() Element of K19(K20({(IC )},{0}))
{0} is non empty V5() functional 1 -element set
K20({(IC )},{0}) is Relation-like set
K19(K20({(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 K514(2,SCMPDS) -compatible K514(2,SCMPDS) -compatible total 0 -started set
sp is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
IExec (sp,P,(Initialize s)) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
stop sp is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() 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 V36() 1 -element V118() non halt-free V127( SCMPDS ) V128( SCMPDS ) paraclosed parahalting shiftable set
halt SCMPDS is V137(2, SCMPDS ) 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 V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
sp ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card sp is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom sp is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Stop SCMPDS),(card sp)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
sp +* (Shift ((Stop SCMPDS),(card sp))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
P +* (stop sp) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Result ((P +* (stop sp)),(Initialize s)) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
LifeSpan ((P +* (stop sp)),(Initialize s)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput ((P +* (stop sp)),(Initialize s),(LifeSpan ((P +* (stop sp)),(Initialize s)))) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
cv is Int-like Element of the carrier of SCMPDS
(IExec (sp,P,(Initialize s))) . cv is ext-real V14() V15() integer set
(Comput ((P +* (stop sp)),(Initialize s),(LifeSpan ((P +* (stop sp)),(Initialize s))))) . cv is ext-real V14() V15() integer set
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 K514(2,SCMPDS) -compatible total set
Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible V36() 0 -started set
(IC ) .--> 0 is V5() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V59() V60() V61() V62() V63() V64() V65() V66() Function-yielding V81() set
{(IC )} is non empty V5() 1 -element set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total V32({(IC )},{0}) V59() V60() V61() V62() Function-yielding V81() Element of K19(K20({(IC )},{0}))
{0} is non empty V5() functional 1 -element set
K20({(IC )},{0}) is Relation-like set
K19(K20({(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 K514(2,SCMPDS) -compatible K514(2,SCMPDS) -compatible total 0 -started set
sp is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() paraclosed parahalting set
IExec (sp,P,(Initialize s)) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
stop sp is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() 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 V36() 1 -element V118() non halt-free V127( SCMPDS ) V128( SCMPDS ) paraclosed parahalting shiftable set
halt SCMPDS is V137(2, SCMPDS ) 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 V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
sp ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card sp is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom sp is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Stop SCMPDS),(card sp)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
sp +* (Shift ((Stop SCMPDS),(card sp))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
P +* (stop sp) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Result ((P +* (stop sp)),(Initialize s)) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
LifeSpan ((P +* (stop sp)),(Initialize s)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput ((P +* (stop sp)),(Initialize s),(LifeSpan ((P +* (stop sp)),(Initialize s)))) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
cv is Int-like Element of the carrier of SCMPDS
(IExec (sp,P,(Initialize s))) . cv is ext-real V14() V15() integer set
(Comput ((P +* (stop sp)),(Initialize s),(LifeSpan ((P +* (stop sp)),(Initialize s))))) . cv is ext-real V14() V15() integer set
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 K514(2,SCMPDS) -compatible total 0 -started set
LifeSpan (P,s) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
sp is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
stop sp is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() 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 V36() 1 -element V118() non halt-free V127( SCMPDS ) V128( SCMPDS ) paraclosed parahalting shiftable set
halt SCMPDS is V137(2, SCMPDS ) 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 V5() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant V36() 1 -element V118() V128( SCMPDS ) set
sp ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() V118() set
card sp is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() Element of NAT
dom sp is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() set
Shift ((Stop SCMPDS),(card sp)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V36() set
sp +* (Shift ((Stop SCMPDS),(card sp))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like set
dom sp is ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal V47() V74() Element of K19(NAT)
cv is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
Comput (P,s,cv) is Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible total set
IC (Comput (P,s,cv)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V14() V15() integer V36() cardinal Element of NAT
(Comput (P,s,cv)) . (IC ) is set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K514(2,SCMPDS) -compatible V36() 0 -started set
(IC ) .--> 0 is V5() Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V59() V60() V61() V62() V63() V64() V65() V66() Function-yielding V81() set
{(IC )} is non empty V5() 1 -element set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total V32({(IC )},{0}) V59() V60() V61() V62() Function-yielding V81() Element of K19(K20({(IC )},{0}))
{0} is non empty V5() functional 1 -element set
K20({(IC )},{0}) is Relation-like set
K19(K20({(IC )},{0})) is set
P +* (stop sp) is non empty Relation-like NAT