theorem Th21: :: SCMPDS_5:33

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of
for J being parahalting shiftable Program of holds LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s)))))