theorem :: SCMPDS_3:16

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 b₃ -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 )