theorem :: SCMFSA8A:39

for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st I is_halting_on Initialized s,P holds
P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by Lm6;