for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA st I is_halting_on Initialized s,P holds
( ( for k being Nat st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) )