for P1, P2 being Instruction-Sequence of SCM+FSA
for s1 being 0 -started State of SCM+FSA
for s2 being State of SCM+FSA
for I being Program of SCM+FSA st I c= P1 & I is_pseudo-closed_on s1,P1 holds
for n being Nat st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Nat st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Nat st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) )