for P1, P2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA
for a being Int-Location st not I refers a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
for k being Nat holds
( ( for b being Int-Location st a <> b holds
(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) & IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) )