theorem Th19: :: SCMFSA8A:28

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 Initialized s,P holds
for k being Nat st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA )