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)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) )

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)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) )

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)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) ) )

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)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) ) )

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)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) ) )

then A3: P1 +* (stop I) halts_on Initialize s1 by SCMPDS_6:def 3;

then A4: Result ((P1 +* (stop I)),(Initialize s1)) = Comput ((P1 +* (stop I)),(Initialize s1),(LifeSpan ((P1 +* (stop I)),(Initialize s1)))) by EXTPRO_1:23;

assume A5: DataPart s1 = DataPart s2 ; :: thesis: ( LifeSpan ((P1 +* (stop I)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) )

then I is_halting_on s2,P2 by A1, A2, SCMPDS_6:23;

then A6: P2 +* (stop I) halts_on Initialize s2 by SCMPDS_6:def 3;

.= halt SCMPDS by A3, EXTPRO_1:def 15 ;

hence LifeSpan ((P1 +* (stop I)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) by A7, A6, EXTPRO_1:def 15; :: thesis: Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2))

then Result ((P2 +* (stop I)),(Initialize s2)) = Comput ((P2 +* (stop I)),(Initialize s2),(LifeSpan ((P1 +* (stop I)),(Initialize s1)))) by A6, EXTPRO_1:23;

hence Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) by A1, A5, A4, Th6; :: thesis: verum

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)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) )

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)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) )

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)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) ) )

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)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) ) )

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)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) ) )

then A3: P1 +* (stop I) halts_on Initialize s1 by SCMPDS_6:def 3;

then A4: Result ((P1 +* (stop I)),(Initialize s1)) = Comput ((P1 +* (stop I)),(Initialize s1),(LifeSpan ((P1 +* (stop I)),(Initialize s1)))) by EXTPRO_1:23;

assume A5: DataPart s1 = DataPart s2 ; :: thesis: ( LifeSpan ((P1 +* (stop I)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) & Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) )

then I is_halting_on s2,P2 by A1, A2, SCMPDS_6:23;

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)),(Initialize s2),l))) = halt SCMPDS holds

LifeSpan ((P1 +* (stop I)),(Initialize s1)) <= l

CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),(LifeSpan ((P1 +* (stop I)),(Initialize s1)))))) =
CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),(LifeSpan ((P1 +* (stop I)),(Initialize s1))))))
by A1, A5, Th6
LifeSpan ((P1 +* (stop I)),(Initialize s1)) <= l

let l be Nat; :: thesis: ( CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),l))) = halt SCMPDS implies LifeSpan ((P1 +* (stop I)),(Initialize s1)) <= l )

assume A8: CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),l))) = halt SCMPDS ; :: thesis: LifeSpan ((P1 +* (stop I)),(Initialize s1)) <= l

CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),l))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),l))) by A1, A5, Th6;

hence LifeSpan ((P1 +* (stop I)),(Initialize s1)) <= l by A3, A8, EXTPRO_1:def 15; :: thesis: verum

end;assume A8: CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),l))) = halt SCMPDS ; :: thesis: LifeSpan ((P1 +* (stop I)),(Initialize s1)) <= l

CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),l))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),l))) by A1, A5, Th6;

hence LifeSpan ((P1 +* (stop I)),(Initialize s1)) <= l by A3, A8, EXTPRO_1:def 15; :: thesis: verum

.= halt SCMPDS by A3, EXTPRO_1:def 15 ;

hence LifeSpan ((P1 +* (stop I)),(Initialize s1)) = LifeSpan ((P2 +* (stop I)),(Initialize s2)) by A7, A6, EXTPRO_1:def 15; :: thesis: Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2))

then Result ((P2 +* (stop I)),(Initialize s2)) = Comput ((P2 +* (stop I)),(Initialize s2),(LifeSpan ((P1 +* (stop I)),(Initialize s1)))) by A6, EXTPRO_1:23;

hence Result ((P1 +* (stop I)),(Initialize s1)) = Result ((P2 +* (stop I)),(Initialize s2)) by A1, A5, A4, Th6; :: thesis: verum