theorem Th6: :: SCMPDS_5:17
for P1, P2 being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being parahalting Program of st stop I c= P1 & stop I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )