theorem Th10: :: SCM_HALT:12

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 p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds
DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1)))