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 ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))) = LifeSpan ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I))) & Result ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))), Result ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (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 ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))) = LifeSpan ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I))) & Result ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))), Result ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (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 ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))) = LifeSpan ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I))) & Result ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))), Result ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I))) equal_outside NAT ) )
set ss1 = (Initialize s1) +* (stop I);
set ss2 = (Initialize s2) +* (stop I);
assume A2: I is_halting_on s1 ; :: thesis: ( not DataPart s1 = DataPart s2 or ( LifeSpan ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))) = LifeSpan ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I))) & Result ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))), Result ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I))) equal_outside NAT ) )
then A3: ProgramPart ((Initialize s1) +* (stop I)) halts_on (Initialize s1) +* (stop I) by SCMPDS_6:def 3;
then A4: Result ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))) = Comput ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))))) by EXTPRO_1:23;
assume A5: DataPart s1 = DataPart s2 ; :: thesis: ( LifeSpan ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))) = LifeSpan ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I))) & Result ((ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I))), Result ((ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I))) equal_outside NAT )
then I is_halting_on s2 by A1, A2, SCMPDS_6:37;
then A6: ProgramPart ((Initialize s2) +* (stop I)) halts_on (Initialize s2) +* (stop I) by SCMPDS_6:def 3;

A7: now

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

end;

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