let s1, s2 be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_closed_on s1 holds
I is_closed_on s2
let I be Program of SCM+FSA ; :: thesis: ( DataPart s1 = DataPart s2 & I is_closed_on s1 implies I is_closed_on s2 )
set S1 = s1 +* (I +* (Start-At (insloc 0 )));
set S2 = s2 +* (I +* (Start-At (insloc 0 )));
assume A1: DataPart s1 = DataPart s2 ; :: thesis: ( not I is_closed_on s1 or I is_closed_on s2 )
A2: Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 = s2 +* (I +* (Start-At (insloc 0 ))) by AMI_1:13;
A3: Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 = s1 +* (I +* (Start-At (insloc 0 ))) by AMI_1:13;
then A4: DataPart (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = DataPart s1 by SCMFSA8A:11
.= DataPart (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) by A1, A2, SCMFSA8A:11 ;
assume A5: I is_closed_on s1 ; :: thesis: I is_closed_on s2
then A6: insloc 0 in dom I by Th3;
defpred S₁[ Element of NAT ] means ( IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) & DataPart (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = DataPart (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) );
A7: I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A8: dom I c= dom (I +* (Start-At (insloc 0 ))) by GRFUNC_1:8;

A9: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A10: Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1) = Following (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k)),(Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ;
assume A11: S₁[k] ; :: thesis: S₁[k + 1]
then A12: for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f by SCMFSA6A:38;
for a being Int-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . a = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . a by A11, SCMFSA6A:38;
then A13: Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT by A11, A12, SCMFSA6A:28;
I +* (Start-At (insloc 0 )) c= s2 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then I c= s2 +* (I +* (Start-At (insloc 0 ))) by A7, XBOOLE_1:1;
then A14: I c= Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1) by AMI_1:81;
A15: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) in dom I by A5, SCMFSA7B:def 7;
A16: Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1) = Following (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)),(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) ;
then A17: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A11, A13, A10, AMI_1:121, SCMFSA6A:32;
I +* (Start-At (insloc 0 )) c= s1 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then I c= s1 +* (I +* (Start-At (insloc 0 ))) by A7, XBOOLE_1:1;
then I c= Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1) by AMI_1:81;
then CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = I . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1))) by A15, GRFUNC_1:8
.= CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A14, A17, A15, GRFUNC_1:8 ;
hence S₁[k + 1] by A11, A13, A16, A10, A17, SCMFSA6A:32, SCMFSA6A:39; :: thesis: verum

end;

A18: IC SCM+FSA in dom (I +* (Start-At (insloc 0 ))) by SF_MASTR:65;
then A19: IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A2, FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
A20: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A18, A3, FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
then CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (insloc 0 ) by A3, A8, A6, FUNCT_4:14
.= CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) by A2, A19, A8, A6, FUNCT_4:14 ;
then A21: S₁[ 0 ] by A20, A19, A4;

now

let k be Element of NAT ; :: thesis: IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I
A22: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A5, SCMFSA7B:def 7;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A21, A9);
hence IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A22; :: thesis: verum

end;

hence I is_closed_on s2 by SCMFSA7B:def 7; :: thesis: verum