theorem :: SCMFSA8A:32

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
IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I by Lm4;