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

A12: 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)
T: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,k) by AMI_1:144;
IC (Comput (ProgramPart s1),(Comput (ProgramPart s1),s1,k),n) = IC (Comput (ProgramPart s1),s1,(k + n)) by AMI_1:51;
hence IC (Comput (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k),n) in dom (stop I) by A1, A4, SCMPDS_6:def 2, T; :: thesis: verum

end;

T: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,k) by AMI_1:144;
x: Comput (ProgramPart s1),s1,(k + n) = Comput (ProgramPart s1),(Comput (ProgramPart s1),s1,k),n by AMI_1:51;
U: Comput (ProgramPart s1),s1,(k + n) = Comput (ProgramPart s1),s1,n by A6, AMI_1:52, NAT_1:11, TX;
CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k),n)),(Comput (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k),n) = CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + n))),(Comput (ProgramPart s1),s1,(k + n)) by x, T
.= CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) by U ;
then ProgramPart (Comput (ProgramPart s1),s1,k) halts_on Comput (ProgramPart s1),s1,k by A6, AMI_1:146;
then A13: I is_halting_on Comput (ProgramPart s1),s1,k by A11, SCMPDS_6:def 3;
A14: DataPart (Comput (ProgramPart s1),s1,k) = DataPart s2 by A8, SCMPDS_6:4;
consider k being Element of NAT such that
A15: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = halt SCMPDS by A5, AMI_1:146;
Y: (ProgramPart (Comput (ProgramPart s1),s1,k)) /. (IC (Comput (ProgramPart s1),s1,k)) = (Comput (ProgramPart s1),s1,k) . (IC (Comput (ProgramPart s1),s1,k)) by AMI_1:150;
A16: s1 . (IC (Comput (ProgramPart s1),s1,k)) = halt SCMPDS by A15, AMI_1:54, Y;
I is_closed_on Comput (ProgramPart s1),s1,k by A11, A12, SCMPDS_6:def 2;
then Result (Comput (ProgramPart s1),s1,k), Result s2 equal_outside NAT by A7, A14, A11, A13, Th29;
hence Result s1, Result s2 equal_outside NAT by A16, AMI_1:57; :: thesis: verum