theorem Th12: :: SCMFSA8A:21

for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds
for k being Nat st k <= LifeSpan ((P +* I),(Initialize s)) holds
( Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA )