theorem Th17: :: SCMPDS_6:26

for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS
for I being Program of
for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I