:: SCMPDS_6 semantic presentation

REAL is set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)

K6(REAL) is set

COMPLEX is set

NAT is non empty epsilon-transitive epsilon-connected ordinal set

K6(NAT) is set

9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

Segm 9 is Element of K6(NAT)

K161() is set

SCM-Memory is set

K6(SCM-Memory) is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

K7(SCM-Memory,2) is Relation-like set

K6(K7(SCM-Memory,2)) is set

SCM-OK is Relation-like Function-like V29( SCM-Memory ,2) Element of K6(K7(SCM-Memory,2))

SCM-VAL is Relation-like 2 -defined Function-like total set

SCM-OK (#) SCM-VAL is Relation-like set

K150((SCM-OK (#) SCM-VAL)) is set

K162() is non empty set

K130(K150((SCM-OK (#) SCM-VAL)),K150((SCM-OK (#) SCM-VAL))) is set

K7(K162(),K130(K150((SCM-OK (#) SCM-VAL)),K150((SCM-OK (#) SCM-VAL)))) is Relation-like set

K6(K7(K162(),K130(K150((SCM-OK (#) SCM-VAL)),K150((SCM-OK (#) SCM-VAL))))) is set

K6(NAT) is set

SCMPDS is non empty V83(2) IC-Ins-separated strict strict V91(2) AMI-Struct over 2

the carrier of SCMPDS is set

the InstructionsF of SCMPDS is non empty Relation-like standard-ins V73() J/A-independent V76() set

K282(2,SCMPDS) is Relation-like non-empty the carrier of SCMPDS -defined Function-like total set

the Object-Kind of SCMPDS is Relation-like Function-like V29( the carrier of SCMPDS,2) Element of K6(K7( the carrier of SCMPDS,2))

K7( the carrier of SCMPDS,2) is Relation-like set

K6(K7( the carrier of SCMPDS,2)) is set

the U7 of SCMPDS is Relation-like 2 -defined Function-like total set

the Object-Kind of SCMPDS (#) the U7 of SCMPDS is Relation-like set

RAT is set

INT is set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding ext-real non positive non negative Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

6 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

IC is Element of the carrier of SCMPDS

K503(NAT,0) is non empty Element of K6(NAT)

SCM-Data-Loc is Element of K6(SCM-Memory)

Stop SCMPDS is non empty V2() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() V71() non halt-free V80( SCMPDS ) V81( SCMPDS ) paraclosed parahalting shiftable set

halt SCMPDS is parahalting Element of the InstructionsF of SCMPDS

halt the InstructionsF of SCMPDS is ins-loc-free Element of the InstructionsF of SCMPDS

Load is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set

(Stop SCMPDS) . 0 is set

dom (Stop SCMPDS) is non empty V2() epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

P is Element of the InstructionsF of SCMPDS

s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

P ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

Load P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set

(Load P) ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card (Load P) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (Load P) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift (s,(card (Load P))) is Relation-like Function-like set

(Load P) +* (Shift (s,(card (Load P)))) is non empty Relation-like Function-like set

card (P ';' s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (P ';' s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

card s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom s is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

(card s) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

card ((Load P) ';' s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom ((Load P) ';' s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

(card (Load P)) + (card s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

P is Element of the InstructionsF of SCMPDS

s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

P ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

Load P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set

(Load P) ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card (Load P) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (Load P) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift (s,(card (Load P))) is Relation-like Function-like set

(Load P) +* (Shift (s,(card (Load P)))) is non empty Relation-like Function-like set

(P ';' s) . 0 is set

(Load P) . 0 is set

P is Element of the InstructionsF of SCMPDS

s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set

K332((IC ),0) is V2() set

{(IC )} is non empty set

K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))

{0} is non empty set

K7({(IC )},{0}) is Relation-like set

K6(K7({(IC )},{0})) is set

s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

P ';' I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

Load P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set

(Load P) ';' I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card (Load P) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (Load P) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift (I,(card (Load P))) is Relation-like Function-like set

(Load P) +* (Shift (I,(card (Load P)))) is non empty Relation-like Function-like set

stop (P ';' I) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

(P ';' I) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card (P ';' I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (P ';' I) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card (P ';' I))) is Relation-like Function-like set

(P ';' I) +* (Shift ((Stop SCMPDS),(card (P ';' I)))) is non empty Relation-like Function-like set

a is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

a +* (stop (P ';' I)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

CurInstr ((a +* (stop (P ';' I))),(Initialize s)) is Element of the InstructionsF of SCMPDS

IC (Initialize s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Initialize s) . (IC ) is set

(a +* (stop (P ';' I))) /. (IC (Initialize s)) is Element of the InstructionsF of SCMPDS

card I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom I is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

(card I) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

dom (stop (P ';' I)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

(a +* (stop (P ';' I))) . (IC (Initialize s)) is Element of the InstructionsF of SCMPDS

(a +* (stop (P ';' I))) . 0 is Element of the InstructionsF of SCMPDS

(stop (P ';' I)) . 0 is set

(P ';' I) . 0 is set

((Load P) ';' I) . 0 is set

(Load P) . 0 is set

P is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IC P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

P . (IC ) is set

s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

ICplusConst (P,I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

s + I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

a + I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

abs (a + I) is V11() V12() ext-real Element of REAL

s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

stop s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

s ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom s is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card s)) is Relation-like Function-like set

s +* (Shift ((Stop SCMPDS),(card s))) is non empty Relation-like Function-like set

P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom P is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((stop s),(card P)) is Relation-like Function-like set

P ';' s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

Shift (s,(card P)) is Relation-like Function-like set

P +* (Shift (s,(card P))) is non empty Relation-like Function-like set

stop (P ';' s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

(P ';' s) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card (P ';' s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (P ';' s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card (P ';' s))) is Relation-like Function-like set

(P ';' s) +* (Shift ((Stop SCMPDS),(card (P ';' s)))) is non empty Relation-like Function-like set

(P ';' s) ';' (Stop SCMPDS) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

s ';' (Stop SCMPDS) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

P ';' (s ';' (Stop SCMPDS)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

Shift ((s ';' (Stop SCMPDS)),(card P)) is Relation-like Function-like set

P +* (Shift ((s ';' (Stop SCMPDS)),(card P))) is non empty Relation-like Function-like set

P ';' (stop s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

P +* (Shift ((stop s),(card P))) is non empty Relation-like Function-like set

P is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

I is No-StopCode parahalting Element of the InstructionsF of SCMPDS

Exec (I,s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set

K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set

the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))

K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set

K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set

K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,I) is Element of K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))

K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,I) . s is set

Initialize (Exec (I,s)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set

K332((IC ),0) is V2() set

{(IC )} is non empty set

K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))

{0} is non empty set

K7({(IC )},{0}) is Relation-like set

K6(K7({(IC )},{0})) is set

(Exec (I,s)) +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() paraclosed parahalting shiftable set

I ';' a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() paraclosed parahalting set

Load I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() halt-free V81( SCMPDS ) set

(Load I) ';' a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card (Load I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (Load I) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift (a,(card (Load I))) is Relation-like Function-like set

(Load I) +* (Shift (a,(card (Load I)))) is non empty Relation-like Function-like set

IExec ((I ';' a),P,s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

stop (I ';' a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

(I ';' a) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card (I ';' a) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (I ';' a) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card (I ';' a))) is Relation-like Function-like set

(I ';' a) +* (Shift ((Stop SCMPDS),(card (I ';' a)))) is non empty Relation-like Function-like set

P +* (stop (I ';' a)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

Result ((P +* (stop (I ';' a))),s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IExec (a,P,(Initialize (Exec (I,s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

stop a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() V71() shiftable set

a ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom a is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card a)) is Relation-like Function-like set

a +* (Shift ((Stop SCMPDS),(card a))) is non empty Relation-like Function-like set

P +* (stop a) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

Result ((P +* (stop a)),(Initialize (Exec (I,s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

b is Int-like Element of the carrier of SCMPDS

(IExec ((I ';' a),P,s)) . b is V11() V12() integer ext-real set

(IExec (a,P,(Initialize (Exec (I,s))))) . b is V11() V12() integer ext-real set

IExec (((Load I) ';' a),P,s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

stop ((Load I) ';' a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

((Load I) ';' a) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card ((Load I) ';' a) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom ((Load I) ';' a) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card ((Load I) ';' a))) is Relation-like Function-like set

((Load I) ';' a) +* (Shift ((Stop SCMPDS),(card ((Load I) ';' a)))) is non empty Relation-like Function-like set

P +* (stop ((Load I) ';' a)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

Result ((P +* (stop ((Load I) ';' a))),s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

(IExec (((Load I) ';' a),P,s)) . b is V11() V12() integer ext-real set

IExec ((Load I),P,s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

stop (Load I) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() V81( SCMPDS ) set

(Load I) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

Shift ((Stop SCMPDS),(card (Load I))) is Relation-like Function-like set

(Load I) +* (Shift ((Stop SCMPDS),(card (Load I)))) is non empty Relation-like Function-like set

P +* (stop (Load I)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

Result ((P +* (stop (Load I))),s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Initialize (IExec ((Load I),P,s)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

(IExec ((Load I),P,s)) +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

IExec (a,P,(Initialize (IExec ((Load I),P,s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Result ((P +* (stop a)),(Initialize (IExec ((Load I),P,s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

(IExec (a,P,(Initialize (IExec ((Load I),P,s))))) . b is V11() V12() integer ext-real set

InsCode (halt SCMPDS) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of InsCodes the InstructionsF of SCMPDS

InsCodes the InstructionsF of SCMPDS is non empty set

P is Int-like Element of the carrier of SCMPDS

s is V11() V12() integer ext-real set

I is V11() V12() integer ext-real set

(P,s) <>0_goto I is No-StopCode Element of the InstructionsF of SCMPDS

InsCode (halt SCMPDS) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of InsCodes the InstructionsF of SCMPDS

InsCodes the InstructionsF of SCMPDS is non empty set

P is Int-like Element of the carrier of SCMPDS

s is V11() V12() integer ext-real set

I is V11() V12() integer ext-real set

(P,s) <=0_goto I is No-StopCode Element of the InstructionsF of SCMPDS

InsCode (halt SCMPDS) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of InsCodes the InstructionsF of SCMPDS

InsCodes the InstructionsF of SCMPDS is non empty set

P is Int-like Element of the carrier of SCMPDS

s is V11() V12() integer ext-real set

I is V11() V12() integer ext-real set

(P,s) >=0_goto I is No-StopCode Element of the InstructionsF of SCMPDS

P is V11() V12() integer ext-real set

goto P is Element of the InstructionsF of SCMPDS

Load (goto P) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set

P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

goto (P + 1) is Element of the InstructionsF of SCMPDS

- (P + 1) is V11() V12() integer ext-real non positive set

goto (- (P + 1)) is Element of the InstructionsF of SCMPDS

P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

((P + 1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

goto (P + 1) is No-StopCode Element of the InstructionsF of SCMPDS

Load (goto (P + 1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() halt-free V81( SCMPDS ) set

- (P + 1) is V11() V12() integer ext-real non positive set

((- (P + 1))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

goto (- (P + 1)) is No-StopCode Element of the InstructionsF of SCMPDS

Load (goto (- (P + 1))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() halt-free V81( SCMPDS ) set

P is V11() V12() integer ext-real set

(P) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

goto P is Element of the InstructionsF of SCMPDS

Load (goto P) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set

dom (P) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

s is V11() V12() integer ext-real set

(s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

goto s is Element of the InstructionsF of SCMPDS

Load (goto s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like V32() 1 -element V71() set

(s) . 0 is set

P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

stop P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

P ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom P is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card P)) is Relation-like Function-like set

P +* (Shift ((Stop SCMPDS),(card P))) is non empty Relation-like Function-like set

I is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

I +* (stop P) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set

K332((IC ),0) is V2() set

{(IC )} is non empty set

K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))

{0} is non empty set

K7({(IC )},{0}) is Relation-like set

K6(K7({(IC )},{0})) is set

s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

dom (stop P) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

a is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

Comput ((I +* (stop P)),(Initialize s),a) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IC (Comput ((I +* (stop P)),(Initialize s),a)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((I +* (stop P)),(Initialize s),a)) . (IC ) is set

s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

K249((stop P)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of K6(NAT)

I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

a is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

Comput (a,s,I) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IC (Comput (a,s,I)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput (a,s,I)) . (IC ) is set

Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

a +* (stop P) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

stop P is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

P ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card P is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom P is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card P)) is Relation-like Function-like set

P +* (Shift ((Stop SCMPDS),(card P))) is non empty Relation-like Function-like set

I is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

I +* (stop P) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set

K332((IC ),0) is V2() set

{(IC )} is non empty set

K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))

{0} is non empty set

K7({(IC )},{0}) is Relation-like set

K6(K7({(IC )},{0})) is set

s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

I is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

I +* (stop P) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

P is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

s is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

DataPart I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

NonZero SCMPDS is Element of K6( the carrier of SCMPDS)

K6( the carrier of SCMPDS) is set

I | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

DataPart a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

a | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

b is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

stop b is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

b ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card b is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom b is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card b)) is Relation-like Function-like set

b +* (Shift ((Stop SCMPDS),(card b))) is non empty Relation-like Function-like set

Initialize I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set

K332((IC ),0) is V2() set

{(IC )} is non empty set

K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))

{0} is non empty set

K7({(IC )},{0}) is Relation-like set

K6(K7({(IC )},{0})) is set

I +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

Initialize a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

a +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

P +* (stop b) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

s +* (stop b) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

Comput ((s +* (stop b)),(Initialize a),0) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Comput ((P +* (stop b)),(Initialize I),0) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

DataPart (Comput ((P +* (stop b)),(Initialize I),0)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((P +* (stop b)),(Initialize I),0)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

DataPart (Comput ((s +* (stop b)),(Initialize a),0)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((s +* (stop b)),(Initialize a),0)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

dom (stop b) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

s4 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

Comput ((s +* (stop b)),(Initialize a),(s4 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Comput ((s +* (stop b)),(Initialize a),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Following ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS

IC (Comput ((s +* (stop b)),(Initialize a),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((s +* (stop b)),(Initialize a),s4)) . (IC ) is set

(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS

Exec ((CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4)))),(Comput ((s +* (stop b)),(Initialize a),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set

K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set

the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))

K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set

K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set

K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))))) is Element of K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))

K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))))) . (Comput ((s +* (stop b)),(Initialize a),s4)) is set

Comput ((P +* (stop b)),(Initialize I),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IC (Comput ((P +* (stop b)),(Initialize I),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((P +* (stop b)),(Initialize I),s4)) . (IC ) is set

CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS

(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS

DataPart (Comput ((P +* (stop b)),(Initialize I),s4)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((P +* (stop b)),(Initialize I),s4)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

DataPart (Comput ((s +* (stop b)),(Initialize a),s4)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((s +* (stop b)),(Initialize a),s4)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

s5 is Int-like Element of the carrier of SCMPDS

(Comput ((P +* (stop b)),(Initialize I),s4)) . s5 is V11() V12() integer ext-real set

(Comput ((s +* (stop b)),(Initialize a),s4)) . s5 is V11() V12() integer ext-real set

Comput ((P +* (stop b)),(Initialize I),(s4 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) . (IC ) is set

Following ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Exec ((CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4)))),(Comput ((P +* (stop b)),(Initialize I),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))))) is Element of K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))

K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))))) . (Comput ((P +* (stop b)),(Initialize I),s4)) is set

IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) . (IC ) is set

(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

(P +* (stop b)) . (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

(s +* (stop b)) . (IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

(stop b) . (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is set

CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

DataPart (Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

DataPart (Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

IC (Comput ((s +* (stop b)),(Initialize a),0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((s +* (stop b)),(Initialize a),0)) . (IC ) is set

IC (Initialize a) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Initialize a) . (IC ) is set

IC (Comput ((P +* (stop b)),(Initialize I),0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((P +* (stop b)),(Initialize I),0)) . (IC ) is set

(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS

(P +* (stop b)) . (IC (Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS

(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS

(s +* (stop b)) . (IC (Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS

IC (Initialize I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Initialize I) . (IC ) is set

CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS

(stop b) . 0 is set

CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS

s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

Comput ((P +* (stop b)),(Initialize I),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IC (Comput ((P +* (stop b)),(Initialize I),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((P +* (stop b)),(Initialize I),s4)) . (IC ) is set

Comput ((s +* (stop b)),(Initialize a),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IC (Comput ((s +* (stop b)),(Initialize a),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((s +* (stop b)),(Initialize a),s4)) . (IC ) is set

P is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

s is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

DataPart I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

NonZero SCMPDS is Element of K6( the carrier of SCMPDS)

K6( the carrier of SCMPDS) is set

I | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

DataPart a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

a | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

b is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

stop b is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

b ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card b is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom b is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card b)) is Relation-like Function-like set

b +* (Shift ((Stop SCMPDS),(card b))) is non empty Relation-like Function-like set

Initialize I is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set

K332((IC ),0) is V2() set

{(IC )} is non empty set

K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))

{0} is non empty set

K7({(IC )},{0}) is Relation-like set

K6(K7({(IC )},{0})) is set

I +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

Initialize a is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

a +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

P +* (stop b) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

s +* (stop b) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

Comput ((P +* (stop b)),(Initialize I),0) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Comput ((s +* (stop b)),(Initialize a),0) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

dom (stop b) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

s4 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT

Comput ((s +* (stop b)),(Initialize a),(s4 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Comput ((s +* (stop b)),(Initialize a),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Following ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS

IC (Comput ((s +* (stop b)),(Initialize a),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((s +* (stop b)),(Initialize a),s4)) . (IC ) is set

(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS

Exec ((CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4)))),(Comput ((s +* (stop b)),(Initialize a),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)) is set

K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))) is set

the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) Element of K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))))

K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))) is Relation-like set

K6(K7( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))))) is set

K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))))) is Element of K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))

K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))))) . (Comput ((s +* (stop b)),(Initialize a),s4)) is set

Comput ((P +* (stop b)),(Initialize I),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IC (Comput ((P +* (stop b)),(Initialize I),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((P +* (stop b)),(Initialize I),s4)) . (IC ) is set

CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS

(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS

DataPart (Comput ((P +* (stop b)),(Initialize I),s4)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((P +* (stop b)),(Initialize I),s4)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

DataPart (Comput ((s +* (stop b)),(Initialize a),s4)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((s +* (stop b)),(Initialize a),s4)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

s5 is Int-like Element of the carrier of SCMPDS

(Comput ((P +* (stop b)),(Initialize I),s4)) . s5 is V11() V12() integer ext-real set

(Comput ((s +* (stop b)),(Initialize a),s4)) . s5 is V11() V12() integer ext-real set

Comput ((P +* (stop b)),(Initialize I),(s4 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) . (IC ) is set

Following ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Exec ((CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4)))),(Comput ((P +* (stop b)),(Initialize I),s4))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))))) is Element of K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)))

K132( the InstructionsF of SCMPDS,K130(K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS)),K150(( the Object-Kind of SCMPDS (#) the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))))) . (Comput ((P +* (stop b)),(Initialize I),s4)) is set

IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) . (IC ) is set

(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

(P +* (stop b)) . (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

(s +* (stop b)) . (IC (Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

(stop b) . (IC (Comput ((P +* (stop b)),(Initialize I),(s4 + 1)))) is set

CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),(s4 + 1)))) is Element of the InstructionsF of SCMPDS

DataPart (Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((P +* (stop b)),(Initialize I),(s4 + 1))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

DataPart (Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((s +* (stop b)),(Initialize a),(s4 + 1))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

IC (Comput ((s +* (stop b)),(Initialize a),0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((s +* (stop b)),(Initialize a),0)) . (IC ) is set

IC (Initialize a) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Initialize a) . (IC ) is set

s4 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

Comput ((P +* (stop b)),(Initialize I),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS

IC (Comput ((P +* (stop b)),(Initialize I),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((P +* (stop b)),(Initialize I),s4)) . (IC ) is set

(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),s4))) is Element of the InstructionsF of SCMPDS

IC (Comput ((P +* (stop b)),(Initialize I),0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((P +* (stop b)),(Initialize I),0)) . (IC ) is set

(P +* (stop b)) /. (IC (Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS

(P +* (stop b)) . (IC (Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS

(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS

(s +* (stop b)) . (IC (Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS

IC (Initialize I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Initialize I) . (IC ) is set

CurInstr ((P +* (stop b)),(Comput ((P +* (stop b)),(Initialize I),0))) is Element of the InstructionsF of SCMPDS

(stop b) . 0 is set

CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),0))) is Element of the InstructionsF of SCMPDS

DataPart (Comput ((P +* (stop b)),(Initialize I),0)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((P +* (stop b)),(Initialize I),0)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

DataPart (Comput ((s +* (stop b)),(Initialize a),0)) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((s +* (stop b)),(Initialize a),0)) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

s5 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

Comput ((P +* (stop b)),(Initialize I),s5) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IC (Comput ((P +* (stop b)),(Initialize I),s5)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((P +* (stop b)),(Initialize I),s5)) . (IC ) is set

Comput ((s +* (stop b)),(Initialize a),s5) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

IC (Comput ((s +* (stop b)),(Initialize a),s5)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((s +* (stop b)),(Initialize a),s5)) . (IC ) is set

Comput ((s +* (stop b)),(Initialize a),s4) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

CurInstr ((s +* (stop b)),(Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS

IC (Comput ((s +* (stop b)),(Initialize a),s4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput ((s +* (stop b)),(Initialize a),s4)) . (IC ) is set

(s +* (stop b)) /. (IC (Comput ((s +* (stop b)),(Initialize a),s4))) is Element of the InstructionsF of SCMPDS

P is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0 -started set

K332((IC ),0) is V2() set

{(IC )} is non empty set

K323({(IC )},0) is Relation-like Function-like V29({(IC )},{0}) Element of K6(K7({(IC )},{0}))

{0} is non empty set

K7({(IC )},{0}) is Relation-like set

K6(K7({(IC )},{0})) is set

s +* (Start-At (0,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible K282(2,SCMPDS) -compatible total 0 -started set

I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

P +* a is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

DataPart s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

NonZero SCMPDS is Element of K6( the carrier of SCMPDS)

K6( the carrier of SCMPDS) is set

s | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

DataPart (Initialize s) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Initialize s) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

P is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

stop I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

I ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom I is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card I)) is Relation-like Function-like set

I +* (Shift ((Stop SCMPDS),(card I))) is non empty Relation-like Function-like set

P +* (stop I) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

LifeSpan ((P +* (stop I)),s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

I ';' a is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

Shift (a,(card I)) is Relation-like Function-like set

I +* (Shift (a,(card I))) is non empty Relation-like Function-like set

stop (I ';' a) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

(I ';' a) ';' (Stop SCMPDS) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V32() V71() set

card (I ';' a) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (I ';' a) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set

Shift ((Stop SCMPDS),(card (I ';' a))) is Relation-like Function-like set

(I ';' a) +* (Shift ((Stop SCMPDS),(card (I ';' a)))) is non empty Relation-like Function-like set

P +* (stop (I ';' a)) is non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set

Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

NonZero SCMPDS is Element of K6( the carrier of SCMPDS)

K6( the carrier of SCMPDS) is set

(Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

Comput ((P +* (stop (I ';' a))),s,(LifeSpan ((P +* (stop I)),s))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total set

DataPart (Comput ((P +* (stop (I ';' a))),s,(LifeSpan ((P +* (stop I)),s)))) is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible data-only set

(Comput ((P +* (stop (I ';' a))),s,(LifeSpan ((P +* (stop I)),s)))) | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined set

Initialize s is Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible total 0 -started set

Start-At (0,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K282(2,SCMPDS) -compatible V32() 0