let s1, s2 be State of ; :: thesis: for I being Program of st DataPart s1 = DataPart s2 & I is_closed_on s1 holds
I is_closed_on s2
let I be Program of ; :: 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: Computation (s2 +* (Initialized (stop I))),0 = s2 +* (Initialized (stop I)) by AMI_1:13;
A3: Computation (s1 +* (Initialized (stop I))),0 = s1 +* (Initialized (stop I)) by AMI_1:13;
then A4: DataPart (Computation (s1 +* (Initialized (stop I))),0 ) = DataPart s1 by Th9
.= DataPart (Computation (s2 +* (Initialized (stop I))),0 ) by A1, A2, Th9 ;
defpred S₁[ Element of NAT ] means ( IC (Computation (s1 +* (Initialized (stop I))),$1) = IC (Computation (s2 +* (Initialized (stop I))),$1) & CurInstr (Computation (s1 +* (Initialized (stop I))),$1) = CurInstr (Computation (s2 +* (Initialized (stop I))),$1) & DataPart (Computation (s1 +* (Initialized (stop I))),$1) = DataPart (Computation (s2 +* (Initialized (stop I))),$1) );
A5: inspos 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] )
A10: Computation (s2 +* (Initialized (stop I))),(k + 1) = Following (Computation (s2 +* (Initialized (stop I))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s2 +* (Initialized (stop I))),k)),(Computation (s2 +* (Initialized (stop I))),k) ;
assume A11: S₁[k] ; :: thesis: S₁[k + 1]
then A12: for a being Int_position holds (Computation (s1 +* (Initialized (stop I))),k) . a = (Computation (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= Computation (s2 +* (Initialized (stop I))),(k + 1) by AMI_1:81;
A14: IC (Computation (s1 +* (Initialized (stop I))),(k + 1)) in dom (stop I) by A8, Def2;
A15: Computation (s1 +* (Initialized (stop I))),(k + 1) = Following (Computation (s1 +* (Initialized (stop I))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s1 +* (Initialized (stop I))),k)),(Computation (s1 +* (Initialized (stop I))),k) ;
then A16: Computation (s1 +* (Initialized (stop I))),(k + 1), Computation (s2 +* (Initialized (stop I))),(k + 1) equal_outside NAT by A11, A12, A10, SCMPDS_4:11, SCMPDS_4:15;
Computation (s1 +* (Initialized (stop I))),k, Computation (s2 +* (Initialized (stop I))),k equal_outside NAT by A11, A12, SCMPDS_4:11;
then A17: IC (Computation (s1 +* (Initialized (stop I))),(k + 1)) = IC (Computation (s2 +* (Initialized (stop I))),(k + 1)) by A11, A15, A10, AMI_1:121, SCMPDS_4:15;
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= Computation (s1 +* (Initialized (stop I))),(k + 1) by AMI_1:81;
then CurInstr (Computation (s1 +* (Initialized (stop I))),(k + 1)) = (stop I) . (IC (Computation (s1 +* (Initialized (stop I))),(k + 1))) by A14, GRFUNC_1:8
.= CurInstr (Computation (s2 +* (Initialized (stop I))),(k + 1)) by A13, A17, A14, GRFUNC_1:8 ;
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 (Computation (s2 +* (Initialized (stop I))),0 ) = (Initialized (stop I)) . (IC SCMPDS ) by A2, FUNCT_4:14
.= inspos 0 by SCMPDS_4:29 ;
A20: IC (Computation (s1 +* (Initialized (stop I))),0 ) = (Initialized (stop I)) . (IC SCMPDS ) by A18, A3, FUNCT_4:14
.= inspos 0 by SCMPDS_4:29 ;
then CurInstr (Computation (s1 +* (Initialized (stop I))),0 ) = (Initialized (stop I)) . (inspos 0 ) by A3, A7, A5, FUNCT_4:14
.= CurInstr (Computation (s2 +* (Initialized (stop I))),0 ) by A2, A19, A7, A5, FUNCT_4:14 ;
then A21: S₁[ 0 ] by A20, A19, A4;

now

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

end;

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