theorem Th12: :: SCMFSA6B:14

for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of st P +* I halts_on s & Directed I c= P holds
DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))