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 )
assume A2: I is_closed_on s1 ; :: thesis: I is_closed_on s2
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) );
A3: IC SCM+FSA in dom (I +* (Start-At (insloc 0 ))) by SF_MASTR:65;
A4: ( Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 = s1 +* (I +* (Start-At (insloc 0 ))) & Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 = s2 +* (I +* (Start-At (insloc 0 ))) ) by AMI_1:13;
then A5: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A3, FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
A6: IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A3, A4, FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
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: insloc 0 in dom I by A2, Th3;
then A10: CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (insloc 0 ) by A4, A5, A8, FUNCT_4:14
.= CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) by A4, A6, A8, A9, FUNCT_4:14 ;
DataPart (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = DataPart s1 by A4, SCMFSA8A:11
.= DataPart (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) by A1, A4, SCMFSA8A:11 ;
then A11: S₁[ 0 ] by A5, A6, A10;

A12: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A13: S₁[k] ; :: thesis: S₁[k + 1]
then ( ( for a being Int-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . a = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . a ) & ( 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;
then A14: Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT by A13, SCMFSA6A:28;
( I +* (Start-At (insloc 0 )) c= s1 +* (I +* (Start-At (insloc 0 ))) & I +* (Start-At (insloc 0 )) c= s2 +* (I +* (Start-At (insloc 0 ))) ) by FUNCT_4:26;
then ( I c= s1 +* (I +* (Start-At (insloc 0 ))) & I c= s2 +* (I +* (Start-At (insloc 0 ))) ) by A7, XBOOLE_1:1;
then A15: ( I c= Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1) & I c= Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1) ) by AMI_1:81;
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) ;
thus S₁[k + 1] :: thesis: verum

proof

A17: 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) ;
hence A18: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A13, A14, A16, AMI_1:121, SCMFSA6A:32; :: thesis: ( CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) & DataPart (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = DataPart (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) )
A19: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) in dom I by A2, SCMFSA7B:def 7;
hence 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 A15, A18, A19, GRFUNC_1:8 ;
:: thesis: DataPart (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = DataPart (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1))
thus DataPart (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = DataPart (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A13, A14, A16, A17, SCMFSA6A:32, SCMFSA6A:39; :: thesis: verum

end;

end;

now

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

end;

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