let s1, s2 be State of ; :: thesis: for I being Program of st I is_closed_on s1 & I is_halting_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & DataPart s1 = DataPart s2 holds
LifeSpan s1 = LifeSpan s2
let I be Program of ; :: thesis: ( I is_closed_on s1 & I is_halting_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & DataPart s1 = DataPart s2 implies LifeSpan s1 = LifeSpan s2 )
set IsI = Initialized (stop I);
assume that
A1: I is_closed_on s1 and
A2: I is_halting_on s1 and
A3: Initialized (stop I) c= s1 and
A4: Initialized (stop I) c= s2 and
A5: DataPart s1 = DataPart s2 ; :: thesis: LifeSpan s1 = LifeSpan s2
s1 = s1 +* (Initialized (stop I)) by A3, 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 (Computation s2,k) = halt SCMPDS implies LifeSpan s1 <= k )
assume CurInstr (Computation s2,k) = halt SCMPDS ; :: thesis: LifeSpan s1 <= k
then CurInstr (Computation s1,k) = halt SCMPDS by A1, A3, A4, A5, Th24;
hence LifeSpan s1 <= k by A6, AMI_1:def 46; :: thesis: verum

end;

CurInstr (Computation s1,(LifeSpan s1)) = halt SCMPDS by A6, AMI_1:def 46;
then A8: CurInstr (Computation s2,(LifeSpan s1)) = halt SCMPDS by A1, A3, A4, A5, Th24;
then ProgramPart s2 halts_on s2 by AMI_1:146;
hence LifeSpan s1 = LifeSpan s2 by A8, A7, AMI_1:def 46; :: thesis: verum