theorem Th17: :: SCMPDS_5:29

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 +* (I ';' J)),s,k)