theorem :: SCMFSA8B:42

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 s . (intloc 0) = 1 holds
( I is_halting_on s,p iff I is_halting_on Initialized s,p )