theorem :: SCMFSA8A:36

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