:: SCMPDS_4 semantic presentation

REAL is set

NAT is non empty V2() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite V43() V44() Element of K6(REAL)

K6(REAL) is set

COMPLEX is set

NAT is non empty V2() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite V43() V44() 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 V43() Element of K6(NAT)

K151() 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 set

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

SCM-OK is Relation-like SCM-Memory -defined 2 -valued 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 Function-like set

K140((SCM-OK (#) SCM-VAL)) is functional V41() V42() set

K152() is non empty set

K120(K140((SCM-OK (#) SCM-VAL)),K140((SCM-OK (#) SCM-VAL))) is set

K7(K152(),K120(K140((SCM-OK (#) SCM-VAL)),K140((SCM-OK (#) SCM-VAL)))) is set

K6(K7(K152(),K120(K140((SCM-OK (#) SCM-VAL)),K140((SCM-OK (#) SCM-VAL))))) is set

K6(NAT) is set

INT is set

K151() \/ INT is set

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

SCM-Data-Loc \/ INT is set

K185() is set

K7(K185(),K120(K140((SCM-OK (#) SCM-VAL)),K140((SCM-OK (#) SCM-VAL)))) is set

K6(K7(K185(),K120(K140((SCM-OK (#) SCM-VAL)),K140((SCM-OK (#) SCM-VAL))))) is set

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

K518(NAT,SCM-Memory) is Element of SCM-Memory

K205() is Relation-like K185() -defined K120(K140((SCM-OK (#) SCM-VAL)),K140((SCM-OK (#) SCM-VAL))) -valued Function-like V29(K185(),K120(K140((SCM-OK (#) SCM-VAL)),K140((SCM-OK (#) SCM-VAL)))) Element of K6(K7(K185(),K120(K140((SCM-OK (#) SCM-VAL)),K140((SCM-OK (#) SCM-VAL)))))

AMI-Struct(# SCM-Memory,K518(NAT,SCM-Memory),K185(),SCM-OK,SCM-VAL,K205() #) is strict AMI-Struct over 2

the carrier of SCMPDS is non empty set

the InstructionsF of SCMPDS is non empty Relation-like standard-ins V73() J/A-independent V76() 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 V29( the carrier of SCMPDS,2) Element of K6(K7( the carrier of SCMPDS,2))

K7( the carrier of SCMPDS,2) is set

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

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

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

RAT is set

K506() is non empty with_non-empty_values IC-Ins-separated strict strict V91(2) AMI-Struct over 2

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

the carrier of K506() is non empty set

the_Values_of K506() is Relation-like non-empty the carrier of K506() -defined Function-like total set

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

K7( the carrier of K506(),2) is set

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

the ValuesF of K506() is Relation-like 2 -defined Function-like total set

the Object-Kind of K506() (#) the ValuesF of K506() is Relation-like Function-like set

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

{} is set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Function-like functional finite V36() V43() V67() ext-real non positive non negative set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Function-like functional finite V36() V43() V67() ext-real non positive non negative set

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

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

14 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

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

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

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

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

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

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

IC is V57( SCMPDS ) Element of the carrier of SCMPDS

halt SCMPDS is V90(2, SCMPDS ) Element of the InstructionsF of SCMPDS

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

[0,{},{}] is V26() V27() set

[0,{}] is V26() set

{0,{}} is finite V43() set

{0} is finite V43() set

{{0,{}},{0}} is finite V36() V43() set

[[0,{}],{}] is V26() set

{[0,{}],{}} is finite V43() set

{[0,{}]} is Function-like finite V43() set

{{[0,{}],{}},{[0,{}]}} is finite V36() V43() set

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

K6( the carrier of SCMPDS) is set

{0,1,4,5,6,14} is finite V43() set

s2 is Element of the InstructionsF of SCMPDS

InsCode s2 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

K90(s2) is set

K90(K90(s2)) is set

P1 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

Exec (s2,P1) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)) is functional V41() V42() set

K120(K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) is set

the Execution of SCMPDS is Relation-like the InstructionsF of SCMPDS -defined K120(K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))) -valued Function-like V29( the InstructionsF of SCMPDS,K120(K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) Element of K6(K7( the InstructionsF of SCMPDS,K120(K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))))

K7( the InstructionsF of SCMPDS,K120(K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))) is set

K6(K7( the InstructionsF of SCMPDS,K120(K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))))) is set

K122( the InstructionsF of SCMPDS,K120(K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))), the Execution of SCMPDS,s2) is Element of K120(K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)))

K122( the InstructionsF of SCMPDS,K120(K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS)),K140(( the Object-Kind of SCMPDS (#) the ValuesF of SCMPDS))), the Execution of SCMPDS,s2) . P1 is set

(Exec (s2,P1)) . (IC ) is set

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

P1 . (IC ) is set

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

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

P2 is Int-like Element of the carrier of SCMPDS

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

P2 := s1 is Element of the InstructionsF of SCMPDS

K176(P2,s1) is set

[2,{},K176(P2,s1)] is V26() V27() set

[2,{}] is V26() set

{2,{}} is finite V43() set

{2} is finite V43() set

{{2,{}},{2}} is finite V36() V43() set

[[2,{}],K176(P2,s1)] is V26() set

{[2,{}],K176(P2,s1)} is finite V43() set

{[2,{}]} is Function-like finite V43() set

{{[2,{}],K176(P2,s1)},{[2,{}]}} is finite V36() V43() set

P2 is Int-like Element of the carrier of SCMPDS

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

saveIC (P2,s1) is Element of the InstructionsF of SCMPDS

K176(P2,s1) is set

[3,{},K176(P2,s1)] is V26() V27() set

[3,{}] is V26() set

{3,{}} is finite V43() set

{3} is finite V43() set

{{3,{}},{3}} is finite V36() V43() set

[[3,{}],K176(P2,s1)] is V26() set

{[3,{}],K176(P2,s1)} is finite V43() set

{[3,{}]} is Function-like finite V43() set

{{[3,{}],K176(P2,s1)},{[3,{}]}} is finite V36() V43() set

P2 is Int-like Element of the carrier of SCMPDS

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

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

(P2,s1) := I is Element of the InstructionsF of SCMPDS

K177(P2,s1,I) is set

[7,{},K177(P2,s1,I)] is V26() V27() set

[7,{}] is V26() set

{7,{}} is finite V43() set

{7} is finite V43() set

{{7,{}},{7}} is finite V36() V43() set

[[7,{}],K177(P2,s1,I)] is V26() set

{[7,{}],K177(P2,s1,I)} is finite V43() set

{[7,{}]} is Function-like finite V43() set

{{[7,{}],K177(P2,s1,I)},{[7,{}]}} is finite V36() V43() set

P2 is Int-like Element of the carrier of SCMPDS

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

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

AddTo (P2,s1,I) is Element of the InstructionsF of SCMPDS

K177(P2,s1,I) is set

[8,{},K177(P2,s1,I)] is V26() V27() set

[8,{}] is V26() set

{8,{}} is finite V43() set

{8} is finite V43() set

{{8,{}},{8}} is finite V36() V43() set

[[8,{}],K177(P2,s1,I)] is V26() set

{[8,{}],K177(P2,s1,I)} is finite V43() set

{[8,{}]} is Function-like finite V43() set

{{[8,{}],K177(P2,s1,I)},{[8,{}]}} is finite V36() V43() set

P2 is Int-like Element of the carrier of SCMPDS

s1 is Int-like Element of the carrier of SCMPDS

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

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

AddTo (P2,I,s1,SI) is Element of the InstructionsF of SCMPDS

P2 is Int-like Element of the carrier of SCMPDS

s1 is Int-like Element of the carrier of SCMPDS

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

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

SubFrom (P2,I,s1,SI) is Element of the InstructionsF of SCMPDS

P2 is Int-like Element of the carrier of SCMPDS

s1 is Int-like Element of the carrier of SCMPDS

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

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

MultBy (P2,I,s1,SI) is Element of the InstructionsF of SCMPDS

P2 is Int-like Element of the carrier of SCMPDS

s1 is Int-like Element of the carrier of SCMPDS

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

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

Divide (P2,I,s1,SI) is Element of the InstructionsF of SCMPDS

P2 is Int-like Element of the carrier of SCMPDS

s1 is Int-like Element of the carrier of SCMPDS

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

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

(P2,I) := (s1,SI) is Element of the InstructionsF of SCMPDS

s2 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

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

s2 . (IC ) is set

P1 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

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

P1 . (IC ) is set

{(IC )} is finite V43() set

{(IC )} \/ SCM-Data-Loc is set

proj1 P1 is set

P1 | (proj1 P1) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set

proj1 (P1 | (proj1 P1)) is set

(proj1 P1) /\ (proj1 P1) is set

proj1 s2 is set

s2 | (proj1 s2) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set

proj1 (s2 | (proj1 s2)) is set

(proj1 s2) /\ (proj1 s2) is set

P2 is set

(s2 | (proj1 s2)) . P2 is set

(P1 | (proj1 P1)) . P2 is set

(s2 | (proj1 s2)) . P2 is set

s2 . P2 is set

P1 . P2 is set

(P1 | (proj1 P1)) . P2 is set

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

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

DataLoc (s2,0) is Int-like Element of the carrier of SCMPDS

s2 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

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

[1,(abs (s2 + 0))] is V26() set

{1,(abs (s2 + 0))} is finite V43() set

{1} is finite V43() set

{{1,(abs (s2 + 0))},{1}} is finite V36() V43() set

DataLoc (P1,0) is Int-like Element of the carrier of SCMPDS

P1 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

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

[1,(abs (P1 + 0))] is V26() set

{1,(abs (P1 + 0))} is finite V43() set

{{1,(abs (P1 + 0))},{1}} is finite V36() V43() set

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

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

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

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

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

s2 is Int-like Element of the carrier of SCMPDS

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

[1,P1] is V26() set

{1,P1} is finite V43() set

{1} is finite V43() set

{{1,P1},{1}} is finite V36() V43() set

DataLoc (P1,0) is Int-like Element of the carrier of SCMPDS

P1 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

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

[1,(abs (P1 + 0))] is V26() set

{1,(abs (P1 + 0))} is finite V43() set

{{1,(abs (P1 + 0))},{1}} is finite V36() V43() set

F

{(IC )} is finite V43() set

s1 is set

{(IC )} \/ SCM-Data-Loc is set

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

DataLoc (I,0) is Int-like Element of the carrier of SCMPDS

I + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

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

[1,(abs (I + 0))] is V26() set

{1,(abs (I + 0))} is finite V43() set

{1} is finite V43() set

{{1,(abs (I + 0))},{1}} is finite V36() V43() set

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

DataLoc (I,0) is Int-like Element of the carrier of SCMPDS

I + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

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

[1,(abs (I + 0))] is V26() set

{1,(abs (I + 0))} is finite V43() set

{1} is finite V43() set

{{1,(abs (I + 0))},{1}} is finite V36() V43() set

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

F

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

s1 is Relation-like Function-like set

proj1 s1 is set

proj1 the Object-Kind of SCMPDS is set

I is set

{(IC )} \/ SCM-Data-Loc is set

s1 . I is set

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

DataLoc (SI,0) is Int-like Element of the carrier of SCMPDS

SI + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

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

[1,(abs (SI + 0))] is V26() set

{1,(abs (SI + 0))} is finite V43() set

{1} is finite V43() set

{{1,(abs (SI + 0))},{1}} is finite V36() V43() set

F

(the_Values_of SCMPDS) . I is set

Values (DataLoc (SI,0)) is non empty set

(the_Values_of SCMPDS) . (DataLoc (SI,0)) is set

(the_Values_of SCMPDS) . I is set

Values (IC ) is non empty set

(the_Values_of SCMPDS) . (IC ) is set

I is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

I . (IC ) is set

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

DataLoc (SI,0) is Int-like Element of the carrier of SCMPDS

SI + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

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

[1,(abs (SI + 0))] is V26() set

{1,(abs (SI + 0))} is finite V43() set

{{1,(abs (SI + 0))},{1}} is finite V36() V43() set

F

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

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

DataLoc (n,0) is Int-like Element of the carrier of SCMPDS

n + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

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

[1,(abs (n + 0))] is V26() set

{1,(abs (n + 0))} is finite V43() set

{{1,(abs (n + 0))},{1}} is finite V36() V43() set

I . (DataLoc (n,0)) is V11() V12() integer ext-real set

F

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

DataLoc (i,0) is Int-like Element of the carrier of SCMPDS

i + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

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

[1,(abs (i + 0))] is V26() set

{1,(abs (i + 0))} is finite V43() set

{{1,(abs (i + 0))},{1}} is finite V36() V43() set

F

{(IC )} is finite V43() set

{(IC )} \/ SCM-Data-Loc is set

s2 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

proj1 s2 is set

s1 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

proj1 s1 is set

I is set

s1 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

I is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

DataPart s1 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set

s1 | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set

DataPart I is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set

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

SI is set

s1 . SI is set

I . SI is set

SI is Int-like Element of the carrier of SCMPDS

s1 . SI is V11() V12() integer ext-real set

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

proj1 I is set

proj1 s1 is set

SI is Int-like Element of the carrier of SCMPDS

s1 . SI is V11() V12() integer ext-real set

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

n is Int-like Element of the carrier of SCMPDS

s1 . n is V11() V12() integer ext-real set

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

i is set

s1 . i is set

I . i is set

s2 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

P1 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

s2 ^ P1 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift (P1,(card s2)) is Relation-like Function-like set

s2 +* (Shift (P1,(card s2))) is non empty Relation-like Function-like set

P2 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

s1 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

s2 is Element of the InstructionsF of SCMPDS

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

K343(0,s2) is non empty V2() finite V43() set

K334({0},s2) is Relation-like {0} -defined {s2} -valued Function-like V29({0},{s2}) finite V43() V136() Element of K6(K7({0},{s2}))

{s2} is finite V43() set

K7({0},{s2}) is finite V43() set

K6(K7({0},{s2})) is finite V36() V43() set

P1 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((Load s2),P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift (P1,(card (Load s2))) is Relation-like Function-like set

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

s2 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

P1 is Element of the InstructionsF of SCMPDS

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

K343(0,P1) is non empty V2() finite V43() set

K334({0},P1) is Relation-like {0} -defined {P1} -valued Function-like V29({0},{P1}) finite V43() V136() Element of K6(K7({0},{P1}))

{P1} is finite V43() set

K7({0},{P1}) is finite V43() set

K6(K7({0},{P1})) is finite V36() V43() set

(s2,(Load P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P1),(card s2)) is Relation-like Function-like set

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

s2 is Element of the InstructionsF of SCMPDS

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

K343(0,s2) is non empty V2() finite V43() set

K334({0},s2) is Relation-like {0} -defined {s2} -valued Function-like V29({0},{s2}) finite V43() V136() Element of K6(K7({0},{s2}))

{s2} is finite V43() set

K7({0},{s2}) is finite V43() set

K6(K7({0},{s2})) is finite V36() V43() set

P1 is Element of the InstructionsF of SCMPDS

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

K343(0,P1) is non empty V2() finite V43() set

K334({0},P1) is Relation-like {0} -defined {P1} -valued Function-like V29({0},{P1}) finite V43() V136() Element of K6(K7({0},{P1}))

{P1} is finite V43() set

K7({0},{P1}) is finite V43() set

K6(K7({0},{P1})) is finite V36() V43() set

((Load s2),(Load P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P1),(card (Load s2))) is Relation-like Function-like set

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

s2 is Element of the InstructionsF of SCMPDS

P1 is Element of the InstructionsF of SCMPDS

(s2,P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,s2) is non empty V2() finite V43() set

K334({0},s2) is Relation-like {0} -defined {s2} -valued Function-like V29({0},{s2}) finite V43() V136() Element of K6(K7({0},{s2}))

{s2} is finite V43() set

K7({0},{s2}) is finite V43() set

K6(K7({0},{s2})) is finite V36() V43() set

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

K343(0,P1) is non empty V2() finite V43() set

K334({0},P1) is Relation-like {0} -defined {P1} -valued Function-like V29({0},{P1}) finite V43() V136() Element of K6(K7({0},{P1}))

{P1} is finite V43() set

K7({0},{P1}) is finite V43() set

K6(K7({0},{P1})) is finite V36() V43() set

((Load s2),(Load P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P1),(card (Load s2))) is Relation-like Function-like set

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

((Load s2),P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

s2 is Element of the InstructionsF of SCMPDS

P1 is Element of the InstructionsF of SCMPDS

(s2,P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,s2) is non empty V2() finite V43() set

K334({0},s2) is Relation-like {0} -defined {s2} -valued Function-like V29({0},{s2}) finite V43() V136() Element of K6(K7({0},{s2}))

{s2} is finite V43() set

K7({0},{s2}) is finite V43() set

K6(K7({0},{s2})) is finite V36() V43() set

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

K343(0,P1) is non empty V2() finite V43() set

K334({0},P1) is Relation-like {0} -defined {P1} -valued Function-like V29({0},{P1}) finite V43() V136() Element of K6(K7({0},{P1}))

{P1} is finite V43() set

K7({0},{P1}) is finite V43() set

K6(K7({0},{P1})) is finite V36() V43() set

((Load s2),(Load P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P1),(card (Load s2))) is Relation-like Function-like set

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

(s2,(Load P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

P1 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

P2 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

(P1,P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 P1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift (P2,(card P1)) is Relation-like Function-like set

P1 +* (Shift (P2,(card P1))) is non empty Relation-like Function-like set

s2 is Element of the InstructionsF of SCMPDS

((P1,P2),s2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,s2) is non empty V2() finite V43() set

K334({0},s2) is Relation-like {0} -defined {s2} -valued Function-like V29({0},{s2}) finite V43() V136() Element of K6(K7({0},{s2}))

{s2} is finite V43() set

K7({0},{s2}) is finite V43() set

K6(K7({0},{s2})) is finite V36() V43() set

((P1,P2),(Load s2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (P1,P2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load s2),(card (P1,P2))) is Relation-like Function-like set

(P1,P2) +* (Shift ((Load s2),(card (P1,P2)))) is non empty Relation-like Function-like set

(P2,s2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

(P2,(Load s2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load s2),(card P2)) is Relation-like Function-like set

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

(P1,(P2,s2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

Shift ((P2,s2),(card P1)) is Relation-like Function-like set

P1 +* (Shift ((P2,s2),(card P1))) is non empty Relation-like Function-like set

P1 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

s2 is Element of the InstructionsF of SCMPDS

(P1,s2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,s2) is non empty V2() finite V43() set

K334({0},s2) is Relation-like {0} -defined {s2} -valued Function-like V29({0},{s2}) finite V43() V136() Element of K6(K7({0},{s2}))

{s2} is finite V43() set

K7({0},{s2}) is finite V43() set

K6(K7({0},{s2})) is finite V36() V43() set

(P1,(Load s2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 P1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load s2),(card P1)) is Relation-like Function-like set

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

P2 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((P1,s2),P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (P1,s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift (P2,(card (P1,s2))) is Relation-like Function-like set

(P1,s2) +* (Shift (P2,(card (P1,s2)))) is non empty Relation-like Function-like set

(s2,P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((Load s2),P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift (P2,(card (Load s2))) is Relation-like Function-like set

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

(P1,(s2,P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

Shift ((s2,P2),(card P1)) is Relation-like Function-like set

P1 +* (Shift ((s2,P2),(card P1))) is non empty Relation-like Function-like set

P2 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

s2 is Element of the InstructionsF of SCMPDS

(P2,s2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,s2) is non empty V2() finite V43() set

K334({0},s2) is Relation-like {0} -defined {s2} -valued Function-like V29({0},{s2}) finite V43() V136() Element of K6(K7({0},{s2}))

{s2} is finite V43() set

K7({0},{s2}) is finite V43() set

K6(K7({0},{s2})) is finite V36() V43() set

(P2,(Load s2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load s2),(card P2)) is Relation-like Function-like set

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

P1 is Element of the InstructionsF of SCMPDS

((P2,s2),P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,P1) is non empty V2() finite V43() set

K334({0},P1) is Relation-like {0} -defined {P1} -valued Function-like V29({0},{P1}) finite V43() V136() Element of K6(K7({0},{P1}))

{P1} is finite V43() set

K7({0},{P1}) is finite V43() set

K6(K7({0},{P1})) is finite V36() V43() set

((P2,s2),(Load P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (P2,s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P1),(card (P2,s2))) is Relation-like Function-like set

(P2,s2) +* (Shift ((Load P1),(card (P2,s2)))) is non empty Relation-like Function-like set

(s2,P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((Load s2),(Load P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P1),(card (Load s2))) is Relation-like Function-like set

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

(P2,(s2,P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

Shift ((s2,P1),(card P2)) is Relation-like Function-like set

P2 +* (Shift ((s2,P1),(card P2))) is non empty Relation-like Function-like set

s2 is Element of the InstructionsF of SCMPDS

P1 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

(s2,P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,s2) is non empty V2() finite V43() set

K334({0},s2) is Relation-like {0} -defined {s2} -valued Function-like V29({0},{s2}) finite V43() V136() Element of K6(K7({0},{s2}))

{s2} is finite V43() set

K7({0},{s2}) is finite V43() set

K6(K7({0},{s2})) is finite V36() V43() set

((Load s2),P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift (P1,(card (Load s2))) is Relation-like Function-like set

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

P2 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((s2,P1),P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (s2,P1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift (P2,(card (s2,P1))) is Relation-like Function-like set

(s2,P1) +* (Shift (P2,(card (s2,P1)))) is non empty Relation-like Function-like set

(P1,P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 P1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift (P2,(card P1)) is Relation-like Function-like set

P1 +* (Shift (P2,(card P1))) is non empty Relation-like Function-like set

(s2,(P1,P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((Load s2),(P1,P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

Shift ((P1,P2),(card (Load s2))) is Relation-like Function-like set

(Load s2) +* (Shift ((P1,P2),(card (Load s2)))) is non empty Relation-like Function-like set

s2 is Element of the InstructionsF of SCMPDS

P2 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

(s2,P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,s2) is non empty V2() finite V43() set

K334({0},s2) is Relation-like {0} -defined {s2} -valued Function-like V29({0},{s2}) finite V43() V136() Element of K6(K7({0},{s2}))

{s2} is finite V43() set

K7({0},{s2}) is finite V43() set

K6(K7({0},{s2})) is finite V36() V43() set

((Load s2),P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift (P2,(card (Load s2))) is Relation-like Function-like set

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

P1 is Element of the InstructionsF of SCMPDS

((s2,P2),P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,P1) is non empty V2() finite V43() set

K334({0},P1) is Relation-like {0} -defined {P1} -valued Function-like V29({0},{P1}) finite V43() V136() Element of K6(K7({0},{P1}))

{P1} is finite V43() set

K7({0},{P1}) is finite V43() set

K6(K7({0},{P1})) is finite V36() V43() set

((s2,P2),(Load P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (s2,P2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P1),(card (s2,P2))) is Relation-like Function-like set

(s2,P2) +* (Shift ((Load P1),(card (s2,P2)))) is non empty Relation-like Function-like set

(P2,P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

(P2,(Load P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P1),(card P2)) is Relation-like Function-like set

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

(s2,(P2,P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((Load s2),(P2,P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

Shift ((P2,P1),(card (Load s2))) is Relation-like Function-like set

(Load s2) +* (Shift ((P2,P1),(card (Load s2)))) is non empty Relation-like Function-like set

s2 is Element of the InstructionsF of SCMPDS

P1 is Element of the InstructionsF of SCMPDS

(s2,P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,s2) is non empty V2() finite V43() set

K334({0},s2) is Relation-like {0} -defined {s2} -valued Function-like V29({0},{s2}) finite V43() V136() Element of K6(K7({0},{s2}))

{s2} is finite V43() set

K7({0},{s2}) is finite V43() set

K6(K7({0},{s2})) is finite V36() V43() set

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

K343(0,P1) is non empty V2() finite V43() set

K334({0},P1) is Relation-like {0} -defined {P1} -valued Function-like V29({0},{P1}) finite V43() V136() Element of K6(K7({0},{P1}))

{P1} is finite V43() set

K7({0},{P1}) is finite V43() set

K6(K7({0},{P1})) is finite V36() V43() set

((Load s2),(Load P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P1),(card (Load s2))) is Relation-like Function-like set

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

P2 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((s2,P1),P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (s2,P1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift (P2,(card (s2,P1))) is Relation-like Function-like set

(s2,P1) +* (Shift (P2,(card (s2,P1)))) is non empty Relation-like Function-like set

(P1,P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((Load P1),P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load P1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift (P2,(card (Load P1))) is Relation-like Function-like set

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

(s2,(P1,P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((Load s2),(P1,P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

Shift ((P1,P2),(card (Load s2))) is Relation-like Function-like set

(Load s2) +* (Shift ((P1,P2),(card (Load s2)))) is non empty Relation-like Function-like set

s2 is Element of the InstructionsF of SCMPDS

P1 is Element of the InstructionsF of SCMPDS

(s2,P1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,s2) is non empty V2() finite V43() set

K334({0},s2) is Relation-like {0} -defined {s2} -valued Function-like V29({0},{s2}) finite V43() V136() Element of K6(K7({0},{s2}))

{s2} is finite V43() set

K7({0},{s2}) is finite V43() set

K6(K7({0},{s2})) is finite V36() V43() set

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

K343(0,P1) is non empty V2() finite V43() set

K334({0},P1) is Relation-like {0} -defined {P1} -valued Function-like V29({0},{P1}) finite V43() V136() Element of K6(K7({0},{P1}))

{P1} is finite V43() set

K7({0},{P1}) is finite V43() set

K6(K7({0},{P1})) is finite V36() V43() set

((Load s2),(Load P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P1),(card (Load s2))) is Relation-like Function-like set

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

P2 is Element of the InstructionsF of SCMPDS

((s2,P1),P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

K343(0,P2) is non empty V2() finite V43() set

K334({0},P2) is Relation-like {0} -defined {P2} -valued Function-like V29({0},{P2}) finite V43() V136() Element of K6(K7({0},{P2}))

{P2} is finite V43() set

K7({0},{P2}) is finite V43() set

K6(K7({0},{P2})) is finite V36() V43() set

((s2,P1),(Load P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (s2,P1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P2),(card (s2,P1))) is Relation-like Function-like set

(s2,P1) +* (Shift ((Load P2),(card (s2,P1)))) is non empty Relation-like Function-like set

(P1,P2) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((Load P1),(Load P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load P1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

Shift ((Load P2),(card (Load P1))) is Relation-like Function-like set

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

(s2,(P1,P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

((Load s2),(P1,P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

Shift ((P1,P2),(card (Load s2))) is Relation-like Function-like set

(Load s2) +* (Shift ((P1,P2),(card (Load s2)))) is non empty Relation-like Function-like set

s2 is Int-like Element of the carrier of SCMPDS

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

Start-At (P1,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible finite V43() P1 -started V136() set

K343((IC ),P1) is non empty V2() finite V43() set

K334({(IC )},P1) is Relation-like {(IC )} -defined {P1} -valued Function-like V29({(IC )},{P1}) finite V43() V136() Element of K6(K7({(IC )},{P1}))

{P1} is finite V43() set

K7({(IC )},{P1}) is finite V43() set

K6(K7({(IC )},{P1})) is finite V36() V43() set

proj1 (Start-At (P1,SCMPDS)) is finite V43() set

s2 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

P1 is Int-like Element of the carrier of SCMPDS

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

s2 +* (P1,P2) is Relation-like the carrier of SCMPDS -defined Function-like total set

proj1 s2 is set

s1 is set

proj1 (s2 +* (P1,P2)) is set

(the_Values_of SCMPDS) . s1 is set

Values P1 is non empty set

(the_Values_of SCMPDS) . P1 is set

(s2 +* (P1,P2)) . s1 is set

(s2 +* (P1,P2)) . s1 is set

s2 . s1 is set

(the_Values_of SCMPDS) . s1 is set

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

s2 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

stop s2 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

Stop SCMPDS is non empty V2() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like constant finite V43() V71() non halt-free V80( SCMPDS ) V81( SCMPDS ) V136() set

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

K343(0,(halt SCMPDS)) is non empty V2() finite V43() set

K334({0},(halt SCMPDS)) is Relation-like {0} -defined {(halt SCMPDS)} -valued Function-like V29({0},{(halt SCMPDS)}) finite V43() V136() Element of K6(K7({0},{(halt SCMPDS)}))

{(halt SCMPDS)} is finite V43() set

K7({0},{(halt SCMPDS)}) is finite V43() set

K6(K7({0},{(halt SCMPDS)})) is finite V36() V43() set

s2 ^ (Stop SCMPDS) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

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

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

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

P1 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

Result ((P2 +* (stop s2)),P1) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

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

stop (Load (halt SCMPDS)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

(Load (halt SCMPDS)) ^ (Stop SCMPDS) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set

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

proj1 (Load (halt SCMPDS)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative set

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

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

s2 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set

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

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

s2 . (IC ) is set

Comput (P1,s2,0) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

IC (Comput (P1,s2,0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput (P1,s2,0)) . (IC ) is set

proj1 P1 is set

CurInstr (P1,(Comput (P1,s2,0))) is Element of the InstructionsF of SCMPDS

P1 /. (IC (Comput (P1,s2,0))) is Element of the InstructionsF of SCMPDS

(Load (halt SCMPDS)) . 0 is set

dom (Load (halt SCMPDS)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)

dom (stop (Load (halt SCMPDS))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)

P1 /. (IC s2) is Element of the InstructionsF of SCMPDS

P1 . (IC s2) is Element of the InstructionsF of SCMPDS

(stop (Load (halt SCMPDS))) . 0 is set

goto 1 is Element of the InstructionsF of SCMPDS

K175(1) is Relation-like Function-like set

[14,{},K175(1)] is V26() V27() set

[14,{}] is V26() set

{14,{}} is finite V43() set

{14} is finite V43() set

{{14,{}},{14}} is finite V36() V43() set

[[14,{}],K175(1)] is V26() set

{[14,{}],K175(1)} is finite V43() set

{[14,{}]} is Function-like finite V43() set

{{[14,{}],K175(1)},{[14,{}]}} is finite V36() V43() set

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

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

K175((- 1)) is Relation-like Function-like set

[14,{},K175((- 1))] is V26() V27() set

[[14,{}],K175((- 1))] is V26() set

{[14,{}],K175((- 1))} is finite V43() set

{{[14,{}],K175((- 1))},{[14,{}]}} is finite V36() V43() set

s2 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set

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

s2 . (IC ) is set

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

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

((IC s2),(succ (IC s2))) --> ((goto 1),(goto (- 1))) is non empty Relation-like {(IC s2),(succ (IC s2))} -defined the InstructionsF of SCMPDS -valued Function-like V29({(IC s2),(succ (IC s2))}, the InstructionsF of SCMPDS) finite V43() V136() Element of K6(K7({(IC s2),(succ (IC s2))}, the InstructionsF of SCMPDS))

{(IC s2),(succ (IC s2))} is finite V43() set

K7({(IC s2),(succ (IC s2))}, the InstructionsF of SCMPDS) is set

K6(K7({(IC s2),(succ (IC s2))}, the InstructionsF of SCMPDS)) is set

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

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

P1 +* (((IC s2),(succ (IC s2))) --> ((goto 1),(goto (- 1)))) is non empty Relation-like the InstructionsF of SCMPDS -valued Function-like