let s1, s2 be State of SCMPDS ; :: thesis: for I being Program of SCMPDS st DataPart s1 = DataPart s2 & I is_closed_on s1 & I is_halting_on s1 holds
( I is_closed_on s2 & I is_halting_on s2 )
let I be Program of SCMPDS ; :: thesis: ( DataPart s1 = DataPart s2 & I is_closed_on s1 & I is_halting_on s1 implies ( I is_closed_on s2 & I is_halting_on s2 ) )
set pI = stop I;
set IsI = Initialized (stop I);
set S1 = s1 +* (Initialized (stop I));
set S2 = s2 +* (Initialized (stop I));
defpred S1[ Element of NAT ] means ( IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),$1) = IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),$1) & CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),$1)),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),$1) = CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),$1)),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),$1) & DataPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),$1) = DataPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),$1) );
A1: Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 = s1 +* (Initialized (stop I)) by AMI_1:13;
A2: Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),0 = s2 +* (Initialized (stop I)) by AMI_1:13;
assume DataPart s1 = DataPart s2 ; :: thesis: ( not I is_closed_on s1 or not I is_halting_on s1 or ( I is_closed_on s2 & I is_halting_on s2 ) )
then A3: Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 , Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),0 equal_outside NAT by A1, A2, Th12;
A4: 0 in dom (stop I) by SCMPDS_4:75;
A5: stop I c= Initialized (stop I) by SCMPDS_4:9;
then A6: dom (stop I) c= dom (Initialized (stop I)) by GRFUNC_1:8;
assume A7: I is_closed_on s1 ; :: thesis: ( not I is_halting_on s1 or ( I is_closed_on s2 & I is_halting_on s2 ) )
A8: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
T: ProgramPart (s2 +* (Initialized (stop I))) = ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) by AMI_1:144;
A9: Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(k + 1) = Following (ProgramPart (s2 +* (Initialized (stop I)))),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k)),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k)),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) by T ;
assume A10: S1[k] ; :: thesis: S1[k + 1]
then for a being Int_position holds (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) . a = (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) . a by SCMPDS_4:23;
then A11: Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k, Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k equal_outside NAT by A10, SCMPDS_4:11;
Initialized (stop I) c= s2 +* (Initialized (stop I)) by FUNCT_4:26;
then stop I c= s2 +* (Initialized (stop I)) by A5, XBOOLE_1:1;
then A12: stop I c= Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(k + 1) by AMI_1:81;
A13: IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1)) in dom (stop I) by A7, Def2;
T: ProgramPart (s1 +* (Initialized (stop I))) = ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) by AMI_1:144;
A14: Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1) = Following (ProgramPart (s1 +* (Initialized (stop I)))),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k)),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k)),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) by T ;
then A15: IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1)) = IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(k + 1)) by A10, A11, A9, AMI_1:121, SCMPDS_4:15;
Y: (ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1))) /. (IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1))) = (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1)) . (IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1))) by AMI_1:150;
Z: (ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(k + 1))) /. (IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(k + 1))) = (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(k + 1)) . (IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(k + 1))) by AMI_1:150;
Initialized (stop I) c= s1 +* (Initialized (stop I)) by FUNCT_4:26;
then stop I c= s1 +* (Initialized (stop I)) by A5, XBOOLE_1:1;
then stop I c= Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1) by AMI_1:81;
then CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1))),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1)) = (stop I) . (IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1))) by A13, GRFUNC_1:8, Y
.= CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(k + 1))),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(k + 1)) by A12, A15, A13, GRFUNC_1:8, Z ;
hence S1[k + 1] by A10, A11, A14, A9, A15, SCMPDS_4:15, SCMPDS_4:24; :: thesis: verum
end;
A16: IC SCMPDS in dom (Initialized (stop I)) by SCMPDS_4:7;
then A17: IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),0 ) = (Initialized (stop I)) . (IC SCMPDS ) by A2, FUNCT_4:14
.= 0 by SCMPDS_4:29 ;
assume I is_halting_on s1 ; :: thesis: ( I is_closed_on s2 & I is_halting_on s2 )
then ProgramPart (s1 +* (Initialized (stop I))) halts_on s1 +* (Initialized (stop I)) by Def3;
then consider m being Element of NAT such that
A18: CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),m)),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),m) = halt SCMPDS by AMI_1:146;
Y: (ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 )) /. (IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 )) = (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 ) . (IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 )) by AMI_1:150;
Z: (ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),0 )) /. (IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),0 )) = (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),0 ) . (IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),0 )) by AMI_1:150;
A19: IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 ) = (Initialized (stop I)) . (IC SCMPDS ) by A16, A1, FUNCT_4:14
.= 0 by SCMPDS_4:29 ;
then CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 )),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 ) = (Initialized (stop I)) . 0 by A1, A6, A4, FUNCT_4:14, Y
.= CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),0 )),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),0 ) by A2, A17, A6, A4, FUNCT_4:14, Z ;
then A20: S1[ 0 ] by A19, A17, A3, SCMPDS_4:24;
now
let k be Element of NAT ; :: thesis: IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) in dom (stop I)
A21: for k being Element of NAT holds S1[k] from NAT_1:sch 1(A20, A8);
 IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) in dom (stop I) by A7, Def2;
hence IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) in dom (stop I) by A21; :: thesis: verum
end;
hence I is_closed_on s2 by Def2; :: thesis: I is_halting_on s2
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A20, A8);
 then CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),m)),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),m) = halt SCMPDS by A18;
then ProgramPart (s2 +* (Initialized (stop I))) halts_on s2 +* (Initialized (stop I)) by AMI_1:146;
hence I is_halting_on s2 by Def3; :: thesis: verum