let s1, s2 be State of SCMPDS; :: thesis: for I being Program of SCMPDS st I is_closed_on s1 & I is_halting_on s1 & Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & DataPart s1 = DataPart s2 holds
LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2)
let I be Program of SCMPDS; :: thesis: ( I is_closed_on s1 & I is_halting_on s1 & Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & DataPart s1 = DataPart s2 implies LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2) )
assume that
A1: I is_closed_on s1 and
A2: I is_halting_on s1 and
A3: Initialize (stop I) c= s1 and
A4: Initialize (stop I) c= s2 and
A5: DataPart s1 = DataPart s2 ; :: thesis: LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2)
I1: s1 +* (Initialize (stop I)) = (Initialize s1) +* (stop I) by COMPOS_1:125;
s1 = (Initialize s1) +* (stop I) by A3, I1, FUNCT_4:79;
then A6: ProgramPart s1 halts_on s1 by A2, SCMPDS_6:def 3;

A7: now

let k be Element of NAT ; :: thesis: ( CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) = halt SCMPDS implies LifeSpan ((ProgramPart s1),s1) <= k )
assume CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) = halt SCMPDS ; :: thesis: LifeSpan ((ProgramPart s1),s1) <= k
then CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) = halt SCMPDS by A1, A3, A4, A5, Th24;
hence LifeSpan ((ProgramPart s1),s1) <= k by A6, EXTPRO_1:def 14; :: thesis: verum

end;

CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) = halt SCMPDS by A6, EXTPRO_1:def 14;
then A8: CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1))))) = halt SCMPDS by A1, A3, A4, A5, Th24;
then ProgramPart s2 halts_on s2 by EXTPRO_1:30;
hence LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2) by A8, A7, EXTPRO_1:def 14; :: thesis: verum