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 & Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & s1,s2 equal_outside NAT holds
( LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2) & Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
let I be Program of SCMPDS; :: thesis: ( I is_closed_on s1 & I is_halting_on s1 & Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & s1,s2 equal_outside NAT implies ( LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2) & Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT ) )
assume that
A1: I is_closed_on s1 and
A2: I is_halting_on s1 and
A3: Initialize (stop I) c= s1 and
A4: Initialize (stop I) c= s2 and
A5: s1,s2 equal_outside NAT ; :: thesis: ( LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2) & Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
DataPart s1 = DataPart s2 by A5, SCMPDS_6:4;
then A6: I is_halting_on s2 by A1, A2, SCMPDS_6:37;
I1: (Initialize s1) +* (stop I) = s1 +* (Initialize (stop I)) by COMPOS_1:125;
I2: (Initialize s2) +* (stop I) = s2 +* (Initialize (stop I)) by COMPOS_1:125;
s2 = (Initialize s2) +* (stop I) by A4, I2, FUNCT_4:79;
then A7: ProgramPart s2 halts_on s2 by A6, SCMPDS_6:def 3;
s1 = (Initialize s1) +* (stop I) by A3, I1, FUNCT_4:79;
then A8: ProgramPart s1 halts_on s1 by A2, SCMPDS_6:def 3;

A9: now

let l be Element of NAT ; :: thesis: ( CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,l))) = halt SCMPDS implies LifeSpan ((ProgramPart s1),s1) <= l )
assume A10: CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,l))) = halt SCMPDS ; :: thesis: LifeSpan ((ProgramPart s1),s1) <= l
CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,l))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,l))) by A1, A3, A4, A5, Th26;
hence LifeSpan ((ProgramPart s1),s1) <= l by A8, A10, EXTPRO_1:def 14; :: thesis: verum

end;

CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1))))) = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))))) by A1, A3, A4, A5, Th26
.= halt SCMPDS by A8, EXTPRO_1:def 14 ;
hence LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2) by A9, A7, EXTPRO_1:def 14; :: thesis: Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT
then A11: Result ((ProgramPart s2),s2) = Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1))) by A7, EXTPRO_1:23;
Result ((ProgramPart s1),s1) = Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))) by A8, EXTPRO_1:23;
hence Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT by A1, A3, A4, A5, A11, Th26; :: thesis: verum