for P1, P2 being Instruction-Sequence of SCMPDS
for s1, s2 being State of SCMPDS
for I being Program of st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 holds
for k being Nat holds
( Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )