theorem Th11: :: SCMFSA6B:13

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
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I