theorem :: SCMFSA8A:33

for I being really-closed Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_halting_on Initialized s,P holds
DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by Lm4;