REAL is set
NAT is non empty V5() V17() V18() V19() non finite V43() V44() Element of K32(REAL)
K32(REAL) is set
COMPLEX is set
NAT is non empty V5() V17() V18() V19() non finite V43() V44() set
K32(NAT) is set
9 is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real positive Element of NAT
K161(9) is V43() Element of K32(NAT)
K176() is set
SCM-Memory is set
{NAT} is non empty finite V43() set
{NAT} \/ K176() is non empty set
K32(SCM-Memory) is set
2 is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real positive Element of NAT
K33(SCM-Memory,2) is Relation-like set
K32(K33(SCM-Memory,2)) is set
SCM-OK is Relation-like Function-like V29( SCM-Memory ,2) Element of K32(K33(SCM-Memory,2))
SCM-VAL is Relation-like 2 -defined Function-like total set
INT is set
K289(NAT,INT) is set
SCM-OK * SCM-VAL is Relation-like Function-like set
K165((SCM-OK * SCM-VAL)) is functional V41() V42() set
K177() is non empty set
K145(K165((SCM-OK * SCM-VAL)),K165((SCM-OK * SCM-VAL))) is set
K33(K177(),K145(K165((SCM-OK * SCM-VAL)),K165((SCM-OK * SCM-VAL)))) is Relation-like set
K32(K33(K177(),K145(K165((SCM-OK * SCM-VAL)),K165((SCM-OK * SCM-VAL))))) is set
K32(NAT) is set
K176() \/ INT is set
SCM-Data-Loc is Element of K32(SCM-Memory)
SCM-Data-Loc \/ INT is set
K210() is set
K33(K210(),K145(K165((SCM-OK * SCM-VAL)),K165((SCM-OK * SCM-VAL)))) is Relation-like set
K32(K33(K210(),K145(K165((SCM-OK * SCM-VAL)),K165((SCM-OK * SCM-VAL))))) is set
SCMPDS is non empty V83(2) IC-Ins-separated strict strict V91(2) AMI-Struct over 2
K519(NAT,SCM-Memory) is Element of SCM-Memory
K230() is Relation-like Function-like V29(K210(),K145(K165((SCM-OK * SCM-VAL)),K165((SCM-OK * SCM-VAL)))) Element of K32(K33(K210(),K145(K165((SCM-OK * SCM-VAL)),K165((SCM-OK * SCM-VAL)))))
AMI-Struct(# SCM-Memory,K519(NAT,SCM-Memory),K210(),SCM-OK,SCM-VAL,K230() #) is strict AMI-Struct over 2
the carrier of SCMPDS is set
the InstructionsF of SCMPDS is non empty Relation-like V72() V73() V74() V76() set
RAT is set
K507() is non empty V83(2) IC-Ins-separated strict strict V91(2) AMI-Struct over 2
the InstructionsF of K507() is non empty Relation-like V72() V73() V74() V76() set
the carrier of K507() is set
K318(2,K507()) is Relation-like non-empty the carrier of K507() -defined Function-like total set
the Object-Kind of K507() is Relation-like Function-like V29( the carrier of K507(),2) Element of K32(K33( the carrier of K507(),2))
K33( the carrier of K507(),2) is Relation-like set
K32(K33( the carrier of K507(),2)) is set
the U7 of K507() is Relation-like 2 -defined Function-like total set
the Object-Kind of K507() * the U7 of K507() is Relation-like Function-like set
1 is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real positive Element of NAT
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() V25() integer finite finite-yielding V36() V40() V43() ext-real Function-yielding V136() set
0 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() V25() integer finite finite-yielding V36() V40() V43() ext-real Function-yielding V136() Element of NAT
IC is Element of the carrier of SCMPDS
K318(2,SCMPDS) is Relation-like non-empty the carrier of SCMPDS -defined Function-like total set
the Object-Kind of SCMPDS is Relation-like Function-like V29( the carrier of SCMPDS,2) Element of K32(K33( the carrier of SCMPDS,2))
K33( the carrier of SCMPDS,2) is Relation-like set
K32(K33( the carrier of SCMPDS,2)) is set
the U7 of SCMPDS is Relation-like 2 -defined Function-like total set
the Object-Kind of SCMPDS * the U7 of SCMPDS is Relation-like Function-like set
NonZero SCMPDS is Element of K32( the carrier of SCMPDS)
K32( the carrier of SCMPDS) is set
P1 is V24() V25() integer ext-real set
P2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
IC P2 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P2 . (IC ) is set
q is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
IC q is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
q . (IC ) is set
ICplusConst (P2,P1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst (q,P1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
p is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
p + P1 is V24() V25() integer ext-real set
abs (p + P1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P1 is V24() V25() integer ext-real set
P2 is Int-like Element of the carrier of SCMPDS
q is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
DataPart q is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible data-only set
q | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible set
p is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
DataPart p is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible data-only set
p | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible set
q . P2 is V24() V25() integer ext-real set
DataLoc ((q . P2),P1) is Int-like Element of the carrier of SCMPDS
(q . P2) + P1 is V24() V25() integer ext-real set
abs ((q . P2) + P1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs ((q . P2) + P1))] is set
q . (DataLoc ((q . P2),P1)) is V24() V25() integer ext-real set
p . P2 is V24() V25() integer ext-real set
DataLoc ((p . P2),P1) is Int-like Element of the carrier of SCMPDS
(p . P2) + P1 is V24() V25() integer ext-real set
abs ((p . P2) + P1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs ((p . P2) + P1))] is set
p . (DataLoc ((p . P2),P1)) is V24() V25() integer ext-real set
(DataPart q) . P2 is set
(DataPart q) . (DataLoc ((q . P2),P1)) is set
P1 is Int-like Element of the carrier of SCMPDS
P2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
DataPart P2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible data-only set
P2 | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible set
q is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
DataPart q is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible data-only set
q | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible set
P2 . P1 is V24() V25() integer ext-real set
q . P1 is V24() V25() integer ext-real set
(DataPart P2) . P1 is set
Values (IC ) is non empty set
K318(2,SCMPDS) . (IC ) is set
P1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
P2 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Start-At (P2,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() P2 -started set
(IC ) .--> P2 is V5() Relation-like {(IC )} -defined NAT -valued Function-like one-to-one constant finite V43() set
{(IC )} is non empty finite V43() set
{(IC )} --> P2 is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant total V29({(IC )},{P2}) finite V43() Element of K32(K33({(IC )},{P2}))
{P2} is non empty finite V43() set
K33({(IC )},{P2}) is Relation-like finite V43() set
K32(K33({(IC )},{P2})) is finite V36() V43() set
P1 +* (Start-At (P2,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible K318(2,SCMPDS) -compatible total P2 -started set
q is Int-like Element of the carrier of SCMPDS
P1 . q is V24() V25() integer ext-real set
(P1 +* (Start-At (P2,SCMPDS))) . q is V24() V25() integer ext-real set
dom P1 is set
dom (Start-At (P2,SCMPDS)) is non empty finite V43() set
(dom P1) \/ (dom (Start-At (P2,SCMPDS))) is non empty set
P1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
P2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
P2 | SCM-Data-Loc is Relation-like SCM-Data-Loc -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible set
P1 +* (P2 | SCM-Data-Loc) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible set
P1 is Int-like Element of the carrier of SCMPDS
P2 is V24() V25() integer ext-real set
P1 .--> P2 is V5() Relation-like {P1} -defined Function-like one-to-one constant finite V43() set
{P1} is non empty finite V43() set
{P1} --> P2 is non empty Relation-like {P1} -defined Function-like constant total V29({P1},{P2}) finite V43() Element of K32(K33({P1},{P2}))
{P2} is non empty finite V43() set
K33({P1},{P2}) is Relation-like finite V43() set
K32(K33({P1},{P2})) is finite V36() V43() set
Values P1 is non empty set
K318(2,SCMPDS) . P1 is set
P1 is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() non halt-free set
P2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() P1 -autonomic set
dom P2 is finite V43() set
{(IC )} is non empty finite V43() set
DataPart P2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() data-only set
P2 | (NonZero SCMPDS) is Relation-like NonZero SCMPDS -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
dom (DataPart P2) is finite V43() set
{(IC )} \/ (dom (DataPart P2)) is non empty finite V43() set
dom P1 is finite V43() set
NAT \ (dom P1) is Element of K32(REAL)
the Element of NAT \ (dom P1) is Element of NAT \ (dom P1)
the Element of dom (DataPart P2) is Element of dom (DataPart P2)
s2 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
s1 is Element of the carrier of SCMPDS
Start-At (s2,SCMPDS) is non empty Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() s2 -started set
(IC ) .--> s2 is V5() Relation-like {(IC )} -defined NAT -valued Function-like one-to-one constant finite V43() set
{(IC )} --> s2 is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant total V29({(IC )},{s2}) finite V43() Element of K32(K33({(IC )},{s2}))
{s2} is non empty finite V43() set
K33({(IC )},{s2}) is Relation-like finite V43() set
K32(K33({(IC )},{s2})) is finite V36() V43() set
dom (Start-At (s2,SCMPDS)) is non empty finite V43() set
P2 +* (Start-At (s2,SCMPDS)) is non empty Relation-like the carrier of SCMPDS -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible K318(2,SCMPDS) -compatible finite V43() s2 -started set
i is Int-like Element of the carrier of SCMPDS
i := 1 is Element of the InstructionsF of SCMPDS
K201(i,1) is set
K15(2,{},K201(i,1)) is set
s2 .--> (i := 1) is V5() Relation-like NAT -defined {s2} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant finite V43() set
{s2} --> (i := 1) is non empty Relation-like {s2} -defined the InstructionsF of SCMPDS -valued Function-like constant total V29({s2},{(i := 1)}) finite V43() Element of K32(K33({s2},{(i := 1)}))
{(i := 1)} is non empty finite V43() set
K33({s2},{(i := 1)}) is Relation-like finite V43() set
K32(K33({s2},{(i := 1)})) is finite V36() V43() set
P1 +* (s2 .--> (i := 1)) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() set
i := 0 is Element of the InstructionsF of SCMPDS
K201(i,0) is set
K15(2,{},K201(i,0)) is set
s2 .--> (i := 0) is V5() Relation-like NAT -defined {s2} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant finite V43() set
{s2} --> (i := 0) is non empty Relation-like {s2} -defined the InstructionsF of SCMPDS -valued Function-like constant total V29({s2},{(i := 0)}) finite V43() Element of K32(K33({s2},{(i := 0)}))
{(i := 0)} is non empty finite V43() set
K33({s2},{(i := 0)}) is Relation-like finite V43() set
K32(K33({s2},{(i := 0)})) is finite V36() V43() set
P1 +* (s2 .--> (i := 0)) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() set
dom (s2 .--> (i := 1)) is V5() finite V43() set
dom (s2 .--> (i := 0)) is V5() finite V43() set
Cs1i is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Cs2i is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Cs1i1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Cs2i1 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
D11 is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
(dom P2) /\ (dom (Start-At (s2,SCMPDS))) is finite V43() set
(dom P2) /\ {(IC )} is finite V43() set
Comput (I,Cs1i,1) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
(Comput (I,Cs1i,1)) | (dom P2) is Relation-like dom P2 -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
Comput (D11,Cs1i1,1) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
(Comput (D11,Cs1i1,1)) | (dom P2) is Relation-like dom P2 -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
dom (P2 +* (Start-At (s2,SCMPDS))) is non empty finite V43() set
(dom P2) \/ (dom (Start-At (s2,SCMPDS))) is non empty finite V43() set
dom (P1 +* (s2 .--> (i := 1))) is finite V43() set
(dom P1) \/ (dom (s2 .--> (i := 1))) is finite V43() set
IC Cs1i1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Cs1i1 . (IC ) is set
(P2 +* (Start-At (s2,SCMPDS))) . (IC ) is set
(Start-At (s2,SCMPDS)) . (IC ) is set
Cs2i1 . s2 is Element of the InstructionsF of SCMPDS
(P1 +* (s2 .--> (i := 1))) . s2 is set
(s2 .--> (i := 1)) . s2 is set
Cs2i1 /. (IC Cs1i1) is Element of the InstructionsF of SCMPDS
Cs2i1 . (IC Cs1i1) is Element of the InstructionsF of SCMPDS
0 + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (Cs2i1,Cs1i1,(0 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
(Comput (Cs2i1,Cs1i1,(0 + 1))) . i is V24() V25() integer ext-real set
Comput (Cs2i1,Cs1i1,0) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Following (Cs2i1,(Comput (Cs2i1,Cs1i1,0))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (Cs2i1,(Comput (Cs2i1,Cs1i1,0))) is Element of the InstructionsF of SCMPDS
IC (Comput (Cs2i1,Cs1i1,0)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (Cs2i1,Cs1i1,0)) . (IC ) is set
Cs2i1 /. (IC (Comput (Cs2i1,Cs1i1,0))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (Cs2i1,(Comput (Cs2i1,Cs1i1,0)))),(Comput (Cs2i1,Cs1i1,0))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)) is functional V41() V42() set
K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))))) is set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs2i1,(Comput (Cs2i1,Cs1i1,0))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs2i1,(Comput (Cs2i1,Cs1i1,0))))) . (Comput (Cs2i1,Cs1i1,0)) is set
(Following (Cs2i1,(Comput (Cs2i1,Cs1i1,0)))) . i is V24() V25() integer ext-real set
Following (Cs2i1,Cs1i1) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (Cs2i1,Cs1i1) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (Cs2i1,Cs1i1)),Cs1i1) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs2i1,Cs1i1))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs2i1,Cs1i1))) . Cs1i1 is set
(Following (Cs2i1,Cs1i1)) . i is V24() V25() integer ext-real set
Comput (Cs2i,Cs1i,1) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
dom (Comput (Cs2i,Cs1i,1)) is set
(Comput (Cs2i,Cs1i,1)) | (dom P2) is Relation-like dom P2 -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
dom ((Comput (Cs2i,Cs1i,1)) | (dom P2)) is finite V43() set
dom (P1 +* (s2 .--> (i := 0))) is finite V43() set
(dom P1) \/ (dom (s2 .--> (i := 0))) is finite V43() set
IC Cs1i is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Cs1i . (IC ) is set
Cs2i . s2 is Element of the InstructionsF of SCMPDS
(P1 +* (s2 .--> (i := 0))) . s2 is set
(s2 .--> (i := 0)) . s2 is set
Cs2i /. (IC Cs1i) is Element of the InstructionsF of SCMPDS
Cs2i . (IC Cs1i) is Element of the InstructionsF of SCMPDS
Comput (Cs2i1,Cs1i1,1) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
dom (Comput (Cs2i1,Cs1i1,1)) is set
(Comput (Cs2i1,Cs1i1,1)) | (dom P2) is Relation-like dom P2 -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
dom ((Comput (Cs2i1,Cs1i1,1)) | (dom P2)) is finite V43() set
Comput (Cs2i,Cs1i,(0 + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
(Comput (Cs2i,Cs1i,(0 + 1))) . i is V24() V25() integer ext-real set
Comput (Cs2i,Cs1i,0) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Following (Cs2i,(Comput (Cs2i,Cs1i,0))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (Cs2i,(Comput (Cs2i,Cs1i,0))) is Element of the InstructionsF of SCMPDS
IC (Comput (Cs2i,Cs1i,0)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (Cs2i,Cs1i,0)) . (IC ) is set
Cs2i /. (IC (Comput (Cs2i,Cs1i,0))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (Cs2i,(Comput (Cs2i,Cs1i,0)))),(Comput (Cs2i,Cs1i,0))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs2i,(Comput (Cs2i,Cs1i,0))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs2i,(Comput (Cs2i,Cs1i,0))))) . (Comput (Cs2i,Cs1i,0)) is set
(Following (Cs2i,(Comput (Cs2i,Cs1i,0)))) . i is V24() V25() integer ext-real set
Following (Cs2i,Cs1i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (Cs2i,Cs1i) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (Cs2i,Cs1i)),Cs1i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs2i,Cs1i))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs2i,Cs1i))) . Cs1i is set
(Following (Cs2i,Cs1i)) . i is V24() V25() integer ext-real set
((Comput (Cs2i,Cs1i,1)) | (dom P2)) . i is set
P1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
IC P1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P1 . (IC ) is set
P2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
IC P2 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P2 . (IC ) is set
q is V24() V25() integer ext-real set
p is V24() V25() integer ext-real set
s1 is V24() V25() integer ext-real set
s1 + q is V24() V25() integer ext-real set
s1 + p is V24() V25() integer ext-real set
ICplusConst (P1,q) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst (P2,p) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
s2 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
s2 + q is V24() V25() integer ext-real set
abs (s2 + q) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
s2 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
s2 + p is V24() V25() integer ext-real set
abs (s2 + p) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
IC P1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P1 . (IC ) is set
P2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
IC P2 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P2 . (IC ) is set
q is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
p is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst (P1,q) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst (P2,p) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
s1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
s1 + 2 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(s1 + 2) - 2 is V24() V25() integer ext-real set
((s1 + 2) - 2) + q is V24() V25() integer ext-real set
s1 + q is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
((s1 + 2) - 2) + p is V24() V25() integer ext-real set
s1 + p is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
IC P1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P1 . (IC ) is set
succ (IC P1) is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real set
(IC P1) + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst (P1,1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P2 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P2 + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
abs (P2 + 1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P2 * 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
q is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
abs q is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(abs q) + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
abs 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(abs q) + (abs 1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
q + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
abs (q + 1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
P1 is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() non halt-free set
dom P1 is finite V43() set
P2 is non empty Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() P1 -autonomic set
q is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
p is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
s1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (p,q,s1) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
IC (Comput (p,q,s1)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (p,q,s1)) . (IC ) is set
(IC (Comput (p,q,s1))) + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
the Int-like Element of the carrier of SCMPDS is Int-like Element of the carrier of SCMPDS
the Int-like Element of the carrier of SCMPDS := 0 is Element of the InstructionsF of SCMPDS
K201( the Int-like Element of the carrier of SCMPDS,0) is set
K15(2,{},K201( the Int-like Element of the carrier of SCMPDS,0)) is set
(IC (Comput (p,q,s1))) .--> ( the Int-like Element of the carrier of SCMPDS := 0) is V5() Relation-like NAT -defined {(IC (Comput (p,q,s1)))} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant finite V43() set
{(IC (Comput (p,q,s1)))} is non empty finite V43() set
{(IC (Comput (p,q,s1)))} --> ( the Int-like Element of the carrier of SCMPDS := 0) is non empty Relation-like {(IC (Comput (p,q,s1)))} -defined the InstructionsF of SCMPDS -valued Function-like constant total V29({(IC (Comput (p,q,s1)))},{( the Int-like Element of the carrier of SCMPDS := 0)}) finite V43() Element of K32(K33({(IC (Comput (p,q,s1)))},{( the Int-like Element of the carrier of SCMPDS := 0)}))
{( the Int-like Element of the carrier of SCMPDS := 0)} is non empty finite V43() set
K33({(IC (Comput (p,q,s1)))},{( the Int-like Element of the carrier of SCMPDS := 0)}) is Relation-like finite V43() set
K32(K33({(IC (Comput (p,q,s1)))},{( the Int-like Element of the carrier of SCMPDS := 0)})) is finite V36() V43() set
P1 +* ((IC (Comput (p,q,s1))) .--> ( the Int-like Element of the carrier of SCMPDS := 0)) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() set
halt SCMPDS is V90(2, SCMPDS ) Element of the InstructionsF of SCMPDS
(IC (Comput (p,q,s1))) .--> (halt SCMPDS) is V5() Relation-like NAT -defined {(IC (Comput (p,q,s1)))} -defined the InstructionsF of SCMPDS -valued Function-like one-to-one constant finite V43() set
{(IC (Comput (p,q,s1)))} --> (halt SCMPDS) is non empty Relation-like {(IC (Comput (p,q,s1)))} -defined the InstructionsF of SCMPDS -valued Function-like constant total V29({(IC (Comput (p,q,s1)))},{(halt SCMPDS)}) finite V43() Element of K32(K33({(IC (Comput (p,q,s1)))},{(halt SCMPDS)}))
{(halt SCMPDS)} is non empty finite V43() set
K33({(IC (Comput (p,q,s1)))},{(halt SCMPDS)}) is Relation-like finite V43() set
K32(K33({(IC (Comput (p,q,s1)))},{(halt SCMPDS)})) is finite V36() V43() set
P1 +* ((IC (Comput (p,q,s1))) .--> (halt SCMPDS)) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() set
p +* ((IC (Comput (p,q,s1))) .--> ( the Int-like Element of the carrier of SCMPDS := 0)) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
p +* ((IC (Comput (p,q,s1))) .--> (halt SCMPDS)) is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
dom ((IC (Comput (p,q,s1))) .--> (halt SCMPDS)) is V5() finite V43() set
dom ((IC (Comput (p,q,s1))) .--> ( the Int-like Element of the carrier of SCMPDS := 0)) is V5() finite V43() set
Cs1i is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Cs2i is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like total set
Comput (Cs2i,q,s1) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Comput (Cs1i,q,s1) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
((IC (Comput (p,q,s1))) .--> (halt SCMPDS)) . (IC (Comput (p,q,s1))) is set
Cs2i . (IC (Comput (p,q,s1))) is Element of the InstructionsF of SCMPDS
((IC (Comput (p,q,s1))) .--> ( the Int-like Element of the carrier of SCMPDS := 0)) . (IC (Comput (p,q,s1))) is set
Cs1i . (IC (Comput (p,q,s1))) is Element of the InstructionsF of SCMPDS
dom P2 is non empty finite V43() set
(Comput (Cs1i,q,s1)) | (dom P2) is Relation-like dom P2 -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
(Comput (p,q,s1)) | (dom P2) is Relation-like dom P2 -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
(Comput (Cs2i,q,s1)) | (dom P2) is Relation-like dom P2 -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
s1 + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
I is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (Cs1i,q,I) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
(Comput (Cs1i,q,I)) | (dom P2) is Relation-like dom P2 -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
Comput (Cs2i,q,I) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
(Comput (Cs2i,q,I)) | (dom P2) is Relation-like dom P2 -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
IC ((Comput (p,q,s1)) | (dom P2)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
((Comput (p,q,s1)) | (dom P2)) . (IC ) is set
IC (Comput (Cs1i,q,s1)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (Cs1i,q,s1)) . (IC ) is set
CurInstr (Cs1i,(Comput (Cs1i,q,s1))) is Element of the InstructionsF of SCMPDS
Cs1i /. (IC (Comput (Cs1i,q,s1))) is Element of the InstructionsF of SCMPDS
Following (Cs1i,(Comput (Cs1i,q,s1))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Exec ((CurInstr (Cs1i,(Comput (Cs1i,q,s1)))),(Comput (Cs1i,q,s1))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)) is functional V41() V42() set
K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))))) is set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs1i,(Comput (Cs1i,q,s1))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs1i,(Comput (Cs1i,q,s1))))) . (Comput (Cs1i,q,s1)) is set
Exec (( the Int-like Element of the carrier of SCMPDS := 0),(Comput (Cs1i,q,s1))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,( the Int-like Element of the carrier of SCMPDS := 0)) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,( the Int-like Element of the carrier of SCMPDS := 0)) . (Comput (Cs1i,q,s1)) is set
IC (Exec (( the Int-like Element of the carrier of SCMPDS := 0),(Comput (Cs1i,q,s1)))) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Exec (( the Int-like Element of the carrier of SCMPDS := 0),(Comput (Cs1i,q,s1)))) . (IC ) is set
succ (IC (Comput (Cs1i,q,s1))) is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real set
(IC (Comput (Cs1i,q,s1))) + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
IC (Comput (Cs1i,q,I)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (Cs1i,q,I)) . (IC ) is set
succ (IC (Comput (p,q,s1))) is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real set
(IC (Comput (p,q,s1))) + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Following (Cs2i,(Comput (Cs2i,q,s1))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (Cs2i,(Comput (Cs2i,q,s1))) is Element of the InstructionsF of SCMPDS
IC (Comput (Cs2i,q,s1)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (Cs2i,q,s1)) . (IC ) is set
Cs2i /. (IC (Comput (Cs2i,q,s1))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (Cs2i,(Comput (Cs2i,q,s1)))),(Comput (Cs2i,q,s1))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs2i,(Comput (Cs2i,q,s1))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (Cs2i,(Comput (Cs2i,q,s1))))) . (Comput (Cs2i,q,s1)) is set
Cs2i . (IC (Comput (Cs2i,q,s1))) is Element of the InstructionsF of SCMPDS
IC (Comput (Cs2i,q,I)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (Cs2i,q,I)) . (IC ) is set
IC ((Comput (Cs1i,q,I)) | (dom P2)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
((Comput (Cs1i,q,I)) | (dom P2)) . (IC ) is set
IC ((Comput (Cs2i,q,I)) | (dom P2)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
((Comput (Cs2i,q,I)) | (dom P2)) . (IC ) is 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
q is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() non halt-free set
p is non empty Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() q -autonomic set
dom p is non empty finite V43() set
s1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
s2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
i is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
Comput (P2,s2,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
m is V24() V25() integer ext-real set
a is V24() V25() integer ext-real set
k1 is Int-like Element of the carrier of SCMPDS
k2 is Int-like Element of the carrier of SCMPDS
(k1,m) := (k2,a) is Element of the InstructionsF of SCMPDS
(Comput (P1,s1,i)) . k1 is V24() V25() integer ext-real set
DataLoc (((Comput (P1,s1,i)) . k1),m) is Int-like Element of the carrier of SCMPDS
((Comput (P1,s1,i)) . k1) + m is V24() V25() integer ext-real set
abs (((Comput (P1,s1,i)) . k1) + m) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P1,s1,i)) . k1) + m))] is set
(Comput (P1,s1,i)) . k2 is V24() V25() integer ext-real set
DataLoc (((Comput (P1,s1,i)) . k2),a) is Int-like Element of the carrier of SCMPDS
((Comput (P1,s1,i)) . k2) + a is V24() V25() integer ext-real set
abs (((Comput (P1,s1,i)) . k2) + a) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P1,s1,i)) . k2) + a))] is set
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k2),a)) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . k2 is V24() V25() integer ext-real set
DataLoc (((Comput (P2,s2,i)) . k2),a) is Int-like Element of the carrier of SCMPDS
((Comput (P2,s2,i)) . k2) + a is V24() V25() integer ext-real set
abs (((Comput (P2,s2,i)) . k2) + a) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P2,s2,i)) . k2) + a))] is set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k2),a)) is V24() V25() integer ext-real set
(Comput (P1,s1,i)) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P1,s1,i)) | (dom p)) . k1 is set
(Comput (P2,s2,i)) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P2,s2,i)) | (dom p)) . k1 is set
(Comput (P2,s2,i)) . k1 is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,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 K318(2,SCMPDS) -compatible total set
K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)) is functional V41() V42() set
K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))))) is set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
(Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P1,s1,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P2,s2,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
(Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
DataLoc (((Comput (P2,s2,i)) . k1),m) is Int-like Element of the carrier of SCMPDS
((Comput (P2,s2,i)) . k1) + m is V24() V25() integer ext-real set
abs (((Comput (P2,s2,i)) . k1) + m) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P2,s2,i)) . k1) + m))] is set
(Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . k1),m)) is V24() V25() integer ext-real 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
q is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() non halt-free set
p is non empty Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() q -autonomic set
dom p is non empty finite V43() set
s1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
s2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
i is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
Comput (P2,s2,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
m is V24() V25() integer ext-real set
a is V24() V25() integer ext-real set
k1 is Int-like Element of the carrier of SCMPDS
k2 is Int-like Element of the carrier of SCMPDS
AddTo (k1,m,k2,a) is Element of the InstructionsF of SCMPDS
(Comput (P1,s1,i)) . k1 is V24() V25() integer ext-real set
DataLoc (((Comput (P1,s1,i)) . k1),m) is Int-like Element of the carrier of SCMPDS
((Comput (P1,s1,i)) . k1) + m is V24() V25() integer ext-real set
abs (((Comput (P1,s1,i)) . k1) + m) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P1,s1,i)) . k1) + m))] is set
(Comput (P1,s1,i)) . k2 is V24() V25() integer ext-real set
DataLoc (((Comput (P1,s1,i)) . k2),a) is Int-like Element of the carrier of SCMPDS
((Comput (P1,s1,i)) . k2) + a is V24() V25() integer ext-real set
abs (((Comput (P1,s1,i)) . k2) + a) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P1,s1,i)) . k2) + a))] is set
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k2),a)) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . k2 is V24() V25() integer ext-real set
DataLoc (((Comput (P2,s2,i)) . k2),a) is Int-like Element of the carrier of SCMPDS
((Comput (P2,s2,i)) . k2) + a is V24() V25() integer ext-real set
abs (((Comput (P2,s2,i)) . k2) + a) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P2,s2,i)) . k2) + a))] is set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k2),a)) is V24() V25() integer ext-real set
(Comput (P1,s1,i)) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P1,s1,i)) | (dom p)) . k1 is set
(Comput (P2,s2,i)) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P2,s2,i)) | (dom p)) . k1 is set
(Comput (P2,s2,i)) . k1 is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
(Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
DataLoc (((Comput (P2,s2,i)) . k1),m) is Int-like Element of the carrier of SCMPDS
((Comput (P2,s2,i)) . k1) + m is V24() V25() integer ext-real set
abs (((Comput (P2,s2,i)) . k1) + m) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P2,s2,i)) . k1) + m))] is set
(Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . k1),m)) is V24() V25() integer ext-real set
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k1),m)) is V24() V25() integer ext-real set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)) is functional V41() V42() set
K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))))) is set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P1,s1,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P2,s2,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
(Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,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 K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k1),m))) + ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k2),a))) is V24() V25() integer ext-real set
((Comput (P1,s1,i)) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
((Comput (P2,s2,i)) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k1),m))) + ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k2),a))) is V24() V25() integer ext-real 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
q is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() non halt-free set
p is non empty Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() q -autonomic set
dom p is non empty finite V43() set
s1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
s2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
i is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
Comput (P2,s2,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
m is V24() V25() integer ext-real set
a is V24() V25() integer ext-real set
k1 is Int-like Element of the carrier of SCMPDS
k2 is Int-like Element of the carrier of SCMPDS
SubFrom (k1,m,k2,a) is Element of the InstructionsF of SCMPDS
(Comput (P1,s1,i)) . k1 is V24() V25() integer ext-real set
DataLoc (((Comput (P1,s1,i)) . k1),m) is Int-like Element of the carrier of SCMPDS
((Comput (P1,s1,i)) . k1) + m is V24() V25() integer ext-real set
abs (((Comput (P1,s1,i)) . k1) + m) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P1,s1,i)) . k1) + m))] is set
(Comput (P1,s1,i)) . k2 is V24() V25() integer ext-real set
DataLoc (((Comput (P1,s1,i)) . k2),a) is Int-like Element of the carrier of SCMPDS
((Comput (P1,s1,i)) . k2) + a is V24() V25() integer ext-real set
abs (((Comput (P1,s1,i)) . k2) + a) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P1,s1,i)) . k2) + a))] is set
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k2),a)) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . k2 is V24() V25() integer ext-real set
DataLoc (((Comput (P2,s2,i)) . k2),a) is Int-like Element of the carrier of SCMPDS
((Comput (P2,s2,i)) . k2) + a is V24() V25() integer ext-real set
abs (((Comput (P2,s2,i)) . k2) + a) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P2,s2,i)) . k2) + a))] is set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k2),a)) is V24() V25() integer ext-real set
(Comput (P1,s1,i)) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P1,s1,i)) | (dom p)) . k1 is set
(Comput (P2,s2,i)) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P2,s2,i)) | (dom p)) . k1 is set
(Comput (P2,s2,i)) . k1 is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
(Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
DataLoc (((Comput (P2,s2,i)) . k1),m) is Int-like Element of the carrier of SCMPDS
((Comput (P2,s2,i)) . k1) + m is V24() V25() integer ext-real set
abs (((Comput (P2,s2,i)) . k1) + m) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P2,s2,i)) . k1) + m))] is set
(Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . k1),m)) is V24() V25() integer ext-real set
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k1),m)) is V24() V25() integer ext-real set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)) is functional V41() V42() set
K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))))) is set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P1,s1,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P2,s2,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
(Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,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 K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k1),m))) - ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k2),a))) is V24() V25() integer ext-real set
((Comput (P1,s1,i)) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
((Comput (P2,s2,i)) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k1),m))) - ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k2),a))) is V24() V25() integer ext-real 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
q is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() non halt-free set
p is non empty Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() q -autonomic set
dom p is non empty finite V43() set
s1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
s2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
i is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
Comput (P2,s2,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
m is V24() V25() integer ext-real set
a is V24() V25() integer ext-real set
k1 is Int-like Element of the carrier of SCMPDS
k2 is Int-like Element of the carrier of SCMPDS
MultBy (k1,m,k2,a) is Element of the InstructionsF of SCMPDS
(Comput (P1,s1,i)) . k1 is V24() V25() integer ext-real set
DataLoc (((Comput (P1,s1,i)) . k1),m) is Int-like Element of the carrier of SCMPDS
((Comput (P1,s1,i)) . k1) + m is V24() V25() integer ext-real set
abs (((Comput (P1,s1,i)) . k1) + m) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P1,s1,i)) . k1) + m))] is set
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
(Comput (P1,s1,i)) . k2 is V24() V25() integer ext-real set
DataLoc (((Comput (P1,s1,i)) . k2),a) is Int-like Element of the carrier of SCMPDS
((Comput (P1,s1,i)) . k2) + a is V24() V25() integer ext-real set
abs (((Comput (P1,s1,i)) . k2) + a) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P1,s1,i)) . k2) + a))] is set
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k2),a)) is V24() V25() integer ext-real set
((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k1),m))) * ((Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . k2),a))) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . k1 is V24() V25() integer ext-real set
DataLoc (((Comput (P2,s2,i)) . k1),m) is Int-like Element of the carrier of SCMPDS
((Comput (P2,s2,i)) . k1) + m is V24() V25() integer ext-real set
abs (((Comput (P2,s2,i)) . k1) + m) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P2,s2,i)) . k1) + m))] is set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k1),m)) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . k2 is V24() V25() integer ext-real set
DataLoc (((Comput (P2,s2,i)) . k2),a) is Int-like Element of the carrier of SCMPDS
((Comput (P2,s2,i)) . k2) + a is V24() V25() integer ext-real set
abs (((Comput (P2,s2,i)) . k2) + a) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P2,s2,i)) . k2) + a))] is set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k2),a)) is V24() V25() integer ext-real set
((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k1),m))) * ((Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . k2),a))) is V24() V25() integer ext-real set
(Comput (P1,s1,i)) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P1,s1,i)) | (dom p)) . k1 is set
(Comput (P2,s2,i)) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P2,s2,i)) | (dom p)) . k1 is set
i + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
(Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real set
(Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . k1),m)) is V24() V25() integer ext-real set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,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 K318(2,SCMPDS) -compatible total set
K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)) is functional V41() V42() set
K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))))) is set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCMPDS
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P1,s1,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
((Comput (P2,s2,(i + 1))) | (dom p)) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is set
(Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . k1),m)) is V24() V25() integer ext-real 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
q is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() non halt-free set
p is non empty Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() q -autonomic set
s1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
s2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
i is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
m is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P2,s2,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
a is Int-like Element of the carrier of SCMPDS
(Comput (P1,s1,i)) . a is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . a is V24() V25() integer ext-real set
k1 is V24() V25() integer ext-real set
k2 is V24() V25() integer ext-real set
(a,k1) <>0_goto k2 is Element of the InstructionsF of SCMPDS
4 is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real positive Element of NAT
K202(a,k1,k2) is set
K15(4,{},K202(a,k1,k2)) is set
m + k2 is V24() V25() integer ext-real set
DataLoc (((Comput (P1,s1,i)) . a),k1) is Int-like Element of the carrier of SCMPDS
((Comput (P1,s1,i)) . a) + k1 is V24() V25() integer ext-real set
abs (((Comput (P1,s1,i)) . a) + k1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P1,s1,i)) . a) + k1))] is set
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) is V24() V25() integer ext-real set
DataLoc (((Comput (P2,s2,i)) . a),k1) is Int-like Element of the carrier of SCMPDS
((Comput (P2,s2,i)) . a) + k1 is V24() V25() integer ext-real set
abs (((Comput (P2,s2,i)) . a) + k1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P2,s2,i)) . a) + k1))] is set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
dom p is non empty finite V43() set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,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 K318(2,SCMPDS) -compatible total set
K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)) is functional V41() V42() set
K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))))) is set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
m + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) is set
(Comput (P1,s1,(i + 1))) . (IC ) is set
((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) is set
(Comput (P2,s2,(i + 1))) . (IC ) is set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total 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
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
ICplusConst ((Comput (P1,s1,i)),k2) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
succ (IC (Comput (P2,s2,i))) is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real set
(IC (Comput (P2,s2,i))) + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst ((Comput (P2,s2,i)),1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst ((Comput (P2,s2,i)),k2) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
succ (IC (Comput (P1,s1,i))) is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real set
(IC (Comput (P1,s1,i))) + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst ((Comput (P1,s1,i)),1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
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
q is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() non halt-free set
p is non empty Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() q -autonomic set
s1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
s2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
i is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
m is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P2,s2,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
a is Int-like Element of the carrier of SCMPDS
(Comput (P1,s1,i)) . a is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . a is V24() V25() integer ext-real set
k1 is V24() V25() integer ext-real set
k2 is V24() V25() integer ext-real set
(a,k1) <=0_goto k2 is Element of the InstructionsF of SCMPDS
5 is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real positive Element of NAT
K202(a,k1,k2) is set
K15(5,{},K202(a,k1,k2)) is set
m + k2 is V24() V25() integer ext-real set
DataLoc (((Comput (P1,s1,i)) . a),k1) is Int-like Element of the carrier of SCMPDS
((Comput (P1,s1,i)) . a) + k1 is V24() V25() integer ext-real set
abs (((Comput (P1,s1,i)) . a) + k1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P1,s1,i)) . a) + k1))] is set
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) is V24() V25() integer ext-real set
DataLoc (((Comput (P2,s2,i)) . a),k1) is Int-like Element of the carrier of SCMPDS
((Comput (P2,s2,i)) . a) + k1 is V24() V25() integer ext-real set
abs (((Comput (P2,s2,i)) . a) + k1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P2,s2,i)) . a) + k1))] is set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
dom p is non empty finite V43() set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,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 K318(2,SCMPDS) -compatible total set
K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)) is functional V41() V42() set
K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))))) is set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
m + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) is set
(Comput (P1,s1,(i + 1))) . (IC ) is set
((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) is set
(Comput (P2,s2,(i + 1))) . (IC ) is set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total 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
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
ICplusConst ((Comput (P1,s1,i)),k2) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
succ (IC (Comput (P2,s2,i))) is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real set
(IC (Comput (P2,s2,i))) + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst ((Comput (P2,s2,i)),1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst ((Comput (P2,s2,i)),k2) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
succ (IC (Comput (P1,s1,i))) is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real set
(IC (Comput (P1,s1,i))) + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst ((Comput (P1,s1,i)),1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
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
q is Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() non halt-free set
p is non empty Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() q -autonomic set
s1 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
s2 is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
i is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCMPDS
m is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P2,s2,i) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
a is Int-like Element of the carrier of SCMPDS
(Comput (P1,s1,i)) . a is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . a is V24() V25() integer ext-real set
k1 is V24() V25() integer ext-real set
k2 is V24() V25() integer ext-real set
(a,k1) >=0_goto k2 is Element of the InstructionsF of SCMPDS
6 is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real positive Element of NAT
K202(a,k1,k2) is set
K15(6,{},K202(a,k1,k2)) is set
m + k2 is V24() V25() integer ext-real set
DataLoc (((Comput (P1,s1,i)) . a),k1) is Int-like Element of the carrier of SCMPDS
((Comput (P1,s1,i)) . a) + k1 is V24() V25() integer ext-real set
abs (((Comput (P1,s1,i)) . a) + k1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P1,s1,i)) . a) + k1))] is set
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) is V24() V25() integer ext-real set
DataLoc (((Comput (P2,s2,i)) . a),k1) is Int-like Element of the carrier of SCMPDS
((Comput (P2,s2,i)) . a) + k1 is V24() V25() integer ext-real set
abs (((Comput (P2,s2,i)) . a) + k1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
[1,(abs (((Comput (P2,s2,i)) . a) + k1))] is set
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
dom p is non empty finite V43() set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible finite V43() set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,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 K318(2,SCMPDS) -compatible total set
K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)) is functional V41() V42() set
K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))) is set
the Execution of SCMPDS is Relation-like Function-like V29( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) Element of K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))))
K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))) is Relation-like set
K32(K33( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))))) is set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
m + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) is set
(Comput (P1,s1,(i + 1))) . (IC ) is set
((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) is set
(Comput (P2,s2,(i + 1))) . (IC ) is set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total 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
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCMPDS -defined Function-like K318(2,SCMPDS) -compatible total set
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)))
K147( the InstructionsF of SCMPDS,K145(K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS)),K165(( the Object-Kind of SCMPDS * the U7 of SCMPDS))), the Execution of SCMPDS,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
ICplusConst ((Comput (P1,s1,i)),k2) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
succ (IC (Comput (P2,s2,i))) is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real set
(IC (Comput (P2,s2,i))) + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst ((Comput (P2,s2,i)),1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst ((Comput (P2,s2,i)),k2) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
succ (IC (Comput (P1,s1,i))) is non empty V17() V18() V19() V23() V24() V25() integer V64() ext-real set
(IC (Comput (P1,s1,i))) + 1 is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT
ICplusConst ((Comput (P1,s1,i)),1) is V17() V18() V19() V23() V24() V25() integer ext-real Element of NAT