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 EXTPRO_1:3;
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 EXTPRO_1:3;
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 S1[ 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: ( S1[k] implies S1[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 EXTPRO_1:4
.= 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: S1[k] ; :: thesis: S1[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 EXTPRO_1:4
.= 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 S1[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 COMPOS_1:141;
then A19: IC (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),0)) = IC (I +* (Start-At (0,SCM+FSA))) by A2, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
A20: IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),0)) = IC (I +* (Start-At (0,SCM+FSA))) by A18, A3, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
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: S1[ 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 S1[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