theorem :: SCMFSA8A:41

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
IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))