for s2 being State of SCM+FSA
for s1 being 0 -started State of SCM+FSA
for P, Q being Instruction-Sequence of SCM+FSA
for J being really-closed parahalting Program of st J c= P holds
for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )