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 being Nat
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))