theorem Th16: :: SCMFSA6B:18

for P being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being really-closed keeping_0 Program of st P +* I halts_on s holds
for J being really-closed Program of st I ";" J c= P holds
for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))