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
F2() 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
F1(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
F1(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
F1(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
F1(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
F1(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