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 & DataPart s1 = DataPart s2 holds
( LifeSpan (s1 +* (Initialized (stop I))) = LifeSpan (s2 +* (Initialized (stop I))) & Result (s1 +* (Initialized (stop I))), Result (s2 +* (Initialized (stop I))) equal_outside NAT )
let I be Program of SCMPDS ; :: thesis: ( I is_closed_on s1 & I is_halting_on s1 & DataPart s1 = DataPart s2 implies ( LifeSpan (s1 +* (Initialized (stop I))) = LifeSpan (s2 +* (Initialized (stop I))) & Result (s1 +* (Initialized (stop I))), Result (s2 +* (Initialized (stop I))) equal_outside NAT ) )
assume A1: I is_closed_on s1 ; :: thesis: ( not I is_halting_on s1 or not DataPart s1 = DataPart s2 or ( LifeSpan (s1 +* (Initialized (stop I))) = LifeSpan (s2 +* (Initialized (stop I))) & Result (s1 +* (Initialized (stop I))), Result (s2 +* (Initialized (stop I))) equal_outside NAT ) )
set IsI = Initialized (stop I);
set ss1 = s1 +* (Initialized (stop I));
set ss2 = s2 +* (Initialized (stop I));
assume A2: I is_halting_on s1 ; :: thesis: ( not DataPart s1 = DataPart s2 or ( LifeSpan (s1 +* (Initialized (stop I))) = LifeSpan (s2 +* (Initialized (stop I))) & Result (s1 +* (Initialized (stop I))), Result (s2 +* (Initialized (stop I))) equal_outside NAT ) )
then A3: ProgramPart (s1 +* (Initialized (stop I))) halts_on s1 +* (Initialized (stop I)) by SCMPDS_6:def 3;
then A4: Result (s1 +* (Initialized (stop I))) = Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(LifeSpan (s1 +* (Initialized (stop I)))) by AMI_1:122;
assume A5: DataPart s1 = DataPart s2 ; :: thesis: ( LifeSpan (s1 +* (Initialized (stop I))) = LifeSpan (s2 +* (Initialized (stop I))) & Result (s1 +* (Initialized (stop I))), Result (s2 +* (Initialized (stop I))) equal_outside NAT )
then I is_halting_on s2 by A1, A2, SCMPDS_6:37;
then A6: ProgramPart (s2 +* (Initialized (stop I))) halts_on s2 +* (Initialized (stop I)) by SCMPDS_6:def 3;

A7: now

let l be Element of NAT ; :: thesis: ( CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),l)),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),l) = halt SCMPDS implies LifeSpan (s1 +* (Initialized (stop I))) <= l )
assume A8: CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),l)),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),l) = halt SCMPDS ; :: thesis: LifeSpan (s1 +* (Initialized (stop I))) <= l
CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),l)),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),l) = CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),l)),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),l) by A1, A5, Th25;
hence LifeSpan (s1 +* (Initialized (stop I))) <= l by A3, A8, AMI_1:def 46; :: thesis: verum

end;

CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(LifeSpan (s1 +* (Initialized (stop I)))))),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(LifeSpan (s1 +* (Initialized (stop I))))) = CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(LifeSpan (s1 +* (Initialized (stop I)))))),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(LifeSpan (s1 +* (Initialized (stop I))))) by A1, A5, Th25
.= halt SCMPDS by A3, AMI_1:def 46 ;
hence LifeSpan (s1 +* (Initialized (stop I))) = LifeSpan (s2 +* (Initialized (stop I))) by A7, A6, AMI_1:def 46; :: thesis: Result (s1 +* (Initialized (stop I))), Result (s2 +* (Initialized (stop I))) equal_outside NAT
then Result (s2 +* (Initialized (stop I))) = Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(LifeSpan (s1 +* (Initialized (stop I)))) by A6, AMI_1:122;
hence Result (s1 +* (Initialized (stop I))), Result (s2 +* (Initialized (stop I))) equal_outside NAT by A1, A5, A4, Th25; :: thesis: verum