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 S1 = (Initialize s1) +* (stop I);
set S2 = (Initialize s2) +* (stop I);
I1: s1 +* (Initialize (stop I)) = (Initialize s1) +* (stop I) by SCMPDS_4:5;
I2: s2 +* (Initialize (stop I)) = (Initialize s2) +* (stop I) by SCMPDS_4:5;
defpred S₁[ Element of NAT ] means ( IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),$1) = IC (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),$1) & CurInstr (ProgramPart ((Initialize s1) +* (stop I))),(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),$1) = CurInstr (ProgramPart ((Initialize s2) +* (stop I))),(Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),$1) & DataPart (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),$1) = DataPart (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),$1) );
A1: Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 = (Initialize s1) +* (stop I) by AMI_1:13;
A2: Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 = (Initialize s2) +* (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 ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 , Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 equal_outside NAT by A1, A2, Th12;
A4: 0 in dom (stop I) by SCMPDS_4:75;
A5: stop I c= Initialize (stop I) by SCMPDS_4:9;
then A6: dom (stop I) c= dom (Initialize (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: ( S₁[k] implies S₁[k + 1] )
T: ProgramPart ((Initialize s2) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) by AMI_1:123;
A9: Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1) = Following (ProgramPart ((Initialize s2) +* (stop I))),(Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k)),(Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k)),(Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) by T ;
assume A10: S₁[k] ; :: thesis: S₁[k + 1]
then for a being Int_position holds (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k) . a = (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) . a by SCMPDS_4:23;
then A11: Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k, Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k equal_outside NAT by A10, SCMPDS_4:11;
Initialize (stop I) c= (Initialize s2) +* (stop I) by I2, FUNCT_4:26;
then stop I c= (Initialize s2) +* (stop I) by A5, XBOOLE_1:1;
then A12: stop I c= Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1) by AMI_1:81;
A13: IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1)) in dom (stop I) by A7, Def2;
A14: Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1) = Following (ProgramPart ((Initialize s1) +* (stop I))),(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k) by AMI_1:14
.= Exec (CurInstr (ProgramPart ((Initialize s1) +* (stop I))),(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k)),(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k) ;
then A15: IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1)) = IC (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1)) by A10, A11, A9, T, COMPOS_1:24, SCMPDS_4:15;
Y: (ProgramPart (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1))) /. (IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1))) = (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1)) . (IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1))) by COMPOS_1:38;
Z: (ProgramPart (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1))) /. (IC (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1))) = (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1)) . (IC (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1))) by COMPOS_1:38;
TX1: ProgramPart ((Initialize s1) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1)) by AMI_1:123;
TX2: ProgramPart ((Initialize s2) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1)) by AMI_1:123;
Initialize (stop I) c= s1 +* (Initialize (stop I)) by FUNCT_4:26;
then stop I c= (Initialize s1) +* (stop I) by A5, I1, XBOOLE_1:1;
then stop I c= Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1) by AMI_1:81;
then CurInstr (ProgramPart ((Initialize s1) +* (stop I))),(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1)) = (stop I) . (IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1))) by A13, Y, TX1, GRFUNC_1:8
.= CurInstr (ProgramPart ((Initialize s2) +* (stop I))),(Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1)) by A12, A15, A13, Z, TX2, GRFUNC_1:8 ;
hence S₁[k + 1] by A10, A11, A14, A9, A15, T, SCMPDS_4:15, SCMPDS_4:24; :: thesis: verum

end;

A16: IC SCMPDS in dom (Initialize (stop I)) by COMPOS_1:def 16;
then A17: IC (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 ) = IC (Initialize (stop I)) by A2, I2, FUNCT_4:14
.= 0 by COMPOS_1:def 16 ;
assume I is_halting_on s1 ; :: thesis: ( I is_closed_on s2 & I is_halting_on s2 )
then ProgramPart ((Initialize s1) +* (stop I)) halts_on (Initialize s1) +* (stop I) by Def3;
then consider m being Element of NAT such that
A18: CurInstr (ProgramPart ((Initialize s1) +* (stop I))),(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),m) = halt SCMPDS by AMI_1:146;
Y: (ProgramPart (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 )) /. (IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 )) = (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 ) . (IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 )) by COMPOS_1:38;
Z: (ProgramPart (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 )) /. (IC (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 )) = (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 ) . (IC (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 )) by COMPOS_1:38;
A19: IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 ) = IC (Initialize (stop I)) by A16, A1, I1, FUNCT_4:14
.= 0 by COMPOS_1:def 16 ;
then CurInstr (ProgramPart ((Initialize s1) +* (stop I))),(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 ) = (Initialize (stop I)) . 0 by A1, A6, A4, Y, I1, FUNCT_4:14
.= CurInstr (ProgramPart ((Initialize s2) +* (stop I))),(Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 ) by A2, A17, A6, A4, Z, I2, FUNCT_4:14 ;
then A20: S₁[ 0 ] by A19, A17, A3, SCMPDS_4:24;

now

let k be Element of NAT ; :: thesis: IC (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) in dom (stop I)
A21: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A20, A8);
IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k) in dom (stop I) by A7, Def2;
hence IC (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (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 S₁[k] from NAT_1:sch 1(A20, A8);
then CurInstr (ProgramPart ((Initialize s2) +* (stop I))),(Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),m) = halt SCMPDS by A18;
then ProgramPart ((Initialize s2) +* (stop I)) halts_on (Initialize s2) +* (stop I) by AMI_1:146;
hence I is_halting_on s2 by Def3; :: thesis: verum