theorem Th12: :: SCMPDS_5:24

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