theorem :: SCMFSA8C:67

for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being good really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds
( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )