:: SCMPDS_8 semantic presentation

REAL is non empty V43() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V43() countable denumerable Element of K32(REAL)
K32(REAL) is set
SCM is non empty with_non-empty_values IC-Ins-separated strict V103(2) AMI-Struct over 2
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
SCM-Memory is set
{NAT} is non empty V76() V77() set
K216() is set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
{1} is non empty countable V76() V77() Element of K32(NAT)
K32(NAT) is set
K66(NAT,REAL,{1},NAT) is Relation-like NAT -defined REAL -valued V33() V34() V35() Element of K32(K33(NAT,REAL))
K33(NAT,REAL) is Relation-like set
K32(K33(NAT,REAL)) is set
{NAT} \/ K216() is non empty set
K377(NAT,SCM-Memory) is Element of SCM-Memory
K217() is non empty set
SCM-OK is Relation-like SCM-Memory -defined 2 -valued Function-like total V30( SCM-Memory ,2) Element of K32(K33(SCM-Memory,2))
K33(SCM-Memory,2) is Relation-like set
K32(K33(SCM-Memory,2)) is set
SCM-VAL is non empty Relation-like 2 -defined Function-like total set
INT is non empty V43() set
K282(NAT,INT) is Relation-like NAT -defined Function-like T-Sequence-like V43() 2 -element countable V83() set
SCM-Exec is non empty Relation-like K217() -defined K133((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))) -valued Function-like total V30(K217(),K133((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL)))) Element of K32(K33(K217(),K133((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL)))))
SCM-OK (#) SCM-VAL is Relation-like SCM-Memory -defined Function-like total set
product (SCM-OK (#) SCM-VAL) is functional with_common_domain product-like set
K133((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))) is non empty functional set
K33(K217(),K133((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL)))) is Relation-like set
K32(K33(K217(),K133((product (SCM-OK (#) SCM-VAL)),(product (SCM-OK (#) SCM-VAL))))) is set
AMI-Struct(# SCM-Memory,K377(NAT,SCM-Memory),K217(),SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2
the carrier of SCM is set
the_Values_of SCM is Relation-like non-empty the carrier of SCM -defined Function-like total set
the Object-Kind of SCM is Relation-like the carrier of SCM -defined 2 -valued Function-like total V30( the carrier of SCM,2) Element of K32(K33( the carrier of SCM,2))
K33( the carrier of SCM,2) is Relation-like set
K32(K33( the carrier of SCM,2)) is set
the ValuesF of SCM is non empty Relation-like 2 -defined Function-like total set
the Object-Kind of SCM (#) the ValuesF of SCM is Relation-like the carrier of SCM -defined Function-like total set
NAT is non empty epsilon-transitive epsilon-connected ordinal V43() countable denumerable set
K32(NAT) is set
9 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
Segm 9 is countable Element of K32(NAT)
K32(SCM-Memory) is set
the InstructionsF of SCM is non empty Relation-like standard-ins V85() V86() V88() set
SCMPDS is non empty with_non-empty_values IC-Ins-separated strict strict V103(2) AMI-Struct over 2
the carrier of SCMPDS is set
the InstructionsF of SCMPDS is non empty Relation-like standard-ins V85() V86() V88() set
the_Values_of 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 total V30( the carrier of SCMPDS,2) Element of K32(K33( the carrier of SCMPDS,2))
K33( the carrier of SCMPDS,2) is Relation-like set
K32(K33( the carrier of SCMPDS,2)) is set
the ValuesF of SCMPDS is non empty Relation-like 2 -defined Function-like total set
the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS is Relation-like the carrier of SCMPDS -defined Function-like total set
COMPLEX is non empty V43() set
RAT is non empty V43() set
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
0 is empty Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() V28() V33() V34() V35() V36() Cardinal-yielding integer V83() Element of NAT
14 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
IC is Element of the carrier of SCMPDS
halt SCMPDS is V102(2, SCMPDS ) V113() Element of the InstructionsF of SCMPDS
halt the InstructionsF of SCMPDS is V87( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
5 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
6 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
K7(0,4,5,6,14) is set
SCM-Data-Loc is Element of K32(SCM-Memory)
P is Int-like Element of the carrier of SCMPDS
s is set
I is set
[s,I] is set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
intpos a is Int-like Element of the carrier of SCMPDS
dl. a is Int-like Element of the carrier of SCM
[1,a] is set
{0,4,5,6,14} is countable Element of K32(NAT)
P is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Initialize P is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V43() countable 0 -started set
K344((IC ),0) is V5() INT -valued V33() V34() V35() V36() set
{(IC )} is non empty set
K335({(IC )},0) is non empty Relation-like {(IC )} -defined INT -valued {0} -valued Function-like total V30({(IC )},{0}) V33() V34() V35() V36() Element of K32(K33({(IC )},{0}))
{0} is non empty functional with_common_domain set
K33({(IC )},{0}) is Relation-like set
K32(K33({(IC )},{0})) is set
P +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
s is Element of the InstructionsF of SCMPDS
InsCode s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer 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 the_Values_of SCMPDS -compatible total set
product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS) is functional with_common_domain product-like set
K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) is non empty functional set
the Execution of SCMPDS is non empty Relation-like the InstructionsF of SCMPDS -defined K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) -valued Function-like total V30( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))))) is set
the Execution of SCMPDS . s is Relation-like Function-like Element of K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . s) . P is set
Initialize (Exec (s,P)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
(Exec (s,P)) +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
DataPart (Exec (s,P)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
NonZero SCMPDS is Element of K32( the carrier of SCMPDS)
K32( the carrier of SCMPDS) is set
(Exec (s,P)) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
DataPart P is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of 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 the_Values_of SCMPDS -compatible set
product (the_Values_of SCMPDS) is non empty functional with_common_domain product-like set
K33((product (the_Values_of SCMPDS)),NAT) is Relation-like set
K32(K33((product (the_Values_of SCMPDS)),NAT)) is set
P is Int-like Element of the carrier of SCMPDS
s is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
s . P is ext-real V27() V28() integer set
I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
s is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
s . P is ext-real V27() V28() integer set
I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
s is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
s . P is ext-real V27() V28() integer set
s is non empty Relation-like product (the_Values_of SCMPDS) -defined NAT -valued Function-like total V30( product (the_Values_of SCMPDS), NAT ) V33() V34() V35() V36() Element of K32(K33((product (the_Values_of SCMPDS)),NAT))
I is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
s . I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
a is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total Element of product (the_Values_of SCMPDS)
s . a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
i is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
i . P is ext-real V27() V28() integer set
I is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
s . I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
I . P is ext-real V27() V28() integer set
a is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
a . P is ext-real V27() V28() integer set
P is Int-like Element of the carrier of SCMPDS
s is ext-real V27() V28() integer set
I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card I) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
(P,s) >=0_goto ((card I) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((P,s) >=0_goto ((card I) + 2)) ';' I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(card I) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card I) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card I) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((P,s) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
s is Int-like Element of the carrier of SCMPDS
I is ext-real V27() V28() integer set
P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() shiftable set
(s,I,P) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom P is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card P) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
(s,I) >=0_goto ((card P) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((s,I) >=0_goto ((card P) + 2)) ';' P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(card P) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card P) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card P) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((s,I) >=0_goto ((card P) + 2)) ';' P) ';' (goto (- ((card P) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
Load ((s,I) >=0_goto ((card P) + 2)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() 1 -element countable V83() halt-free V93( SCMPDS ) set
(Load ((s,I) >=0_goto ((card P) + 2))) ';' P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card ((Load ((s,I) >=0_goto ((card P) + 2))) ';' P) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom ((Load ((s,I) >=0_goto ((card P) + 2))) ';' P) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card ((Load ((s,I) >=0_goto ((card P) + 2))) ';' P)) + (- ((card P) + 1)) is ext-real V27() V28() integer set
s is Int-like Element of the carrier of SCMPDS
I is ext-real V27() V28() integer set
P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() halt-free V93( SCMPDS ) set
(s,I,P) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom P is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card P) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
(s,I) >=0_goto ((card P) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((s,I) >=0_goto ((card P) + 2)) ';' P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() halt-free V93( SCMPDS ) set
(card P) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card P) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card P) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((s,I) >=0_goto ((card P) + 2)) ';' P) ';' (goto (- ((card P) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() halt-free V93( SCMPDS ) set
P is Int-like Element of the carrier of SCMPDS
s is ext-real V27() V28() integer set
I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(P,s,I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card I) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
(P,s) >=0_goto ((card I) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((P,s) >=0_goto ((card I) + 2)) ';' I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(card I) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card I) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card I) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((P,s) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card (P,s,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom (P,s,I) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
card (((P,s) >=0_goto ((card I) + 2)) ';' I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom (((P,s) >=0_goto ((card I) + 2)) ';' I) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card (((P,s) >=0_goto ((card I) + 2)) ';' I)) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
((card I) + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
P is Int-like Element of the carrier of SCMPDS
s is ext-real V27() V28() integer set
I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(P,s,I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card I) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
(P,s) >=0_goto ((card I) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((P,s) >=0_goto ((card I) + 2)) ';' I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(card I) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card I) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card I) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((P,s) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
stop (P,s,I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
K302(SCMPDS) is non empty V5() Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant T-Sequence-like V43() countable V83() non halt-free V92( SCMPDS ) V93( SCMPDS ) paraclosed parahalting shiftable set
Load is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() 1 -element countable V83() set
(P,s,I) ';' K302(SCMPDS) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card (stop (P,s,I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom (stop (P,s,I)) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card I) + 3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
card (P,s,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom (P,s,I) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card (P,s,I)) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
((card I) + 2) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
P is Int-like Element of the carrier of SCMPDS
s is ext-real V27() V28() integer set
I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
a is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom a is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card a) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
(P,s,a) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(P,s) >=0_goto ((card a) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((P,s) >=0_goto ((card a) + 2)) ';' a is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(card a) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card a) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card a) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((P,s) >=0_goto ((card a) + 2)) ';' a) ';' (goto (- ((card a) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
dom (P,s,a) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
card (P,s,a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
P is Int-like Element of the carrier of SCMPDS
s is ext-real V27() V28() integer set
I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(P,s,I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card I) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
(P,s) >=0_goto ((card I) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((P,s) >=0_goto ((card I) + 2)) ';' I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(card I) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card I) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card I) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((P,s) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(P,s,I) . 0 is set
(P,s,I) . ((card I) + 1) is set
I ';' (goto (- ((card I) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
((P,s) >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card (((P,s) >=0_goto ((card I) + 2)) ';' I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom (((P,s) >=0_goto ((card I) + 2)) ';' I) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() 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 the_Values_of SCMPDS -compatible total set
I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
a is Int-like Element of the carrier of SCMPDS
s . a is ext-real V27() V28() integer set
i is ext-real V27() V28() integer set
DataLoc ((s . a),i) is Int-like Element of the carrier of SCMPDS
s . (DataLoc ((s . a),i)) is ext-real V27() V28() integer set
(a,i,I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card I) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
(a,i) >=0_goto ((card I) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((a,i) >=0_goto ((card I) + 2)) ';' I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(card I) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card I) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card I) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
stop (a,i,I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
K302(SCMPDS) is non empty V5() Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant T-Sequence-like V43() countable V83() non halt-free V92( SCMPDS ) V93( SCMPDS ) paraclosed parahalting shiftable set
Load is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() 1 -element countable V83() set
(a,i,I) ';' K302(SCMPDS) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
Initialize s is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V43() countable 0 -started set
K344((IC ),0) is V5() INT -valued V33() V34() V35() V36() set
{(IC )} is non empty set
K335({(IC )},0) is non empty Relation-like {(IC )} -defined INT -valued {0} -valued Function-like total V30({(IC )},{0}) V33() V34() V35() V36() Element of K32(K33({(IC )},{0}))
{0} is non empty functional with_common_domain set
K33({(IC )},{0}) is Relation-like set
K32(K33({(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 the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
P +* (stop (a,i,I)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Comput ((P +* (stop (a,i,I))),(Initialize s),1) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Initialize s) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
(Initialize s) . (IC ) is set
dom (Start-At (0,SCMPDS)) is non empty set
(Initialize s) . a is ext-real V27() V28() integer set
DataLoc (((Initialize s) . a),i) is Int-like Element of the carrier of SCMPDS
(Initialize s) . (DataLoc (((Initialize s) . a),i)) is ext-real V27() V28() integer set
(Initialize s) . (DataLoc ((s . a),i)) is ext-real V27() V28() integer set
I ';' (goto (- ((card I) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
((a,i) >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
Comput ((P +* (stop (a,i,I))),(Initialize s),(0 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Comput ((P +* (stop (a,i,I))),(Initialize s),0) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Following ((P +* (stop (a,i,I))),(Comput ((P +* (stop (a,i,I))),(Initialize s),0))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
CurInstr ((P +* (stop (a,i,I))),(Comput ((P +* (stop (a,i,I))),(Initialize s),0))) is Element of the InstructionsF of SCMPDS
IC (Comput ((P +* (stop (a,i,I))),(Initialize s),0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
(Comput ((P +* (stop (a,i,I))),(Initialize s),0)) . (IC ) is set
(P +* (stop (a,i,I))) /. (IC (Comput ((P +* (stop (a,i,I))),(Initialize s),0))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr ((P +* (stop (a,i,I))),(Comput ((P +* (stop (a,i,I))),(Initialize s),0)))),(Comput ((P +* (stop (a,i,I))),(Initialize s),0))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS) is functional with_common_domain product-like set
K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) is non empty functional set
the Execution of SCMPDS is non empty Relation-like the InstructionsF of SCMPDS -defined K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) -valued Function-like total V30( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))))) is set
the Execution of SCMPDS . (CurInstr ((P +* (stop (a,i,I))),(Comput ((P +* (stop (a,i,I))),(Initialize s),0)))) is Relation-like Function-like Element of K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . (CurInstr ((P +* (stop (a,i,I))),(Comput ((P +* (stop (a,i,I))),(Initialize s),0))))) . (Comput ((P +* (stop (a,i,I))),(Initialize s),0)) is set
Following ((P +* (stop (a,i,I))),(Initialize s)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
CurInstr ((P +* (stop (a,i,I))),(Initialize s)) is Element of the InstructionsF of SCMPDS
(P +* (stop (a,i,I))) /. (IC (Initialize s)) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr ((P +* (stop (a,i,I))),(Initialize s))),(Initialize s)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
the Execution of SCMPDS . (CurInstr ((P +* (stop (a,i,I))),(Initialize s))) is Relation-like Function-like Element of K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . (CurInstr ((P +* (stop (a,i,I))),(Initialize s)))) . (Initialize s) is set
Exec (((a,i) >=0_goto ((card I) + 2)),(Initialize s)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
the Execution of SCMPDS . ((a,i) >=0_goto ((card I) + 2)) is Relation-like Function-like Element of K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . ((a,i) >=0_goto ((card I) + 2))) . (Initialize s) is set
IC (Comput ((P +* (stop (a,i,I))),(Initialize s),1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
(Comput ((P +* (stop (a,i,I))),(Initialize s),1)) . (IC ) is set
ICplusConst ((Initialize s),((card I) + 2)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
0 + ((card I) + 2) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
card (a,i,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom (a,i,I) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
dom (stop (a,i,I)) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(P +* (stop (a,i,I))) . ((card I) + 2) is Element of the InstructionsF of SCMPDS
(stop (a,i,I)) . ((card I) + 2) is set
CurInstr ((P +* (stop (a,i,I))),(Comput ((P +* (stop (a,i,I))),(Initialize s),1))) is Element of the InstructionsF of SCMPDS
(P +* (stop (a,i,I))) /. (IC (Comput ((P +* (stop (a,i,I))),(Initialize s),1))) is Element of the InstructionsF of SCMPDS
t1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
1 + 0 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
Comput ((P +* (stop (a,i,I))),(Initialize s),t1) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput ((P +* (stop (a,i,I))),(Initialize s),t1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
(Comput ((P +* (stop (a,i,I))),(Initialize s),t1)) . (IC ) is set
t1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
Comput ((P +* (stop (a,i,I))),(Initialize s),t1) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput ((P +* (stop (a,i,I))),(Initialize s),t1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
(Comput ((P +* (stop (a,i,I))),(Initialize s),t1)) . (IC ) is set
t1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
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 the_Values_of SCMPDS -compatible total 0 -started set
I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card I) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
Start-At (((card I) + 2),SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V43() countable (card I) + 2 -started set
K344((IC ),((card I) + 2)) is V5() INT -valued V33() V34() V35() V36() set
{(IC )} is non empty set
K335({(IC )},((card I) + 2)) is non empty Relation-like non-empty non empty-yielding {(IC )} -defined INT -valued {((card I) + 2)} -valued Function-like total V30({(IC )},{((card I) + 2)}) V33() V34() V35() V36() Element of K32(K33({(IC )},{((card I) + 2)}))
{((card I) + 2)} is non empty V76() V77() set
K33({(IC )},{((card I) + 2)}) is Relation-like set
K32(K33({(IC )},{((card I) + 2)})) is set
s +* (Start-At (((card I) + 2),SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total (card I) + 2 -started set
a is Int-like Element of the carrier of SCMPDS
s . a is ext-real V27() V28() integer set
c is ext-real V27() V28() integer set
DataLoc ((s . a),c) is Int-like Element of the carrier of SCMPDS
s . (DataLoc ((s . a),c)) is ext-real V27() V28() integer set
(a,c,I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(a,c) >=0_goto ((card I) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((a,c) >=0_goto ((card I) + 2)) ';' I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(card I) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card I) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card I) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((a,c) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
IExec ((a,c,I),P,s) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
stop (a,c,I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
K302(SCMPDS) is non empty V5() Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant T-Sequence-like V43() countable V83() non halt-free V92( SCMPDS ) V93( SCMPDS ) paraclosed parahalting shiftable set
Load is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() 1 -element countable V83() set
(a,c,I) ';' K302(SCMPDS) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
P +* (stop (a,c,I)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Comput ((P +* (stop (a,c,I))),s,1) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Initialize s is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V43() countable 0 -started set
K344((IC ),0) is V5() INT -valued V33() V34() V35() V36() set
K335({(IC )},0) is non empty Relation-like {(IC )} -defined INT -valued {0} -valued Function-like total V30({(IC )},{0}) V33() V34() V35() V36() Element of K32(K33({(IC )},{0}))
{0} is non empty functional with_common_domain set
K33({(IC )},{0}) is Relation-like set
K32(K33({(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 the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
IC s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
s . (IC ) is set
I ';' (goto (- ((card I) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
((a,c) >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
CurInstr ((P +* (stop (a,c,I))),s) is Element of the InstructionsF of SCMPDS
(P +* (stop (a,c,I))) /. (IC s) is Element of the InstructionsF of SCMPDS
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
Comput ((P +* (stop (a,c,I))),s,(0 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Comput ((P +* (stop (a,c,I))),s,0) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Following ((P +* (stop (a,c,I))),(Comput ((P +* (stop (a,c,I))),s,0))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
CurInstr ((P +* (stop (a,c,I))),(Comput ((P +* (stop (a,c,I))),s,0))) is Element of the InstructionsF of SCMPDS
IC (Comput ((P +* (stop (a,c,I))),s,0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
(Comput ((P +* (stop (a,c,I))),s,0)) . (IC ) is set
(P +* (stop (a,c,I))) /. (IC (Comput ((P +* (stop (a,c,I))),s,0))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr ((P +* (stop (a,c,I))),(Comput ((P +* (stop (a,c,I))),s,0)))),(Comput ((P +* (stop (a,c,I))),s,0))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS) is functional with_common_domain product-like set
K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) is non empty functional set
the Execution of SCMPDS is non empty Relation-like the InstructionsF of SCMPDS -defined K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) -valued Function-like total V30( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))))) is set
the Execution of SCMPDS . (CurInstr ((P +* (stop (a,c,I))),(Comput ((P +* (stop (a,c,I))),s,0)))) is Relation-like Function-like Element of K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . (CurInstr ((P +* (stop (a,c,I))),(Comput ((P +* (stop (a,c,I))),s,0))))) . (Comput ((P +* (stop (a,c,I))),s,0)) is set
Following ((P +* (stop (a,c,I))),s) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Exec ((CurInstr ((P +* (stop (a,c,I))),s)),s) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
the Execution of SCMPDS . (CurInstr ((P +* (stop (a,c,I))),s)) is Relation-like Function-like Element of K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . (CurInstr ((P +* (stop (a,c,I))),s))) . s is set
Exec (((a,c) >=0_goto ((card I) + 2)),s) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
the Execution of SCMPDS . ((a,c) >=0_goto ((card I) + 2)) is Relation-like Function-like Element of K133((product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),(product ( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))
( the Execution of SCMPDS . ((a,c) >=0_goto ((card I) + 2))) . s is set
Result ((P +* (stop (a,c,I))),s) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput ((P +* (stop (a,c,I))),s,1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
(Comput ((P +* (stop (a,c,I))),s,1)) . (IC ) is set
ICplusConst (s,((card I) + 2)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
0 + ((card I) + 2) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
card (a,c,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom (a,c,I) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
dom (stop (a,c,I)) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(P +* (stop (a,c,I))) . ((card I) + 2) is Element of the InstructionsF of SCMPDS
(stop (a,c,I)) . ((card I) + 2) is set
CurInstr ((P +* (stop (a,c,I))),(Comput ((P +* (stop (a,c,I))),s,1))) is Element of the InstructionsF of SCMPDS
(P +* (stop (a,c,I))) /. (IC (Comput ((P +* (stop (a,c,I))),s,1))) is Element of the InstructionsF of SCMPDS
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
Comput ((P +* (stop (a,c,I))),s,v) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
CurInstr ((P +* (stop (a,c,I))),(Comput ((P +* (stop (a,c,I))),s,v))) is Element of the InstructionsF of SCMPDS
IC (Comput ((P +* (stop (a,c,I))),s,v)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
(Comput ((P +* (stop (a,c,I))),s,v)) . (IC ) is set
(P +* (stop (a,c,I))) /. (IC (Comput ((P +* (stop (a,c,I))),s,v))) is Element of the InstructionsF of SCMPDS
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
Comput ((P +* (stop (a,c,I))),s,v) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
CurInstr ((P +* (stop (a,c,I))),(Comput ((P +* (stop (a,c,I))),s,v))) is Element of the InstructionsF of SCMPDS
IC (Comput ((P +* (stop (a,c,I))),s,v)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
(Comput ((P +* (stop (a,c,I))),s,v)) . (IC ) is set
(P +* (stop (a,c,I))) /. (IC (Comput ((P +* (stop (a,c,I))),s,v))) is Element of the InstructionsF of SCMPDS
LifeSpan ((P +* (stop (a,c,I))),s) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom (Start-At (((card I) + 2),SCMPDS)) is non empty set
v is set
dom (IExec ((a,c,I),P,s)) is set
(IExec ((a,c,I),P,s)) . v is set
(Comput ((P +* (stop (a,c,I))),s,1)) . v is set
s . v is set
(s +* (Start-At (((card I) + 2),SCMPDS))) . v is set
(IExec ((a,c,I),P,s)) . v is set
(s +* (Start-At (((card I) + 2),SCMPDS))) . v is set
dom (s +* (Start-At (((card I) + 2),SCMPDS))) is non empty 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 the_Values_of SCMPDS -compatible total 0 -started set
I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card I) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
a is Int-like Element of the carrier of SCMPDS
s . a is ext-real V27() V28() integer set
i is ext-real V27() V28() integer set
DataLoc ((s . a),i) is Int-like Element of the carrier of SCMPDS
s . (DataLoc ((s . a),i)) is ext-real V27() V28() integer set
(a,i,I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(a,i) >=0_goto ((card I) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((a,i) >=0_goto ((card I) + 2)) ';' I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(card I) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card I) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card I) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
IExec ((a,i,I),P,s) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (IExec ((a,i,I),P,s)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
(IExec ((a,i,I),P,s)) . (IC ) is set
Start-At (((card I) + 2),SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V43() countable (card I) + 2 -started set
K344((IC ),((card I) + 2)) is V5() INT -valued V33() V34() V35() V36() set
{(IC )} is non empty set
K335({(IC )},((card I) + 2)) is non empty Relation-like non-empty non empty-yielding {(IC )} -defined INT -valued {((card I) + 2)} -valued Function-like total V30({(IC )},{((card I) + 2)}) V33() V34() V35() V36() Element of K32(K33({(IC )},{((card I) + 2)}))
{((card I) + 2)} is non empty V76() V77() set
K33({(IC )},{((card I) + 2)}) is Relation-like set
K32(K33({(IC )},{((card I) + 2)})) is set
s +* (Start-At (((card I) + 2),SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total (card I) + 2 -started 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 the_Values_of SCMPDS -compatible total 0 -started set
I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
a is Int-like Element of the carrier of SCMPDS
s . a is ext-real V27() V28() integer set
i is Int-like Element of the carrier of SCMPDS
s . i is ext-real V27() V28() integer set
c is ext-real V27() V28() integer set
DataLoc ((s . a),c) is Int-like Element of the carrier of SCMPDS
s . (DataLoc ((s . a),c)) is ext-real V27() V28() integer set
(a,c,I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom I is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card I) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
(a,c) >=0_goto ((card I) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((a,c) >=0_goto ((card I) + 2)) ';' I is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(card I) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card I) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card I) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((a,c) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
IExec ((a,c,I),P,s) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
(IExec ((a,c,I),P,s)) . i is ext-real V27() V28() integer set
Start-At (((card I) + 2),SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V43() countable (card I) + 2 -started set
K344((IC ),((card I) + 2)) is V5() INT -valued V33() V34() V35() V36() set
{(IC )} is non empty set
K335({(IC )},((card I) + 2)) is non empty Relation-like non-empty non empty-yielding {(IC )} -defined INT -valued {((card I) + 2)} -valued Function-like total V30({(IC )},{((card I) + 2)}) V33() V34() V35() V36() Element of K32(K33({(IC )},{((card I) + 2)}))
{((card I) + 2)} is non empty V76() V77() set
K33({(IC )},{((card I) + 2)}) is Relation-like set
K32(K33({(IC )},{((card I) + 2)})) is set
s +* (Start-At (((card I) + 2),SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total (card I) + 2 -started set
dom (Start-At (((card I) + 2),SCMPDS)) is non empty set
P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
Shift (P,1) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V43() countable set
s is Int-like Element of the carrier of SCMPDS
I is ext-real V27() V28() integer set
(s,I,P) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom P is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card P) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
(s,I) >=0_goto ((card P) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((s,I) >=0_goto ((card P) + 2)) ';' P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
(card P) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card P) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card P) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((s,I) >=0_goto ((card P) + 2)) ';' P) ';' (goto (- ((card P) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
Load (goto (- ((card P) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() 1 -element countable V83() halt-free V93( SCMPDS ) set
(((s,I) >=0_goto ((card P) + 2)) ';' P) ';' (Load (goto (- ((card P) + 1)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
Load ((s,I) >=0_goto ((card P) + 2)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() 1 -element countable V83() halt-free V93( SCMPDS ) set
(Load ((s,I) >=0_goto ((card P) + 2))) ';' P is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
((Load ((s,I) >=0_goto ((card P) + 2))) ';' P) ';' (Load (goto (- ((card P) + 1)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
card (Load ((s,I) >=0_goto ((card P) + 2))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom (Load ((s,I) >=0_goto ((card P) + 2))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
F₂() is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
F₅() is Int-like Element of the carrier of SCMPDS
F₂() . F₅() is ext-real V27() V28() integer set
F₆() is ext-real V27() V28() integer set
DataLoc ((F₂() . F₅()),F₆()) is Int-like Element of the carrier of SCMPDS
F₄() is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() halt-free V93( SCMPDS ) shiftable set
(F₅(),F₆(),F₄()) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() halt-free V93( SCMPDS ) shiftable set
card F₄() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
dom F₄() is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
(card F₄()) + 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
(F₅(),F₆()) >=0_goto ((card F₄()) + 2) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
((F₅(),F₆()) >=0_goto ((card F₄()) + 2)) ';' F₄() is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() halt-free V93( SCMPDS ) set
(card F₄()) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
- ((card F₄()) + 1) is ext-real non positive V27() V28() integer set
goto (- ((card F₄()) + 1)) is V89( the InstructionsF of SCMPDS) Element of the InstructionsF of SCMPDS
(((F₅(),F₆()) >=0_goto ((card F₄()) + 2)) ';' F₄()) ';' (goto (- ((card F₄()) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() halt-free V93( SCMPDS ) set
F₃() is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
stop (F₅(),F₆(),F₄()) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() V93( SCMPDS ) shiftable set
K302(SCMPDS) is non empty V5() Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like constant T-Sequence-like V43() countable V83() non halt-free V92( SCMPDS ) V93( SCMPDS ) paraclosed parahalting shiftable set
Load is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() 1 -element countable V83() set
(F₅(),F₆(),F₄()) ';' K302(SCMPDS) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
stop F₄() is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() V93( SCMPDS ) shiftable set
F₄() ';' K302(SCMPDS) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() set
X is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
X + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
b is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
F₁(b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
b . F₅() is ext-real V27() V28() integer set
b is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Initialize b is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible V43() countable 0 -started set
K344((IC ),0) is V5() INT -valued V33() V34() V35() V36() set
{(IC )} is non empty set
K335({(IC )},0) is non empty Relation-like {(IC )} -defined INT -valued {0} -valued Function-like total V30({(IC )},{0}) V33() V34() V35() V36() Element of K32(K33({(IC )},{0}))
{0} is non empty functional with_common_domain set
K33({(IC )},{0}) is Relation-like set
K32(K33({(IC )},{0})) is set
b +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible the_Values_of SCMPDS -compatible total 0 -started set
b . (DataLoc ((F₂() . F₅()),F₆())) is ext-real V27() V28() integer set
b . (DataLoc ((F₂() . F₅()),F₆())) is ext-real V27() V28() integer set
dom (stop (F₅(),F₆(),F₄())) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
F₄() ';' (goto (- ((card F₄()) + 1))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() halt-free V93( SCMPDS ) set
((F₅(),F₆()) >=0_goto ((card F₄()) + 2)) ';' (F₄() ';' (goto (- ((card F₄()) + 1)))) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like T-Sequence-like V43() countable V83() halt-free V93( SCMPDS ) set
b +* (stop F₄()) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
b +* (stop (F₅(),F₆(),F₄())) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Comput ((b +* (stop (F₅(),F₆(),F₄()))),b,1) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
LifeSpan ((b +* (stop F₄())),b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
Comput ((b +* (stop (F₅(),F₆(),F₄()))),(Comput ((b +* (stop (F₅(),F₆(),F₄()))),b,1)),(LifeSpan ((b +* (stop F₄())),b))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer Element of NAT
b . (IC ) is set
(LifeSpan ((b +* (stop F₄())),b)) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
Comput ((b +* (stop (F₅(),F₆(),F₄()))),b,((LifeSpan ((b +* (stop F₄())),b)) + 1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
((LifeSpan ((b +* (stop F₄())),b)) + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
Comput ((b +* (stop (F₅(),F₆(),F₄()))),b,(((LifeSpan ((b +* (stop F₄())),b)) + 1) + 1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
dom (F₅(),F₆(),F₄()) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() V124() set
Shift (F₄(),1) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V43() countable set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() integer V76() Element of NAT
Comput ((b +* (stop (F₅(),F₆(),F₄())