:: 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₂() is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
{(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₁(I) is V11() V12() integer ext-real set
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₁(SI) is V11() V12() integer ext-real set
(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₁(SI) is V11() V12() integer ext-real set
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₁(n) is V11() V12() integer ext-real 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,(abs (i + 0))},{1}} is finite V36() V43() set
F₁(i) is V11() V12() integer ext-real set
{(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 set
(((IC s2),(succ (IC s2))) --> ((goto 1),(goto (- 1)))) . (succ (IC s2)) is set
(((IC s2),(succ (IC s2))) --> ((goto 1),(goto (- 1)))) . (IC s2) is set
proj1 (((IC s2),(succ (IC s2))) --> ((goto 1),(goto (- 1)))) is finite V43() set
I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P2,s2,I) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P2,s2,I)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,I)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,I))) is Element of the InstructionsF of SCMPDS
P2 . (IC (Comput (P2,s2,I))) is Element of the InstructionsF of SCMPDS
CurInstr (P2,(Comput (P2,s2,I))) is Element of the InstructionsF of SCMPDS
P2 . (IC s2) is Element of the InstructionsF of SCMPDS
I + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (P2,s2,(I + 1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P2,s2,(I + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,(I + 1))) . (IC ) is set
Following (P2,(Comput (P2,s2,I))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Exec ((CurInstr (P2,(Comput (P2,s2,I)))),(Comput (P2,s2,I))) 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,(CurInstr (P2,(Comput (P2,s2,I))))) 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,(CurInstr (P2,(Comput (P2,s2,I))))) . (Comput (P2,s2,I)) is set
IC (Following (P2,(Comput (P2,s2,I)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Following (P2,(Comput (P2,s2,I)))) . (IC ) is set
ICplusConst ((Comput (P2,s2,I)),1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
ICplusConst ((Comput (P2,s2,I)),(- 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
CurInstr (P2,(Comput (P2,s2,I))) is Element of the InstructionsF of SCMPDS
P2 . (succ (IC s2)) is Element of the InstructionsF of SCMPDS
I + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (P2,s2,(I + 1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P2,s2,(I + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,(I + 1))) . (IC ) is set
Following (P2,(Comput (P2,s2,I))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Exec ((CurInstr (P2,(Comput (P2,s2,I)))),(Comput (P2,s2,I))) 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,(CurInstr (P2,(Comput (P2,s2,I))))) 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,(CurInstr (P2,(Comput (P2,s2,I))))) . (Comput (P2,s2,I)) is set
IC (Following (P2,(Comput (P2,s2,I)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Following (P2,(Comput (P2,s2,I)))) . (IC ) is set
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
n + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
- 4 is V11() V12() integer ext-real non positive set
(n + 4) + (- 4) is V11() V12() integer ext-real set
abs ((n + 4) + (- 4)) 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
i + (- 1) is V11() V12() integer ext-real set
abs (i + (- 1)) 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
Comput (P2,s2,I) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P2,s2,I)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,I)) . (IC ) is set
I + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (P2,s2,(I + 1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P2,s2,(I + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,(I + 1))) . (IC ) is set
I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
Comput (P2,s2,I) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P2,s2,I)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,I)) . (IC ) is set
proj1 P2 is set
CurInstr (P2,(Comput (P2,s2,I))) is Element of the InstructionsF of SCMPDS
P2 /. (IC (Comput (P2,s2,I))) is Element of the InstructionsF of SCMPDS
Comput (P2,s2,0) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P2,s2,0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,0)) . (IC ) is set
SI is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P2,s2,SI) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P2,s2,SI)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,SI)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,SI))) is Element of the InstructionsF of SCMPDS
P2 . (IC (Comput (P2,s2,SI))) is Element of the InstructionsF of SCMPDS
CurInstr (P2,(Comput (P2,s2,SI))) is Element of the InstructionsF of SCMPDS
P2 . (IC s2) is Element of the InstructionsF of SCMPDS
CurInstr (P2,(Comput (P2,s2,SI))) is Element of the InstructionsF of SCMPDS
P2 . (succ (IC s2)) is Element of the InstructionsF of SCMPDS
s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P1 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set
dom P1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
P2 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
s1 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
I is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
SI is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (I,P2,n) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Comput (SI,s1,n) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (I,P2,(n + 1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Comput (SI,s1,(n + 1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Following (SI,(Comput (SI,s1,n))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
CurInstr (SI,(Comput (SI,s1,n))) is Element of the InstructionsF of SCMPDS
IC (Comput (SI,s1,n)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (SI,s1,n)) . (IC ) is set
SI /. (IC (Comput (SI,s1,n))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (SI,(Comput (SI,s1,n)))),(Comput (SI,s1,n))) 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,(CurInstr (SI,(Comput (SI,s1,n))))) 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,(CurInstr (SI,(Comput (SI,s1,n))))) . (Comput (SI,s1,n)) is set
Following (I,(Comput (I,P2,n))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
CurInstr (I,(Comput (I,P2,n))) is Element of the InstructionsF of SCMPDS
IC (Comput (I,P2,n)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (I,P2,n)) . (IC ) is set
I /. (IC (Comput (I,P2,n))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (I,(Comput (I,P2,n)))),(Comput (I,P2,n))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 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,(CurInstr (I,(Comput (I,P2,n))))) 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,(CurInstr (I,(Comput (I,P2,n))))) . (Comput (I,P2,n)) is set
I . (IC (Comput (I,P2,n))) is Element of the InstructionsF of SCMPDS
SI . (IC (Comput (SI,s1,n))) is Element of the InstructionsF of SCMPDS
P1 . (IC (Comput (I,P2,n))) is set
Comput (I,P2,0) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Comput (SI,s1,0) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible 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
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
P1 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started set
dom (stop s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
s1 is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Comput (s1,P1,P2) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (s1,P1,P2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (s1,P1,P2)) . (IC ) is set
I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
Comput (s1,P1,I) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (s1,P1,I)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (s1,P1,I)) . (IC ) is set
SI 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
Comput (s1,P1,n) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (s1,P1,n)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (s1,P1,n)) . (IC ) is set
Comput (s1,P1,SI) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (s1,P1,SI)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (s1,P1,SI)) . (IC ) is set
succ (IC (Comput (s1,P1,SI))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
(IC (Comput (s1,P1,SI))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
((IC (Comput (s1,P1,SI))),(succ (IC (Comput (s1,P1,SI))))) --> ((goto 1),(goto (- 1))) is non empty Relation-like {(IC (Comput (s1,P1,SI))),(succ (IC (Comput (s1,P1,SI))))} -defined the InstructionsF of SCMPDS -valued Function-like V29({(IC (Comput (s1,P1,SI))),(succ (IC (Comput (s1,P1,SI))))}, the InstructionsF of SCMPDS) finite V43() V136() Element of K6(K7({(IC (Comput (s1,P1,SI))),(succ (IC (Comput (s1,P1,SI))))}, the InstructionsF of SCMPDS))
{(IC (Comput (s1,P1,SI))),(succ (IC (Comput (s1,P1,SI))))} is finite V43() set
K7({(IC (Comput (s1,P1,SI))),(succ (IC (Comput (s1,P1,SI))))}, the InstructionsF of SCMPDS) is set
K6(K7({(IC (Comput (s1,P1,SI))),(succ (IC (Comput (s1,P1,SI))))}, the InstructionsF of SCMPDS)) is set
s1 +* (((IC (Comput (s1,P1,SI))),(succ (IC (Comput (s1,P1,SI))))) --> ((goto 1),(goto (- 1)))) is non empty Relation-like the InstructionsF of SCMPDS -valued Function-like set
s1 +* ((IC (Comput (s1,P1,SI))),(goto 1)) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
i is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
i +* ((succ (IC (Comput (s1,P1,SI)))),(goto (- 1))) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
m is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
c is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Comput (m,P1,SI) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 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)
P1 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
(Load (halt SCMPDS)) . P1 is set
P2 is Element of the InstructionsF of SCMPDS
InsCode P2 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(P2) is set
K90(K90(P2)) is set
s2 is Element of the InstructionsF of SCMPDS
P1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
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
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
(s1,I) <>0_goto SI is Element of the InstructionsF of SCMPDS
K177(s1,I,SI) is set
[4,{},K177(s1,I,SI)] is V26() V27() set
[4,{}] is V26() set
{4,{}} is finite V43() set
{4} is finite V43() set
{{4,{}},{4}} is finite V36() V43() set
[[4,{}],K177(s1,I,SI)] is V26() set
{[4,{}],K177(s1,I,SI)} is finite V43() set
{[4,{}]} is Function-like finite V43() set
{{[4,{}],K177(s1,I,SI)},{[4,{}]}} is finite V36() V43() set
P1 + SI is V11() V12() integer ext-real set
n is Int-like Element of the carrier of SCMPDS
i is V11() V12() integer ext-real set
m is V11() V12() integer ext-real set
(n,i) <>0_goto m is Element of the InstructionsF of SCMPDS
K177(n,i,m) is set
[4,{},K177(n,i,m)] is V26() V27() set
[[4,{}],K177(n,i,m)] is V26() set
{[4,{}],K177(n,i,m)} is finite V43() set
{{[4,{}],K177(n,i,m)},{[4,{}]}} is finite V36() V43() set
P2 + m is V11() V12() integer ext-real set
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
(s1,I) >=0_goto SI is Element of the InstructionsF of SCMPDS
K177(s1,I,SI) is set
[6,{},K177(s1,I,SI)] is V26() V27() set
[6,{}] is V26() set
{6,{}} is finite V43() set
{6} is finite V43() set
{{6,{}},{6}} is finite V36() V43() set
[[6,{}],K177(s1,I,SI)] is V26() set
{[6,{}],K177(s1,I,SI)} is finite V43() set
{[6,{}]} is Function-like finite V43() set
{{[6,{}],K177(s1,I,SI)},{[6,{}]}} is finite V36() V43() set
P1 + SI is V11() V12() integer ext-real set
n is Int-like Element of the carrier of SCMPDS
i is V11() V12() integer ext-real set
m is V11() V12() integer ext-real set
(n,i) >=0_goto m is Element of the InstructionsF of SCMPDS
K177(n,i,m) is set
[6,{},K177(n,i,m)] is V26() V27() set
[[6,{}],K177(n,i,m)] is V26() set
{[6,{}],K177(n,i,m)} is finite V43() set
{{[6,{}],K177(n,i,m)},{[6,{}]}} is finite V36() V43() set
P2 + m is V11() V12() integer ext-real set
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
(s1,I) <=0_goto SI is Element of the InstructionsF of SCMPDS
K177(s1,I,SI) is set
[5,{},K177(s1,I,SI)] is V26() V27() set
[5,{}] is V26() set
{5,{}} is finite V43() set
{5} is finite V43() set
{{5,{}},{5}} is finite V36() V43() set
[[5,{}],K177(s1,I,SI)] is V26() set
{[5,{}],K177(s1,I,SI)} is finite V43() set
{[5,{}]} is Function-like finite V43() set
{{[5,{}],K177(s1,I,SI)},{[5,{}]}} is finite V36() V43() set
P1 + SI is V11() V12() integer ext-real set
n is Int-like Element of the carrier of SCMPDS
i is V11() V12() integer ext-real set
m is V11() V12() integer ext-real set
(n,i) <=0_goto m is Element of the InstructionsF of SCMPDS
K177(n,i,m) is set
[5,{},K177(n,i,m)] is V26() V27() set
[[5,{}],K177(n,i,m)] is V26() set
{[5,{}],K177(n,i,m)} is finite V43() set
{{[5,{}],K177(n,i,m)},{[5,{}]}} is finite V36() V43() set
P2 + m is V11() V12() integer ext-real set
s1 is V11() V12() integer ext-real set
goto s1 is Element of the InstructionsF of SCMPDS
K175(s1) is Relation-like Function-like set
[14,{},K175(s1)] is V26() V27() set
[[14,{}],K175(s1)] is V26() set
{[14,{}],K175(s1)} is finite V43() set
{{[14,{}],K175(s1)},{[14,{}]}} is finite V36() V43() set
P1 + s1 is V11() V12() integer ext-real set
I is V11() V12() integer ext-real set
goto I is Element of the InstructionsF of SCMPDS
K175(I) is Relation-like Function-like set
[14,{},K175(I)] is V26() V27() set
[[14,{}],K175(I)] is V26() set
{[14,{}],K175(I)} is finite V43() set
{{[14,{}],K175(I)},{[14,{}]}} is finite V36() V43() set
P2 + I is V11() V12() integer ext-real set
s1 is V11() V12() integer ext-real set
goto s1 is Element of the InstructionsF of SCMPDS
K175(s1) is Relation-like Function-like set
[14,{},K175(s1)] is V26() V27() set
[[14,{}],K175(s1)] is V26() set
{[14,{}],K175(s1)} is finite V43() set
{{[14,{}],K175(s1)},{[14,{}]}} is finite V36() V43() set
P2 + s1 is V11() V12() integer ext-real set
I is Int-like Element of the carrier of SCMPDS
SI is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
(I,SI) <>0_goto n is Element of the InstructionsF of SCMPDS
K177(I,SI,n) is set
[4,{},K177(I,SI,n)] is V26() V27() set
[[4,{}],K177(I,SI,n)] is V26() set
{[4,{}],K177(I,SI,n)} is finite V43() set
{{[4,{}],K177(I,SI,n)},{[4,{}]}} is finite V36() V43() set
P2 + n is V11() V12() integer ext-real set
i is Int-like Element of the carrier of SCMPDS
m is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
(i,m) <=0_goto i is Element of the InstructionsF of SCMPDS
K177(i,m,i) is set
[5,{},K177(i,m,i)] is V26() V27() set
[[5,{}],K177(i,m,i)] is V26() set
{[5,{}],K177(i,m,i)} is finite V43() set
{{[5,{}],K177(i,m,i)},{[5,{}]}} is finite V36() V43() set
P2 + i is V11() V12() integer ext-real set
l is Int-like Element of the carrier of SCMPDS
c is V11() V12() integer ext-real set
c₁₃ is V11() V12() integer ext-real set
(l,c) >=0_goto c₁₃ is Element of the InstructionsF of SCMPDS
K177(l,c,c₁₃) is set
[6,{},K177(l,c,c₁₃)] is V26() V27() set
[[6,{}],K177(l,c,c₁₃)] is V26() set
{[6,{}],K177(l,c,c₁₃)} is finite V43() set
{{[6,{}],K177(l,c,c₁₃)},{[6,{}]}} is finite V36() V43() set
P2 + c₁₃ is V11() V12() integer ext-real set
DataLoc (0,0) is Int-like Element of the carrier of SCMPDS
0 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
abs (0 + 0) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs (0 + 0))] is V26() set
{1,(abs (0 + 0))} is finite V43() set
{1} is finite V43() set
{{1,(abs (0 + 0))},{1}} is finite V36() V43() set
(DataLoc (0,0)) := 1 is Element of the InstructionsF of SCMPDS
K176((DataLoc (0,0)),1) is set
[2,{},K176((DataLoc (0,0)),1)] 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((DataLoc (0,0)),1)] is V26() set
{[2,{}],K176((DataLoc (0,0)),1)} is finite V43() set
{[2,{}]} is Function-like finite V43() set
{{[2,{}],K176((DataLoc (0,0)),1)},{[2,{}]}} is finite V36() 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
s2 is Int-like Element of the carrier of SCMPDS
P1 is V11() V12() integer ext-real set
s2 := P1 is Element of the InstructionsF of SCMPDS
K176(s2,P1) is set
[2,{},K176(s2,P1)] 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(s2,P1)] is V26() set
{[2,{}],K176(s2,P1)} is finite V43() set
{[2,{}]} is Function-like finite V43() set
{{[2,{}],K176(s2,P1)},{[2,{}]}} is finite V36() V43() set
InsCode (s2 := P1) 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 := P1)) is set
K90(K90((s2 := P1))) is set
s2 is Int-like Element of the carrier of SCMPDS
P1 is V11() V12() integer ext-real set
P2 is V11() V12() integer ext-real set
(s2,P1) := P2 is Element of the InstructionsF of SCMPDS
K177(s2,P1,P2) is set
[7,{},K177(s2,P1,P2)] 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(s2,P1,P2)] is V26() set
{[7,{}],K177(s2,P1,P2)} is finite V43() set
{[7,{}]} is Function-like finite V43() set
{{[7,{}],K177(s2,P1,P2)},{[7,{}]}} is finite V36() V43() set
InsCode ((s2,P1) := P2) 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,P1) := P2)) is set
K90(K90(((s2,P1) := P2))) is set
s2 is Int-like Element of the carrier of SCMPDS
P1 is V11() V12() integer ext-real set
P2 is V11() V12() integer ext-real set
AddTo (s2,P1,P2) is Element of the InstructionsF of SCMPDS
K177(s2,P1,P2) is set
[8,{},K177(s2,P1,P2)] 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(s2,P1,P2)] is V26() set
{[8,{}],K177(s2,P1,P2)} is finite V43() set
{[8,{}]} is Function-like finite V43() set
{{[8,{}],K177(s2,P1,P2)},{[8,{}]}} is finite V36() V43() set
InsCode (AddTo (s2,P1,P2)) 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((AddTo (s2,P1,P2))) is set
K90(K90((AddTo (s2,P1,P2)))) is set
s2 is Int-like Element of the carrier of SCMPDS
P1 is Int-like Element of the carrier of SCMPDS
P2 is V11() V12() integer ext-real set
s1 is V11() V12() integer ext-real set
AddTo (s2,P2,P1,s1) is Element of the InstructionsF of SCMPDS
InsCode (AddTo (s2,P2,P1,s1)) 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((AddTo (s2,P2,P1,s1))) is set
K90(K90((AddTo (s2,P2,P1,s1)))) is set
SubFrom (s2,P2,P1,s1) is Element of the InstructionsF of SCMPDS
InsCode (SubFrom (s2,P2,P1,s1)) 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((SubFrom (s2,P2,P1,s1))) is set
K90(K90((SubFrom (s2,P2,P1,s1)))) is set
MultBy (s2,P2,P1,s1) is Element of the InstructionsF of SCMPDS
InsCode (MultBy (s2,P2,P1,s1)) 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((MultBy (s2,P2,P1,s1))) is set
K90(K90((MultBy (s2,P2,P1,s1)))) is set
Divide (s2,P2,P1,s1) is Element of the InstructionsF of SCMPDS
InsCode (Divide (s2,P2,P1,s1)) 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((Divide (s2,P2,P1,s1))) is set
K90(K90((Divide (s2,P2,P1,s1)))) is set
(s2,P2) := (P1,s1) is Element of the InstructionsF of SCMPDS
InsCode ((s2,P2) := (P1,s1)) 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,P2) := (P1,s1))) is set
K90(K90(((s2,P2) := (P1,s1)))) 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
dom P1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
{ (b₁ + (card s2)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : b₁ in dom P1 } is set
I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (s2,P1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
SI is Element of the InstructionsF of SCMPDS
(s2,P1) . I is set
proj1 (Shift (P1,(card s2))) is set
dom s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
(dom s2) \/ { (b₁ + (card s2)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : b₁ in dom P1 } is set
s2 . I is set
InsCode SI 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(SI) is set
K90(K90(SI)) is set
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
n + (card s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P1 . n is set
InsCode SI 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(SI) is set
K90(K90(SI)) is 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
P2 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
P1 . P2 is set
s1 is Element of the InstructionsF of SCMPDS
InsCode s1 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(s1) is set
K90(K90(s1)) is set
dom P1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
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
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
(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
(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
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 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
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
s2 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
P1 is V11() V12() integer ext-real set
(card s2) + P1 is V11() V12() integer ext-real set
goto P1 is Element of the InstructionsF of SCMPDS
K175(P1) is Relation-like Function-like set
[14,{},K175(P1)] is V26() V27() set
[[14,{}],K175(P1)] is V26() set
{[14,{}],K175(P1)} is finite V43() set
{{[14,{}],K175(P1)},{[14,{}]}} is finite V36() V43() set
(s2,(goto P1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set
Load (goto 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,(goto P1)) is non empty V2() finite V43() set
K334({0},(goto P1)) is Relation-like {0} -defined {(goto P1)} -valued Function-like V29({0},{(goto P1)}) finite V43() V136() Element of K6(K7({0},{(goto P1)}))
{(goto P1)} is finite V43() set
K7({0},{(goto P1)}) is finite V43() set
K6(K7({0},{(goto P1)})) is finite V36() V43() set
(s2,(Load (goto P1))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set
Shift ((Load (goto P1)),(card s2)) is Relation-like Function-like set
s2 +* (Shift ((Load (goto P1)),(card s2))) is non empty Relation-like Function-like set
dom (Load (goto P1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
{ (b₁ + (card s2)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : b₁ in dom (Load (goto P1)) } is set
SI is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (s2,(goto P1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
n is Element of the InstructionsF of SCMPDS
(s2,(goto P1)) . SI is set
proj1 (Shift ((Load (goto P1)),(card s2))) is set
dom s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
(dom s2) \/ { (b₁ + (card s2)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : b₁ in dom (Load (goto P1)) } is set
s2 . SI is set
InsCode n 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(n) is set
K90(K90(n)) is set
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i + (card s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Load (goto P1)) . i is set
InsCode n 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(n) is set
K90(K90(n)) is set
s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
goto s2 is Element of the InstructionsF of SCMPDS
K175(s2) is Relation-like Function-like set
[14,{},K175(s2)] is V26() V27() set
[[14,{}],K175(s2)] is V26() set
{[14,{}],K175(s2)} is finite V43() set
{{[14,{}],K175(s2)},{[14,{}]}} is finite V36() V43() set
Load (goto 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,(goto s2)) is non empty V2() finite V43() set
K334({0},(goto s2)) is Relation-like {0} -defined {(goto s2)} -valued Function-like V29({0},{(goto s2)}) finite V43() V136() Element of K6(K7({0},{(goto s2)}))
{(goto s2)} is finite V43() set
K7({0},{(goto s2)}) is finite V43() set
K6(K7({0},{(goto s2)})) is finite V36() V43() set
s1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (Load (goto s2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
I is Element of the InstructionsF of SCMPDS
(Load (goto s2)) . s1 is set
InsCode I 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(I) is set
K90(K90(I)) is set
s1 + s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
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 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
P2 is V11() V12() integer ext-real set
(card s2) + P2 is V11() V12() integer ext-real set
P1 is V11() V12() integer ext-real set
s1 is Int-like Element of the carrier of SCMPDS
(s1,P1) <>0_goto P2 is Element of the InstructionsF of SCMPDS
K177(s1,P1,P2) is set
[4,{},K177(s1,P1,P2)] is V26() V27() set
[4,{}] is V26() set
{4,{}} is finite V43() set
{4} is finite V43() set
{{4,{}},{4}} is finite V36() V43() set
[[4,{}],K177(s1,P1,P2)] is V26() set
{[4,{}],K177(s1,P1,P2)} is finite V43() set
{[4,{}]} is Function-like finite V43() set
{{[4,{}],K177(s1,P1,P2)},{[4,{}]}} is finite V36() V43() set
(s2,((s1,P1) <>0_goto P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set
Load ((s1,P1) <>0_goto 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,((s1,P1) <>0_goto P2)) is non empty V2() finite V43() set
K334({0},((s1,P1) <>0_goto P2)) is Relation-like {0} -defined {((s1,P1) <>0_goto P2)} -valued Function-like V29({0},{((s1,P1) <>0_goto P2)}) finite V43() V136() Element of K6(K7({0},{((s1,P1) <>0_goto P2)}))
{((s1,P1) <>0_goto P2)} is finite V43() set
K7({0},{((s1,P1) <>0_goto P2)}) is finite V43() set
K6(K7({0},{((s1,P1) <>0_goto P2)})) is finite V36() V43() set
(s2,(Load ((s1,P1) <>0_goto P2))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set
Shift ((Load ((s1,P1) <>0_goto P2)),(card s2)) is Relation-like Function-like set
s2 +* (Shift ((Load ((s1,P1) <>0_goto P2)),(card s2))) is non empty Relation-like Function-like set
dom (Load ((s1,P1) <>0_goto P2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
{ (b₁ + (card s2)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : b₁ in dom (Load ((s1,P1) <>0_goto P2)) } is set
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (s2,((s1,P1) <>0_goto P2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
i is Element of the InstructionsF of SCMPDS
(s2,((s1,P1) <>0_goto P2)) . m is set
proj1 (Shift ((Load ((s1,P1) <>0_goto P2)),(card s2))) is set
dom s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
(dom s2) \/ { (b₁ + (card s2)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : b₁ in dom (Load ((s1,P1) <>0_goto P2)) } is set
s2 . m is set
InsCode i 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(i) is set
K90(K90(i)) is set
l is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
l + (card s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Load ((s1,P1) <>0_goto P2)) . l is set
InsCode i 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(i) is set
K90(K90(i)) is set
P1 is Int-like Element of the carrier of SCMPDS
s2 is V11() V12() integer ext-real set
P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(P1,s2) <>0_goto P2 is Element of the InstructionsF of SCMPDS
K177(P1,s2,P2) is set
[4,{},K177(P1,s2,P2)] is V26() V27() set
[4,{}] is V26() set
{4,{}} is finite V43() set
{4} is finite V43() set
{{4,{}},{4}} is finite V36() V43() set
[[4,{}],K177(P1,s2,P2)] is V26() set
{[4,{}],K177(P1,s2,P2)} is finite V43() set
{[4,{}]} is Function-like finite V43() set
{{[4,{}],K177(P1,s2,P2)},{[4,{}]}} is finite V36() V43() set
Load ((P1,s2) <>0_goto 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,((P1,s2) <>0_goto P2)) is non empty V2() finite V43() set
K334({0},((P1,s2) <>0_goto P2)) is Relation-like {0} -defined {((P1,s2) <>0_goto P2)} -valued Function-like V29({0},{((P1,s2) <>0_goto P2)}) finite V43() V136() Element of K6(K7({0},{((P1,s2) <>0_goto P2)}))
{((P1,s2) <>0_goto P2)} is finite V43() set
K7({0},{((P1,s2) <>0_goto P2)}) is finite V43() set
K6(K7({0},{((P1,s2) <>0_goto P2)})) is finite V36() V43() set
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (Load ((P1,s2) <>0_goto P2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
i is Element of the InstructionsF of SCMPDS
(Load ((P1,s2) <>0_goto P2)) . n is set
InsCode i 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(i) is set
K90(K90(i)) is set
n + P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
n is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set
s2 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
P2 is V11() V12() integer ext-real set
(card s2) + P2 is V11() V12() integer ext-real set
P1 is V11() V12() integer ext-real set
s1 is Int-like Element of the carrier of SCMPDS
(s1,P1) <=0_goto P2 is Element of the InstructionsF of SCMPDS
K177(s1,P1,P2) is set
[5,{},K177(s1,P1,P2)] is V26() V27() set
[5,{}] is V26() set
{5,{}} is finite V43() set
{5} is finite V43() set
{{5,{}},{5}} is finite V36() V43() set
[[5,{}],K177(s1,P1,P2)] is V26() set
{[5,{}],K177(s1,P1,P2)} is finite V43() set
{[5,{}]} is Function-like finite V43() set
{{[5,{}],K177(s1,P1,P2)},{[5,{}]}} is finite V36() V43() set
(s2,((s1,P1) <=0_goto P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set
Load ((s1,P1) <=0_goto 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,((s1,P1) <=0_goto P2)) is non empty V2() finite V43() set
K334({0},((s1,P1) <=0_goto P2)) is Relation-like {0} -defined {((s1,P1) <=0_goto P2)} -valued Function-like V29({0},{((s1,P1) <=0_goto P2)}) finite V43() V136() Element of K6(K7({0},{((s1,P1) <=0_goto P2)}))
{((s1,P1) <=0_goto P2)} is finite V43() set
K7({0},{((s1,P1) <=0_goto P2)}) is finite V43() set
K6(K7({0},{((s1,P1) <=0_goto P2)})) is finite V36() V43() set
(s2,(Load ((s1,P1) <=0_goto P2))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set
Shift ((Load ((s1,P1) <=0_goto P2)),(card s2)) is Relation-like Function-like set
s2 +* (Shift ((Load ((s1,P1) <=0_goto P2)),(card s2))) is non empty Relation-like Function-like set
dom (Load ((s1,P1) <=0_goto P2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
{ (b₁ + (card s2)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : b₁ in dom (Load ((s1,P1) <=0_goto P2)) } is set
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (s2,((s1,P1) <=0_goto P2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
i is Element of the InstructionsF of SCMPDS
(s2,((s1,P1) <=0_goto P2)) . m is set
proj1 (Shift ((Load ((s1,P1) <=0_goto P2)),(card s2))) is set
dom s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
(dom s2) \/ { (b₁ + (card s2)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : b₁ in dom (Load ((s1,P1) <=0_goto P2)) } is set
s2 . m is set
InsCode i 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(i) is set
K90(K90(i)) is set
l is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
l + (card s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Load ((s1,P1) <=0_goto P2)) . l is set
InsCode i 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(i) is set
K90(K90(i)) is set
P1 is Int-like Element of the carrier of SCMPDS
s2 is V11() V12() integer ext-real set
P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(P1,s2) <=0_goto P2 is Element of the InstructionsF of SCMPDS
K177(P1,s2,P2) is set
[5,{},K177(P1,s2,P2)] is V26() V27() set
[5,{}] is V26() set
{5,{}} is finite V43() set
{5} is finite V43() set
{{5,{}},{5}} is finite V36() V43() set
[[5,{}],K177(P1,s2,P2)] is V26() set
{[5,{}],K177(P1,s2,P2)} is finite V43() set
{[5,{}]} is Function-like finite V43() set
{{[5,{}],K177(P1,s2,P2)},{[5,{}]}} is finite V36() V43() set
Load ((P1,s2) <=0_goto 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,((P1,s2) <=0_goto P2)) is non empty V2() finite V43() set
K334({0},((P1,s2) <=0_goto P2)) is Relation-like {0} -defined {((P1,s2) <=0_goto P2)} -valued Function-like V29({0},{((P1,s2) <=0_goto P2)}) finite V43() V136() Element of K6(K7({0},{((P1,s2) <=0_goto P2)}))
{((P1,s2) <=0_goto P2)} is finite V43() set
K7({0},{((P1,s2) <=0_goto P2)}) is finite V43() set
K6(K7({0},{((P1,s2) <=0_goto P2)})) is finite V36() V43() set
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (Load ((P1,s2) <=0_goto P2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
i is Element of the InstructionsF of SCMPDS
(Load ((P1,s2) <=0_goto P2)) . n is set
InsCode i 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(i) is set
K90(K90(i)) is set
n + P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
n is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set
s2 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
P2 is V11() V12() integer ext-real set
(card s2) + P2 is V11() V12() integer ext-real set
P1 is V11() V12() integer ext-real set
s1 is Int-like Element of the carrier of SCMPDS
(s1,P1) >=0_goto P2 is Element of the InstructionsF of SCMPDS
K177(s1,P1,P2) is set
[6,{},K177(s1,P1,P2)] is V26() V27() set
[6,{}] is V26() set
{6,{}} is finite V43() set
{6} is finite V43() set
{{6,{}},{6}} is finite V36() V43() set
[[6,{}],K177(s1,P1,P2)] is V26() set
{[6,{}],K177(s1,P1,P2)} is finite V43() set
{[6,{}]} is Function-like finite V43() set
{{[6,{}],K177(s1,P1,P2)},{[6,{}]}} is finite V36() V43() set
(s2,((s1,P1) >=0_goto P2)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set
Load ((s1,P1) >=0_goto 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,((s1,P1) >=0_goto P2)) is non empty V2() finite V43() set
K334({0},((s1,P1) >=0_goto P2)) is Relation-like {0} -defined {((s1,P1) >=0_goto P2)} -valued Function-like V29({0},{((s1,P1) >=0_goto P2)}) finite V43() V136() Element of K6(K7({0},{((s1,P1) >=0_goto P2)}))
{((s1,P1) >=0_goto P2)} is finite V43() set
K7({0},{((s1,P1) >=0_goto P2)}) is finite V43() set
K6(K7({0},{((s1,P1) >=0_goto P2)})) is finite V36() V43() set
(s2,(Load ((s1,P1) >=0_goto P2))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() set
Shift ((Load ((s1,P1) >=0_goto P2)),(card s2)) is Relation-like Function-like set
s2 +* (Shift ((Load ((s1,P1) >=0_goto P2)),(card s2))) is non empty Relation-like Function-like set
dom (Load ((s1,P1) >=0_goto P2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
{ (b₁ + (card s2)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : b₁ in dom (Load ((s1,P1) >=0_goto P2)) } is set
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (s2,((s1,P1) >=0_goto P2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
i is Element of the InstructionsF of SCMPDS
(s2,((s1,P1) >=0_goto P2)) . m is set
proj1 (Shift ((Load ((s1,P1) >=0_goto P2)),(card s2))) is set
dom s2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
(dom s2) \/ { (b₁ + (card s2)) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : b₁ in dom (Load ((s1,P1) >=0_goto P2)) } is set
s2 . m is set
InsCode i 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(i) is set
K90(K90(i)) is set
l is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
l + (card s2) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Load ((s1,P1) >=0_goto P2)) . l is set
InsCode i 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(i) is set
K90(K90(i)) is set
P1 is Int-like Element of the carrier of SCMPDS
s2 is V11() V12() integer ext-real set
P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(P1,s2) >=0_goto P2 is Element of the InstructionsF of SCMPDS
K177(P1,s2,P2) is set
[6,{},K177(P1,s2,P2)] is V26() V27() set
[6,{}] is V26() set
{6,{}} is finite V43() set
{6} is finite V43() set
{{6,{}},{6}} is finite V36() V43() set
[[6,{}],K177(P1,s2,P2)] is V26() set
{[6,{}],K177(P1,s2,P2)} is finite V43() set
{[6,{}]} is Function-like finite V43() set
{{[6,{}],K177(P1,s2,P2)},{[6,{}]}} is finite V36() V43() set
Load ((P1,s2) >=0_goto 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,((P1,s2) >=0_goto P2)) is non empty V2() finite V43() set
K334({0},((P1,s2) >=0_goto P2)) is Relation-like {0} -defined {((P1,s2) >=0_goto P2)} -valued Function-like V29({0},{((P1,s2) >=0_goto P2)}) finite V43() V136() Element of K6(K7({0},{((P1,s2) >=0_goto P2)}))
{((P1,s2) >=0_goto P2)} is finite V43() set
K7({0},{((P1,s2) >=0_goto P2)}) is finite V43() set
K6(K7({0},{((P1,s2) >=0_goto P2)})) is finite V36() V43() set
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (Load ((P1,s2) >=0_goto P2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
i is Element of the InstructionsF of SCMPDS
(Load ((P1,s2) >=0_goto P2)) . n is set
InsCode i 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(i) is set
K90(K90(i)) is set
n + P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
n is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() 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
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
s1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(IC s2) + P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
I is V11() V12() integer ext-real set
s1 + I is V11() V12() integer ext-real set
ICplusConst (s2,I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(ICplusConst (s2,I)) + P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
ICplusConst (P1,I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
SI 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
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i + I is V11() V12() integer ext-real set
abs (i + I) 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
i + I is V11() V12() integer ext-real set
abs (i + I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
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
DataPart s2 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
s2 | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
DataPart P1 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
P1 | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
s1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(IC s2) + P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
I is Element of the InstructionsF of SCMPDS
InsCode I 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(I) is set
K90(K90(I)) is set
Exec (I,s2) 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,I) 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,I) . s2 is set
IC (Exec (I,s2)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Exec (I,s2)) . (IC ) is set
(IC (Exec (I,s2))) + P2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Exec (I,P1) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 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,I) . P1 is set
IC (Exec (I,P1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Exec (I,P1)) . (IC ) is set
DataPart (Exec (I,s2)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Exec (I,s2)) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
DataPart (Exec (I,P1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Exec (I,P1)) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
SI is Int-like Element of the carrier of SCMPDS
s2 . SI is V11() V12() integer ext-real set
n is V11() V12() integer ext-real set
DataLoc ((s2 . SI),n) is Int-like Element of the carrier of SCMPDS
(s2 . SI) + n is V11() V12() integer ext-real set
abs ((s2 . SI) + n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . SI) + n))] is V26() set
{1,(abs ((s2 . SI) + n))} is finite V43() set
{1} is finite V43() set
{{1,(abs ((s2 . SI) + n))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . SI),n)) is V11() V12() integer ext-real set
P1 . SI is V11() V12() integer ext-real set
DataLoc ((P1 . SI),n) is Int-like Element of the carrier of SCMPDS
(P1 . SI) + n is V11() V12() integer ext-real set
abs ((P1 . SI) + n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . SI) + n))] is V26() set
{1,(abs ((P1 . SI) + n))} is finite V43() set
{{1,(abs ((P1 . SI) + n))},{1}} is finite V36() V43() set
s2 . (DataLoc ((P1 . SI),n)) is V11() V12() integer ext-real set
P1 . (DataLoc ((P1 . SI),n)) is V11() V12() integer ext-real 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
(succ (IC s2)) + P2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
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
i is V11() V12() integer ext-real set
goto i is Element of the InstructionsF of SCMPDS
K175(i) is Relation-like Function-like set
[14,{},K175(i)] is V26() V27() set
[[14,{}],K175(i)] is V26() set
{[14,{}],K175(i)} is finite V43() set
{{[14,{}],K175(i)},{[14,{}]}} is finite V36() V43() set
s1 + i is V11() V12() integer ext-real set
ICplusConst (s2,i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
ICplusConst (P1,i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
m is Int-like Element of the carrier of SCMPDS
(Exec (I,s2)) . m is V11() V12() integer ext-real set
s2 . m is V11() V12() integer ext-real set
P1 . m is V11() V12() integer ext-real set
(Exec (I,P1)) . m is V11() V12() integer ext-real set
i is Int-like Element of the carrier of SCMPDS
m is V11() V12() integer ext-real set
i := m is () Element of the InstructionsF of SCMPDS
K176(i,m) is set
[2,{},K176(i,m)] is V26() V27() set
[[2,{}],K176(i,m)] is V26() set
{[2,{}],K176(i,m)} is finite V43() set
{{[2,{}],K176(i,m)},{[2,{}]}} is finite V36() V43() set
i is Int-like Element of the carrier of SCMPDS
(Exec (I,s2)) . i is V11() V12() integer ext-real set
(Exec (I,P1)) . i is V11() V12() integer ext-real set
i is Int-like Element of the carrier of SCMPDS
(Exec (I,s2)) . i is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
P1 . i is V11() V12() integer ext-real set
(Exec (I,P1)) . i is V11() V12() integer ext-real set
i is Int-like Element of the carrier of SCMPDS
i is Int-like Element of the carrier of SCMPDS
m is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
(i,m) <>0_goto i is Element of the InstructionsF of SCMPDS
K177(i,m,i) is set
[4,{},K177(i,m,i)] is V26() V27() set
[[4,{}],K177(i,m,i)] is V26() set
{[4,{}],K177(i,m,i)} is finite V43() set
{{[4,{}],K177(i,m,i)},{[4,{}]}} is finite V36() V43() set
s1 + i is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . i),m)) is V11() V12() integer ext-real set
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),m) is Int-like Element of the carrier of SCMPDS
(P1 . i) + m is V11() V12() integer ext-real set
abs ((P1 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + m))] is V26() set
{1,(abs ((P1 . i) + m))} is finite V43() set
{{1,(abs ((P1 . i) + m))},{1}} is finite V36() V43() set
P1 . (DataLoc ((P1 . i),m)) is V11() V12() integer ext-real set
ICplusConst (s2,i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
ICplusConst (P1,i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . i),m)) is V11() V12() integer ext-real set
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),m) is Int-like Element of the carrier of SCMPDS
(P1 . i) + m is V11() V12() integer ext-real set
abs ((P1 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + m))] is V26() set
{1,(abs ((P1 . i) + m))} is finite V43() set
{{1,(abs ((P1 . i) + m))},{1}} is finite V36() V43() set
P1 . (DataLoc ((P1 . i),m)) is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . i),m)) is V11() V12() integer ext-real set
l is Int-like Element of the carrier of SCMPDS
(Exec (I,s2)) . l is V11() V12() integer ext-real set
s2 . l is V11() V12() integer ext-real set
P1 . l is V11() V12() integer ext-real set
(Exec (I,P1)) . l is V11() V12() integer ext-real set
i is Int-like Element of the carrier of SCMPDS
m is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
(i,m) <=0_goto i is Element of the InstructionsF of SCMPDS
K177(i,m,i) is set
[5,{},K177(i,m,i)] is V26() V27() set
[[5,{}],K177(i,m,i)] is V26() set
{[5,{}],K177(i,m,i)} is finite V43() set
{{[5,{}],K177(i,m,i)},{[5,{}]}} is finite V36() V43() set
s1 + i is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . i),m)) is V11() V12() integer ext-real set
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),m) is Int-like Element of the carrier of SCMPDS
(P1 . i) + m is V11() V12() integer ext-real set
abs ((P1 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + m))] is V26() set
{1,(abs ((P1 . i) + m))} is finite V43() set
{{1,(abs ((P1 . i) + m))},{1}} is finite V36() V43() set
P1 . (DataLoc ((P1 . i),m)) is V11() V12() integer ext-real set
ICplusConst (s2,i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
ICplusConst (P1,i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . i),m)) is V11() V12() integer ext-real set
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),m) is Int-like Element of the carrier of SCMPDS
(P1 . i) + m is V11() V12() integer ext-real set
abs ((P1 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + m))] is V26() set
{1,(abs ((P1 . i) + m))} is finite V43() set
{{1,(abs ((P1 . i) + m))},{1}} is finite V36() V43() set
P1 . (DataLoc ((P1 . i),m)) is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . i),m)) is V11() V12() integer ext-real set
l is Int-like Element of the carrier of SCMPDS
(Exec (I,s2)) . l is V11() V12() integer ext-real set
s2 . l is V11() V12() integer ext-real set
P1 . l is V11() V12() integer ext-real set
(Exec (I,P1)) . l is V11() V12() integer ext-real set
i is Int-like Element of the carrier of SCMPDS
m is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
(i,m) >=0_goto i is Element of the InstructionsF of SCMPDS
K177(i,m,i) is set
[6,{},K177(i,m,i)] is V26() V27() set
[[6,{}],K177(i,m,i)] is V26() set
{[6,{}],K177(i,m,i)} is finite V43() set
{{[6,{}],K177(i,m,i)},{[6,{}]}} is finite V36() V43() set
s1 + i is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . i),m)) is V11() V12() integer ext-real set
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),m) is Int-like Element of the carrier of SCMPDS
(P1 . i) + m is V11() V12() integer ext-real set
abs ((P1 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + m))] is V26() set
{1,(abs ((P1 . i) + m))} is finite V43() set
{{1,(abs ((P1 . i) + m))},{1}} is finite V36() V43() set
P1 . (DataLoc ((P1 . i),m)) is V11() V12() integer ext-real set
ICplusConst (s2,i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
ICplusConst (P1,i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . i),m)) is V11() V12() integer ext-real set
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),m) is Int-like Element of the carrier of SCMPDS
(P1 . i) + m is V11() V12() integer ext-real set
abs ((P1 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + m))] is V26() set
{1,(abs ((P1 . i) + m))} is finite V43() set
{{1,(abs ((P1 . i) + m))},{1}} is finite V36() V43() set
P1 . (DataLoc ((P1 . i),m)) is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . i),m)) is V11() V12() integer ext-real set
l is Int-like Element of the carrier of SCMPDS
(Exec (I,s2)) . l is V11() V12() integer ext-real set
s2 . l is V11() V12() integer ext-real set
P1 . l is V11() V12() integer ext-real set
(Exec (I,P1)) . l is V11() V12() integer ext-real set
i is Int-like Element of the carrier of SCMPDS
m is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
(i,m) := i is () Element of the InstructionsF of SCMPDS
K177(i,m,i) is set
[7,{},K177(i,m,i)] is V26() V27() set
[[7,{}],K177(i,m,i)] is V26() set
{[7,{}],K177(i,m,i)} is finite V43() set
{{[7,{}],K177(i,m,i)},{[7,{}]}} is finite V36() V43() set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
l is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),m) is Int-like Element of the carrier of SCMPDS
(P1 . i) + m is V11() V12() integer ext-real set
abs ((P1 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + m))] is V26() set
{1,(abs ((P1 . i) + m))} is finite V43() set
{{1,(abs ((P1 . i) + m))},{1}} is finite V36() V43() set
(Exec (I,s2)) . l is V11() V12() integer ext-real set
(Exec (I,P1)) . l is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
l is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),m) is Int-like Element of the carrier of SCMPDS
(P1 . i) + m is V11() V12() integer ext-real set
abs ((P1 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + m))] is V26() set
{1,(abs ((P1 . i) + m))} is finite V43() set
{{1,(abs ((P1 . i) + m))},{1}} is finite V36() V43() set
(Exec (I,s2)) . l is V11() V12() integer ext-real set
s2 . l is V11() V12() integer ext-real set
P1 . l is V11() V12() integer ext-real set
(Exec (I,P1)) . l is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
l is Int-like Element of the carrier of SCMPDS
i is Int-like Element of the carrier of SCMPDS
m is V11() V12() integer ext-real set
i is V11() V12() integer ext-real set
AddTo (i,m,i) is () Element of the InstructionsF of SCMPDS
K177(i,m,i) is set
[8,{},K177(i,m,i)] is V26() V27() set
[[8,{}],K177(i,m,i)] is V26() set
{[8,{}],K177(i,m,i)} is finite V43() set
{{[8,{}],K177(i,m,i)},{[8,{}]}} is finite V36() V43() set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
l is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),m) is Int-like Element of the carrier of SCMPDS
(P1 . i) + m is V11() V12() integer ext-real set
abs ((P1 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + m))] is V26() set
{1,(abs ((P1 . i) + m))} is finite V43() set
{{1,(abs ((P1 . i) + m))},{1}} is finite V36() V43() set
(Exec (I,s2)) . l is V11() V12() integer ext-real set
s2 . (DataLoc ((s2 . i),m)) is V11() V12() integer ext-real set
(s2 . (DataLoc ((s2 . i),m))) + i is V11() V12() integer ext-real set
P1 . (DataLoc ((P1 . i),m)) is V11() V12() integer ext-real set
(P1 . (DataLoc ((P1 . i),m))) + i is V11() V12() integer ext-real set
(Exec (I,P1)) . l is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
l is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),m) is Int-like Element of the carrier of SCMPDS
(P1 . i) + m is V11() V12() integer ext-real set
abs ((P1 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + m))] is V26() set
{1,(abs ((P1 . i) + m))} is finite V43() set
{{1,(abs ((P1 . i) + m))},{1}} is finite V36() V43() set
(Exec (I,s2)) . l is V11() V12() integer ext-real set
s2 . l is V11() V12() integer ext-real set
P1 . l is V11() V12() integer ext-real set
(Exec (I,P1)) . l is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),m) is Int-like Element of the carrier of SCMPDS
(s2 . i) + m is V11() V12() integer ext-real set
abs ((s2 . i) + m) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + m))] is V26() set
{1,(abs ((s2 . i) + m))} is finite V43() set
{{1,(abs ((s2 . i) + m))},{1}} is finite V36() V43() set
l is Int-like Element of the carrier of SCMPDS
i is Int-like Element of the carrier of SCMPDS
m is Int-like Element of the carrier of SCMPDS
i is V11() V12() integer ext-real set
l is V11() V12() integer ext-real set
AddTo (i,i,m,l) is () Element of the InstructionsF of SCMPDS
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),i) is Int-like Element of the carrier of SCMPDS
(P1 . i) + i is V11() V12() integer ext-real set
abs ((P1 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + i))] is V26() set
{1,(abs ((P1 . i) + i))} is finite V43() set
{{1,(abs ((P1 . i) + i))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
s2 . (DataLoc ((s2 . i),i)) is V11() V12() integer ext-real set
s2 . m is V11() V12() integer ext-real set
DataLoc ((s2 . m),l) is Int-like Element of the carrier of SCMPDS
(s2 . m) + l is V11() V12() integer ext-real set
abs ((s2 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . m) + l))] is V26() set
{1,(abs ((s2 . m) + l))} is finite V43() set
{{1,(abs ((s2 . m) + l))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . m),l)) is V11() V12() integer ext-real set
(s2 . (DataLoc ((s2 . i),i))) + (s2 . (DataLoc ((s2 . m),l))) is V11() V12() integer ext-real set
P1 . (DataLoc ((P1 . i),i)) is V11() V12() integer ext-real set
(P1 . (DataLoc ((P1 . i),i))) + (s2 . (DataLoc ((s2 . m),l))) is V11() V12() integer ext-real set
P1 . m is V11() V12() integer ext-real set
DataLoc ((P1 . m),l) is Int-like Element of the carrier of SCMPDS
(P1 . m) + l is V11() V12() integer ext-real set
abs ((P1 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . m) + l))] is V26() set
{1,(abs ((P1 . m) + l))} is finite V43() set
{{1,(abs ((P1 . m) + l))},{1}} is finite V36() V43() set
P1 . (DataLoc ((P1 . m),l)) is V11() V12() integer ext-real set
(P1 . (DataLoc ((P1 . i),i))) + (P1 . (DataLoc ((P1 . m),l))) is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),i) is Int-like Element of the carrier of SCMPDS
(P1 . i) + i is V11() V12() integer ext-real set
abs ((P1 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + i))] is V26() set
{1,(abs ((P1 . i) + i))} is finite V43() set
{{1,(abs ((P1 . i) + i))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
s2 . c is V11() V12() integer ext-real set
P1 . c is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
i is Int-like Element of the carrier of SCMPDS
m is Int-like Element of the carrier of SCMPDS
i is V11() V12() integer ext-real set
l is V11() V12() integer ext-real set
SubFrom (i,i,m,l) is () Element of the InstructionsF of SCMPDS
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),i) is Int-like Element of the carrier of SCMPDS
(P1 . i) + i is V11() V12() integer ext-real set
abs ((P1 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + i))] is V26() set
{1,(abs ((P1 . i) + i))} is finite V43() set
{{1,(abs ((P1 . i) + i))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
s2 . (DataLoc ((s2 . i),i)) is V11() V12() integer ext-real set
s2 . m is V11() V12() integer ext-real set
DataLoc ((s2 . m),l) is Int-like Element of the carrier of SCMPDS
(s2 . m) + l is V11() V12() integer ext-real set
abs ((s2 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . m) + l))] is V26() set
{1,(abs ((s2 . m) + l))} is finite V43() set
{{1,(abs ((s2 . m) + l))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . m),l)) is V11() V12() integer ext-real set
(s2 . (DataLoc ((s2 . i),i))) - (s2 . (DataLoc ((s2 . m),l))) is V11() V12() integer ext-real set
P1 . (DataLoc ((P1 . i),i)) is V11() V12() integer ext-real set
(P1 . (DataLoc ((P1 . i),i))) - (s2 . (DataLoc ((s2 . m),l))) is V11() V12() integer ext-real set
P1 . m is V11() V12() integer ext-real set
DataLoc ((P1 . m),l) is Int-like Element of the carrier of SCMPDS
(P1 . m) + l is V11() V12() integer ext-real set
abs ((P1 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . m) + l))] is V26() set
{1,(abs ((P1 . m) + l))} is finite V43() set
{{1,(abs ((P1 . m) + l))},{1}} is finite V36() V43() set
P1 . (DataLoc ((P1 . m),l)) is V11() V12() integer ext-real set
(P1 . (DataLoc ((P1 . i),i))) - (P1 . (DataLoc ((P1 . m),l))) is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),i) is Int-like Element of the carrier of SCMPDS
(P1 . i) + i is V11() V12() integer ext-real set
abs ((P1 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + i))] is V26() set
{1,(abs ((P1 . i) + i))} is finite V43() set
{{1,(abs ((P1 . i) + i))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
s2 . c is V11() V12() integer ext-real set
P1 . c is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
i is Int-like Element of the carrier of SCMPDS
m is Int-like Element of the carrier of SCMPDS
i is V11() V12() integer ext-real set
l is V11() V12() integer ext-real set
MultBy (i,i,m,l) is () Element of the InstructionsF of SCMPDS
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),i) is Int-like Element of the carrier of SCMPDS
(P1 . i) + i is V11() V12() integer ext-real set
abs ((P1 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + i))] is V26() set
{1,(abs ((P1 . i) + i))} is finite V43() set
{{1,(abs ((P1 . i) + i))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
s2 . (DataLoc ((s2 . i),i)) is V11() V12() integer ext-real set
s2 . m is V11() V12() integer ext-real set
DataLoc ((s2 . m),l) is Int-like Element of the carrier of SCMPDS
(s2 . m) + l is V11() V12() integer ext-real set
abs ((s2 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . m) + l))] is V26() set
{1,(abs ((s2 . m) + l))} is finite V43() set
{{1,(abs ((s2 . m) + l))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . m),l)) is V11() V12() integer ext-real set
(s2 . (DataLoc ((s2 . i),i))) * (s2 . (DataLoc ((s2 . m),l))) is V11() V12() integer ext-real set
P1 . (DataLoc ((P1 . i),i)) is V11() V12() integer ext-real set
(P1 . (DataLoc ((P1 . i),i))) * (s2 . (DataLoc ((s2 . m),l))) is V11() V12() integer ext-real set
P1 . m is V11() V12() integer ext-real set
DataLoc ((P1 . m),l) is Int-like Element of the carrier of SCMPDS
(P1 . m) + l is V11() V12() integer ext-real set
abs ((P1 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . m) + l))] is V26() set
{1,(abs ((P1 . m) + l))} is finite V43() set
{{1,(abs ((P1 . m) + l))},{1}} is finite V36() V43() set
P1 . (DataLoc ((P1 . m),l)) is V11() V12() integer ext-real set
(P1 . (DataLoc ((P1 . i),i))) * (P1 . (DataLoc ((P1 . m),l))) is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),i) is Int-like Element of the carrier of SCMPDS
(P1 . i) + i is V11() V12() integer ext-real set
abs ((P1 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + i))] is V26() set
{1,(abs ((P1 . i) + i))} is finite V43() set
{{1,(abs ((P1 . i) + i))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
s2 . c is V11() V12() integer ext-real set
P1 . c is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
i is Int-like Element of the carrier of SCMPDS
m is Int-like Element of the carrier of SCMPDS
i is V11() V12() integer ext-real set
l is V11() V12() integer ext-real set
Divide (i,i,m,l) is () Element of the InstructionsF of SCMPDS
s2 . m is V11() V12() integer ext-real set
DataLoc ((s2 . m),l) is Int-like Element of the carrier of SCMPDS
(s2 . m) + l is V11() V12() integer ext-real set
abs ((s2 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . m) + l))] is V26() set
{1,(abs ((s2 . m) + l))} is finite V43() set
{{1,(abs ((s2 . m) + l))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
P1 . m is V11() V12() integer ext-real set
DataLoc ((P1 . m),l) is Int-like Element of the carrier of SCMPDS
(P1 . m) + l is V11() V12() integer ext-real set
abs ((P1 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . m) + l))] is V26() set
{1,(abs ((P1 . m) + l))} is finite V43() set
{{1,(abs ((P1 . m) + l))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . i),i)) is V11() V12() integer ext-real set
s2 . (DataLoc ((s2 . m),l)) is V11() V12() integer ext-real set
(s2 . (DataLoc ((s2 . i),i))) mod (s2 . (DataLoc ((s2 . m),l))) is V11() V12() integer ext-real set
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),i) is Int-like Element of the carrier of SCMPDS
(P1 . i) + i is V11() V12() integer ext-real set
abs ((P1 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + i))] is V26() set
{1,(abs ((P1 . i) + i))} is finite V43() set
{{1,(abs ((P1 . i) + i))},{1}} is finite V36() V43() set
P1 . (DataLoc ((P1 . i),i)) is V11() V12() integer ext-real set
(P1 . (DataLoc ((P1 . i),i))) mod (s2 . (DataLoc ((s2 . m),l))) is V11() V12() integer ext-real set
P1 . (DataLoc ((P1 . m),l)) is V11() V12() integer ext-real set
(P1 . (DataLoc ((P1 . i),i))) mod (P1 . (DataLoc ((P1 . m),l))) is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . m is V11() V12() integer ext-real set
DataLoc ((s2 . m),l) is Int-like Element of the carrier of SCMPDS
(s2 . m) + l is V11() V12() integer ext-real set
abs ((s2 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . m) + l))] is V26() set
{1,(abs ((s2 . m) + l))} is finite V43() set
{{1,(abs ((s2 . m) + l))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
P1 . m is V11() V12() integer ext-real set
DataLoc ((P1 . m),l) is Int-like Element of the carrier of SCMPDS
(P1 . m) + l is V11() V12() integer ext-real set
abs ((P1 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . m) + l))] is V26() set
{1,(abs ((P1 . m) + l))} is finite V43() set
{{1,(abs ((P1 . m) + l))},{1}} is finite V36() V43() set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),i) is Int-like Element of the carrier of SCMPDS
(P1 . i) + i is V11() V12() integer ext-real set
abs ((P1 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + i))] is V26() set
{1,(abs ((P1 . i) + i))} is finite V43() set
{{1,(abs ((P1 . i) + i))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
s2 . c is V11() V12() integer ext-real set
P1 . c is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),i) is Int-like Element of the carrier of SCMPDS
(P1 . i) + i is V11() V12() integer ext-real set
abs ((P1 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + i))] is V26() set
{1,(abs ((P1 . i) + i))} is finite V43() set
{{1,(abs ((P1 . i) + i))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
s2 . (DataLoc ((s2 . i),i)) is V11() V12() integer ext-real set
s2 . (DataLoc ((s2 . m),l)) is V11() V12() integer ext-real set
(s2 . (DataLoc ((s2 . i),i))) div (s2 . (DataLoc ((s2 . m),l))) is V11() V12() integer ext-real set
P1 . (DataLoc ((P1 . i),i)) is V11() V12() integer ext-real set
(P1 . (DataLoc ((P1 . i),i))) div (s2 . (DataLoc ((s2 . m),l))) is V11() V12() integer ext-real set
P1 . (DataLoc ((P1 . m),l)) is V11() V12() integer ext-real set
(P1 . (DataLoc ((P1 . i),i))) div (P1 . (DataLoc ((P1 . m),l))) is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . m is V11() V12() integer ext-real set
DataLoc ((s2 . m),l) is Int-like Element of the carrier of SCMPDS
(s2 . m) + l is V11() V12() integer ext-real set
abs ((s2 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . m) + l))] is V26() set
{1,(abs ((s2 . m) + l))} is finite V43() set
{{1,(abs ((s2 . m) + l))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
i is Int-like Element of the carrier of SCMPDS
m is Int-like Element of the carrier of SCMPDS
i is V11() V12() integer ext-real set
l is V11() V12() integer ext-real set
(i,i) := (m,l) is () Element of the InstructionsF of SCMPDS
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),i) is Int-like Element of the carrier of SCMPDS
(P1 . i) + i is V11() V12() integer ext-real set
abs ((P1 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + i))] is V26() set
{1,(abs ((P1 . i) + i))} is finite V43() set
{{1,(abs ((P1 . i) + i))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
s2 . m is V11() V12() integer ext-real set
DataLoc ((s2 . m),l) is Int-like Element of the carrier of SCMPDS
(s2 . m) + l is V11() V12() integer ext-real set
abs ((s2 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . m) + l))] is V26() set
{1,(abs ((s2 . m) + l))} is finite V43() set
{{1,(abs ((s2 . m) + l))},{1}} is finite V36() V43() set
s2 . (DataLoc ((s2 . m),l)) is V11() V12() integer ext-real set
P1 . m is V11() V12() integer ext-real set
DataLoc ((P1 . m),l) is Int-like Element of the carrier of SCMPDS
(P1 . m) + l is V11() V12() integer ext-real set
abs ((P1 . m) + l) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . m) + l))] is V26() set
{1,(abs ((P1 . m) + l))} is finite V43() set
{{1,(abs ((P1 . m) + l))},{1}} is finite V36() V43() set
P1 . (DataLoc ((P1 . m),l)) is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier of SCMPDS
P1 . i is V11() V12() integer ext-real set
DataLoc ((P1 . i),i) is Int-like Element of the carrier of SCMPDS
(P1 . i) + i is V11() V12() integer ext-real set
abs ((P1 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((P1 . i) + i))] is V26() set
{1,(abs ((P1 . i) + i))} is finite V43() set
{{1,(abs ((P1 . i) + i))},{1}} is finite V36() V43() set
(Exec (I,s2)) . c is V11() V12() integer ext-real set
s2 . c is V11() V12() integer ext-real set
P1 . c is V11() V12() integer ext-real set
(Exec (I,P1)) . c is V11() V12() integer ext-real set
s2 . i is V11() V12() integer ext-real set
DataLoc ((s2 . i),i) is Int-like Element of the carrier of SCMPDS
(s2 . i) + i is V11() V12() integer ext-real set
abs ((s2 . i) + i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
[1,(abs ((s2 . i) + i))] is V26() set
{1,(abs ((s2 . i) + i))} is finite V43() set
{{1,(abs ((s2 . i) + i))},{1}} is finite V36() V43() set
c is Int-like Element of the carrier 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
DataPart s2 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
s2 | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
P1 is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
P2 is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s1 is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 0 -started 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
I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() () () () set
stop I is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() () set
I ^ (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 I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
proj1 I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real 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
n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Shift ((stop I),n) is Relation-like Function-like set
dom (stop I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer finite V43() ext-real non negative Element of K6(NAT)
0 + n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
proj1 (Shift ((stop I),n)) is set
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P1,s1,i)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
(IC (Comput (P1,s1,i))) + n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P2,s2,i) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P2,s2,i)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
DataPart (Comput (P1,s1,i)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Comput (P1,s1,i)) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
DataPart (Comput (P2,s2,i)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Comput (P2,s2,i)) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P1,s1,(i + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P1,s1,(i + 1))) . (IC ) is set
(IC (Comput (P1,s1,(i + 1)))) + n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P2,s2,(i + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,(i + 1))) . (IC ) is set
CurInstr (P1,(Comput (P1,s1,(i + 1)))) is Element of the InstructionsF of SCMPDS
P1 /. (IC (Comput (P1,s1,(i + 1)))) is Element of the InstructionsF of SCMPDS
CurInstr (P2,(Comput (P2,s2,(i + 1)))) is Element of the InstructionsF of SCMPDS
P2 /. (IC (Comput (P2,s2,(i + 1)))) is Element of the InstructionsF of SCMPDS
DataPart (Comput (P1,s1,(i + 1))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Comput (P1,s1,(i + 1))) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
DataPart (Comput (P2,s2,(i + 1))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Comput (P2,s2,(i + 1))) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) 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,(CurInstr (P1,(Comput (P1,s1,i))))) 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,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
l is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
l + n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total 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,(CurInstr (P2,(Comput (P2,s2,i))))) 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,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
P1 . (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
(stop I) . (IC (Comput (P1,s1,i))) is set
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) 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((CurInstr (P1,(Comput (P1,s1,i))))) is set
K90(K90((CurInstr (P1,(Comput (P1,s1,i)))))) is set
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P1 . l is Element of the InstructionsF of SCMPDS
(stop I) . l is set
(Shift ((stop I),n)) . (IC (Comput (P2,s2,(i + 1)))) is set
P2 . (IC (Comput (P2,s2,(i + 1)))) is Element of the InstructionsF of SCMPDS
IC s1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
s1 . (IC ) is set
P1 . (IC s1) is Element of the InstructionsF of SCMPDS
P1 . 0 is Element of the InstructionsF of SCMPDS
(stop I) . 0 is set
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P1,s1,i)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
(IC (Comput (P1,s1,i))) + n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P2,s2,i) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
IC (Comput (P2,s2,i)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
DataPart (Comput (P1,s1,i)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Comput (P1,s1,i)) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
DataPart (Comput (P2,s2,i)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Comput (P2,s2,i)) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
Comput (P1,s1,0) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
DataPart (Comput (P1,s1,0)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Comput (P1,s1,0)) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
Comput (P2,s2,0) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible total set
DataPart (Comput (P2,s2,0)) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible data-only set
(Comput (P2,s2,0)) | (NonZero SCMPDS) is Relation-like the carrier of SCMPDS -defined Function-like the_Values_of SCMPDS -compatible set
IC (Comput (P1,s1,0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P1,s1,0)) . (IC ) is set
P2 /. (IC s2) is Element of the InstructionsF of SCMPDS
P2 . (IC s2) is Element of the InstructionsF of SCMPDS
P1 /. (IC s1) is Element of the InstructionsF of SCMPDS
CurInstr (P1,(Comput (P1,s1,0))) is Element of the InstructionsF of SCMPDS
P1 /. (IC (Comput (P1,s1,0))) is Element of the InstructionsF of SCMPDS
(Shift ((stop I),n)) . (0 + n) is set
CurInstr (P2,(Comput (P2,s2,0))) is Element of the InstructionsF of SCMPDS
IC (Comput (P2,s2,0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P2,s2,0)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,0))) is Element of the InstructionsF of SCMPDS
(IC (Comput (P1,s1,0))) + n is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT