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 IsI = Initialized (stop I);
set S1 = s1 +* (Initialized (stop I));
set S2 = s2 +* (Initialized (stop I));
assume A1: DataPart s1 = DataPart s2 ; :: thesis: ( not I is_closed_on s1 or I is_closed_on s2 )
A2: Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),0 = s2 +* (Initialized (stop I)) by AMI_1:13;
A3: Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 = s1 +* (Initialized (stop I)) by AMI_1:13;
then A4: DataPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 ) = DataPart s1 by Th9
.= DataPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),0 ) by A1, A2, Th9 ;
defpred S₁[ 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) );
A5: 0 in dom (stop I) by SCMPDS_4:75;
A6: stop I c= Initialized (stop I) by SCMPDS_4:9;
then A7: dom (stop I) c= dom (Initialized (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 (s2 +* (Initialized (stop I))) = ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) by AMI_1:144;
A10: 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 A11: S₁[k] ; :: thesis: S₁[k + 1]
then A12: 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;
Initialized (stop I) c= s2 +* (Initialized (stop I)) by FUNCT_4:26;
then stop I c= s2 +* (Initialized (stop I)) by A6, XBOOLE_1:1;
then A13: stop I c= Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(k + 1) by AMI_1:81;
A14: IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1)) in dom (stop I) by A8, Def2;
T: ProgramPart (s1 +* (Initialized (stop I))) = ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) by AMI_1:144;
A15: 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 A16: Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),(k + 1), Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),(k + 1) equal_outside NAT by A11, A12, A10, SCMPDS_4:11, SCMPDS_4:15;
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 A11, A12, SCMPDS_4:11;
then A17: 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 A11, A15, A10, 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 A6, 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 A14, 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 A13, A17, A14, GRFUNC_1:8, Z ;
hence S₁[k + 1] by A16, AMI_1:121, SCMPDS_4:24; :: thesis: verum

end;

A18: IC SCMPDS in dom (Initialized (stop I)) by SCMPDS_4:7;
then A19: 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 ;
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;
A20: IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),0 ) = (Initialized (stop I)) . (IC SCMPDS ) by A18, A3, 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 A3, A7, A5, 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, A19, A7, A5, FUNCT_4:14, Z ;
then A21: S₁[ 0 ] by A20, A19, A4;

now

let k be Element of NAT ; :: thesis: IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (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 (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) in dom (stop I) by A8, Def2;
hence IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) in dom (stop I) by A22; :: thesis: verum

end;

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