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 0 ,SCM+FSA ));
set S2 = s2 +* (I +* (Start-At 0 ,SCM+FSA ));
assume A1: DataPart s1 = DataPart s2 ; :: thesis: ( not I is_closed_on s1 or I is_closed_on s2 )
A2: Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),0 = s2 +* (I +* (Start-At 0 ,SCM+FSA )) by AMI_1:13;
A3: Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),0 = s1 +* (I +* (Start-At 0 ,SCM+FSA )) by AMI_1:13;
then A4: DataPart (Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),0 ) = DataPart s1 by SCMFSA8A:11
.= DataPart (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),0 ) by A1, A2, SCMFSA8A:11 ;
assume A5: I is_closed_on s1 ; :: thesis: I is_closed_on s2
then A6: 0 in dom I by Th3;
defpred S₁[ Nat] means ( IC (Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),$1) = IC (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),$1) & CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),$1)),(Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),$1) = CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),$1)),(Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),$1) & DataPart (Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),$1) = DataPart (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),$1) );
A7: I c= I +* (Start-At 0 ,SCM+FSA ) by SCMFSA8A:9;
then A8: dom I c= dom (I +* (Start-At 0 ,SCM+FSA )) by GRFUNC_1:8;

A9: now

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

end;

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

now

let k be Element of NAT ; :: thesis: IC (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I
A22: IC (Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),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 (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I by A22; :: thesis: verum

end;

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