theorem Th8: :: SCMPDS_5:20

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being parahalting Program of
for J being Program of st stop I c= P holds
for m being Nat st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (stop (I ';' J))),s,m)