theorem Th18: :: SCMPDS_5:30

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
for k being Nat st k <= LifeSpan ((P +* (stop I)),s) holds
Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k)