theorem Th8: :: SCMPDS_7:10

for P1, P2 being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being Program of st I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )