theorem :: SCMFSA8A:38

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