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 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1,s2 equal_outside NAT holds
( LifeSpan s1 = LifeSpan s2 & Result s1, Result s2 equal_outside NAT )
let I be Program of SCMPDS ; :: thesis: ( I is_closed_on s1 & I is_halting_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1,s2 equal_outside NAT implies ( LifeSpan s1 = LifeSpan s2 & Result s1, Result s2 equal_outside NAT ) )
set iI = Initialized (stop I);
assume that
A1: I is_closed_on s1 and
A2: I is_halting_on s1 and
A3: Initialized (stop I) c= s1 and
A4: Initialized (stop I) c= s2 and
A5: s1,s2 equal_outside NAT ; :: thesis: ( LifeSpan s1 = LifeSpan s2 & Result s1, Result 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;
s2 = s2 +* (Initialized (stop I)) by A4, FUNCT_4:79;
then A7: ProgramPart s2 halts_on s2 by A6, SCMPDS_6:def 3;
s1 = s1 +* (Initialized (stop I)) by A3, 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 (Comput (ProgramPart s2),s2,l)),(Comput (ProgramPart s2),s2,l) = halt SCMPDS implies LifeSpan s1 <= l )
assume A10: CurInstr (ProgramPart (Comput (ProgramPart s2),s2,l)),(Comput (ProgramPart s2),s2,l) = halt SCMPDS ; :: thesis: LifeSpan s1 <= l
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,l)),(Comput (ProgramPart s1),s1,l) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,l)),(Comput (ProgramPart s2),s2,l) by A1, A3, A4, A5, Th26;
hence LifeSpan s1 <= l by A8, A10, AMI_1:def 46; :: thesis: verum

end;

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