let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s1, s2 being State of SCMPDS
for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* (stop I)),()) = LifeSpan ((P2 +* (stop I)),()) & Result ((P1 +* (stop I)),()) = Result ((P2 +* (stop I)),()) )

let s1, s2 be State of SCMPDS; :: thesis: for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* (stop I)),()) = LifeSpan ((P2 +* (stop I)),()) & Result ((P1 +* (stop I)),()) = Result ((P2 +* (stop I)),()) )

let I be Program of ; :: thesis: ( I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 implies ( LifeSpan ((P1 +* (stop I)),()) = LifeSpan ((P2 +* (stop I)),()) & Result ((P1 +* (stop I)),()) = Result ((P2 +* (stop I)),()) ) )
assume A1: I is_closed_on s1,P1 ; :: thesis: ( not I is_halting_on s1,P1 or not DataPart s1 = DataPart s2 or ( LifeSpan ((P1 +* (stop I)),()) = LifeSpan ((P2 +* (stop I)),()) & Result ((P1 +* (stop I)),()) = Result ((P2 +* (stop I)),()) ) )
set ss1 = Initialize s1;
set PP1 = P1 +* (stop I);
set ss2 = Initialize s2;
set PP2 = P2 +* (stop I);
assume A2: I is_halting_on s1,P1 ; :: thesis: ( not DataPart s1 = DataPart s2 or ( LifeSpan ((P1 +* (stop I)),()) = LifeSpan ((P2 +* (stop I)),()) & Result ((P1 +* (stop I)),()) = Result ((P2 +* (stop I)),()) ) )
then A3: P1 +* (stop I) halts_on Initialize s1 by SCMPDS_6:def 3;
then A4: Result ((P1 +* (stop I)),()) = Comput ((P1 +* (stop I)),(),(LifeSpan ((P1 +* (stop I)),()))) by EXTPRO_1:23;
assume A5: DataPart s1 = DataPart s2 ; :: thesis: ( LifeSpan ((P1 +* (stop I)),()) = LifeSpan ((P2 +* (stop I)),()) & Result ((P1 +* (stop I)),()) = Result ((P2 +* (stop I)),()) )
then I is_halting_on s2,P2 by ;
then A6: P2 +* (stop I) halts_on Initialize s2 by SCMPDS_6:def 3;
A7: now :: thesis: for l being Nat st CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(),l))) = halt SCMPDS holds
LifeSpan ((P1 +* (stop I)),()) <= l
let l be Nat; :: thesis: ( CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(),l))) = halt SCMPDS implies LifeSpan ((P1 +* (stop I)),()) <= l )
assume A8: CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(),l))) = halt SCMPDS ; :: thesis: LifeSpan ((P1 +* (stop I)),()) <= l
CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(),l))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(),l))) by A1, A5, Th6;
hence LifeSpan ((P1 +* (stop I)),()) <= l by ; :: thesis: verum
end;
CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(),(LifeSpan ((P1 +* (stop I)),()))))) = CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(),(LifeSpan ((P1 +* (stop I)),()))))) by A1, A5, Th6
.= halt SCMPDS by ;
hence LifeSpan ((P1 +* (stop I)),()) = LifeSpan ((P2 +* (stop I)),()) by ; :: thesis: Result ((P1 +* (stop I)),()) = Result ((P2 +* (stop I)),())
then Result ((P2 +* (stop I)),()) = Comput ((P2 +* (stop I)),(),(LifeSpan ((P1 +* (stop I)),()))) by ;
hence Result ((P1 +* (stop I)),()) = Result ((P2 +* (stop I)),()) by A1, A5, A4, Th6; :: thesis: verum