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 & ex k being Element of NAT st Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT holds
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 & ex k being Element of NAT st Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT implies Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
set pI = stop I;
assume A1: I is_closed_on s1 ; :: thesis: ( not I is_halting_on s1 or not Initialize (stop I) c= s1 or not Initialize (stop I) c= s2 or for k being Element of NAT holds not Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT or Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
A2: s1 +* (Initialize (stop I)) = (Initialize s1) +* (stop I) by COMPOS_1:125;
assume A3: I is_halting_on s1 ; :: thesis: ( not Initialize (stop I) c= s1 or not Initialize (stop I) c= s2 or for k being Element of NAT holds not Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT or Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
assume A4: Initialize (stop I) c= s1 ; :: thesis: ( not Initialize (stop I) c= s2 or for k being Element of NAT holds not Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT or Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
then A5: s1 = (Initialize s1) +* (stop I) by A2, FUNCT_4:79;
then A6: ProgramPart s1 halts_on s1 by A3, SCMPDS_6:def 3;
then consider n being Element of NAT such that
A7: CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,n))) = halt SCMPDS by EXTPRO_1:30;
A8: s2 +* (Initialize (stop I)) = (Initialize s2) +* (stop I) by COMPOS_1:125;
assume Initialize (stop I) c= s2 ; :: thesis: ( for k being Element of NAT holds not Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT or Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT )
then A9: s2 = (Initialize s2) +* (stop I) by A8, FUNCT_4:79;
given k being Element of NAT such that A10: Comput ((ProgramPart s1),s1,k),s2 equal_outside NAT ; :: thesis: Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT
set s3 = Comput ((ProgramPart s1),s1,k);
A11: IC in dom (Comput ((ProgramPart s1),s1,k)) by COMPOS_1:9;
A12: (Comput ((ProgramPart s1),s1,k)) +* (Initialize (stop I)) = (Initialize (Comput ((ProgramPart s1),s1,k))) +* (stop I) by COMPOS_1:125;
stop I c= Initialize (stop I) by COMPOS_1:126;
then stop I c= s1 by A4, XBOOLE_1:1;
then A13: stop I c= Comput ((ProgramPart s1),s1,k) by AMI_1:86;
IC (Comput ((ProgramPart s1),s1,k)) = IC ((Initialize s2) +* (stop I)) by A10, A9, COMPOS_1:24
.= 0 by SCMPDS_6:21 ;
then (IC ) .--> 0 c= Comput ((ProgramPart s1),s1,k) by A11, FUNCOP_1:88;
then Initialize (stop I) c= Comput ((ProgramPart s1),s1,k) by A13, FUNCT_4:92;
then A14: Comput ((ProgramPart s1),s1,k) = (Initialize (Comput ((ProgramPart s1),s1,k))) +* (stop I) by A12, FUNCT_4:79;

A15: now

let n be Element of NAT ; :: thesis: IC (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)),n)) in dom (stop I)
A16: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
IC (Comput ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k)),n)) = IC (Comput ((ProgramPart s1),s1,(k + n))) by EXTPRO_1:5;
hence IC (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)),n)) in dom (stop I) by A1, A5, A16, SCMPDS_6:def 2; :: thesis: verum

end;

A17: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
A18: Comput ((ProgramPart s1),s1,(k + n)) = Comput ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k)),n) by EXTPRO_1:5;
A19: Comput ((ProgramPart s1),s1,(k + n)) = Comput ((ProgramPart s1),s1,n) by A7, EXTPRO_1:6, NAT_1:11;
CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)),n))) = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,(k + n)))) by A18, A17
.= CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,n))) by A19 ;
then ProgramPart (Comput ((ProgramPart s1),s1,k)) halts_on Comput ((ProgramPart s1),s1,k) by A7, EXTPRO_1:30;
then A20: I is_halting_on Comput ((ProgramPart s1),s1,k) by A14, SCMPDS_6:def 3;
A21: DataPart (Comput ((ProgramPart s1),s1,k)) = DataPart s2 by A10, SCMPDS_6:4;
consider k being Element of NAT such that
A22: CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) = halt SCMPDS by A6, EXTPRO_1:30;
A23: (ProgramPart (Comput ((ProgramPart s1),s1,k))) /. (IC (Comput ((ProgramPart s1),s1,k))) = (Comput ((ProgramPart s1),s1,k)) . (IC (Comput ((ProgramPart s1),s1,k))) by COMPOS_1:38;
A24: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
A25: (ProgramPart s1) . (IC (Comput ((ProgramPart s1),s1,k))) = s1 . (IC (Comput ((ProgramPart s1),s1,k))) by COMPOS_1:2
.= halt SCMPDS by A22, A23, A24, AMI_1:54 ;
A26: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
I is_closed_on Comput ((ProgramPart s1),s1,k) by A14, A15, SCMPDS_6:def 2;
then Result ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k))), Result ((ProgramPart s2),s2) equal_outside NAT by A9, A21, A14, A20, Th29;
hence Result ((ProgramPart s1),s1), Result ((ProgramPart s2),s2) equal_outside NAT by A25, A26, EXTPRO_1:9; :: thesis: verum