theorem Th4: :: SCM_HALT:6

for s1, s2 being State of SCM+FSA
for p1, p2 being Instruction-Sequence of SCM+FSA
for J being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & J c= p1 holds
for n being Nat st Reloc (J,n) c= p2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (p1,s1,i))) + n = IC (Comput (p2,s2,i)) & IncAddr ((CurInstr (p1,(Comput (p1,s1,i)))),n) = CurInstr (p2,(Comput (p2,s2,i))) & DataPart (Comput (p1,s1,i)) = DataPart (Comput (p2,s2,i)) )