let s1, s2 be 0 -started State of SCMPDS; :: thesis: for I being parahalting Program of SCMPDS st stop I c= s1 & 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 parahalting Program of SCMPDS; :: thesis: ( stop I c= s1 & 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 ) )
set SI = stop I;
assume that
A1: stop I c= s1 and
A2: stop I c= s2 and
A3: 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 )
A4: ProgramPart s2 halts_on s2 by A2, SCMPDS_4:def 10;
A5: ProgramPart s1 halts_on s1 by A1, SCMPDS_4:def 10;

A6: 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 A7: 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, A2, A3, Th20;
hence LifeSpan ((ProgramPart s1),s1) <= l by A5, A7, 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, A2, A3, Th20
.= halt SCMPDS by A5, EXTPRO_1:def 14 ;
hence LifeSpan ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2) by A6, A4, EXTPRO_1:def 14; :: thesis: Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT
then A8: Result ((ProgramPart s2),s2) = Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1))) by A2, EXTPRO_1:23, SCMPDS_4:def 10;
Result ((ProgramPart s1),s1) = Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1))) by A1, EXTPRO_1:23, SCMPDS_4:def 10;
hence Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT by A1, A2, A3, A8, Th20; :: thesis: verum