theorem
for
P1,
P2 being
Instruction-Sequence of
SCMPDS for
q being
NAT -defined the
InstructionsF of
SCMPDS -valued finite non
halt-free Function for
p being non
empty b3 -autonomic FinPartState of
SCMPDS for
s1,
s2 being
State of
SCMPDS st
p c= s1 &
p c= s2 &
q c= P1 &
q c= P2 holds
for
i,
m being
Nat for
a being
Int_position for
k1,
k2 being
Integer st
CurInstr (
P1,
(Comput (P1,s1,i)))
= (
a,
k1)
>=0_goto k2 &
m = IC (Comput (P1,s1,i)) &
m + k2 >= 0 &
k2 <> 1 holds
(
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) < 0 iff
(Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) < 0 )