let s1, s2 be State of SCMPDS ; :: thesis: for I being Program of SCMPDS st DataPart s1 = DataPart s2 & I is_closed_on s1 holds
I is_closed_on s2
let I be Program of SCMPDS ; :: thesis: ( DataPart s1 = DataPart s2 & I is_closed_on s1 implies I is_closed_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;
assume A1: DataPart s1 = DataPart s2 ; :: thesis: ( not I is_closed_on s1 or I is_closed_on s2 )
A2: Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 = (Initialize s2) +* (stop I) by AMI_1:13;
A3: Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 = (Initialize s1) +* (stop I) by AMI_1:13;
then A4: DataPart (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 ) = DataPart s1 by Th9
.= DataPart (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 ) by A1, A2, Th9 ;
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 (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),$1)),(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),$1) = CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),$1)),(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) );
A5: 0 in dom (stop I) by SCMPDS_4:75;
A6: stop I c= Initialize (stop I) by SCMPDS_4:9;
then A7: dom (stop I) c= dom (Initialize (stop I)) by GRFUNC_1:8;
assume A8: I is_closed_on s1 ; :: thesis: I is_closed_on s2

A9: 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;
A10: 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 A11: S₁[k] ; :: thesis: S₁[k + 1]
then A12: 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;
Initialize (stop I) c= (Initialize s2) +* (stop I) by I2, FUNCT_4:26;
then stop I c= (Initialize s2) +* (stop I) by A6, XBOOLE_1:1;
then A13: stop I c= Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1) by AMI_1:81;
A14: IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1)) in dom (stop I) by A8, Def2;
T: ProgramPart ((Initialize s1) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k) by AMI_1:123;
A15: 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 (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k)),(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k)),(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k) by T ;
then A16: Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1), Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1) equal_outside NAT by A11, A12, A10, SCMPDS_4:11, SCMPDS_4:15;
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 A11, A12, SCMPDS_4:11;
then A17: 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 A11, A15, A10, 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;
Initialize (stop I) c= (Initialize s1) +* (stop I) by I1, FUNCT_4:26;
then stop I c= (Initialize s1) +* (stop I) by A6, 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 (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),(k + 1))),(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 A14, Y, GRFUNC_1:8
.= CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1))),(Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),(k + 1)) by A13, A17, A14, Z, GRFUNC_1:8 ;
hence S₁[k + 1] by A16, COMPOS_1:24, SCMPDS_4:24; :: thesis: verum

end;

A18: IC SCMPDS in dom (Initialize (stop I)) by COMPOS_1:def 16;
then A19: 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 ;
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;
A20: IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 ) = IC (Initialize (stop I)) by A18, A3, I1, FUNCT_4:14
.= 0 by COMPOS_1:def 16 ;
then CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 )),(Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),0 ) = (Initialize (stop I)) . 0 by A3, A7, A5, Y, I1, FUNCT_4:14
.= CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 )),(Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),0 ) by A2, A19, A7, A5, Z, I2, FUNCT_4:14 ;
then A21: S₁[ 0 ] by A20, A19, A4;

now

let k be Element of NAT ; :: thesis: IC (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) in dom (stop I)
A22: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A21, A9);
IC (Comput (ProgramPart ((Initialize s1) +* (stop I))),((Initialize s1) +* (stop I)),k) in dom (stop I) by A8, Def2;
hence IC (Comput (ProgramPart ((Initialize s2) +* (stop I))),((Initialize s2) +* (stop I)),k) in dom (stop I) by A22; :: thesis: verum

end;

hence I is_closed_on s2 by Def2; :: thesis: verum