let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 holds
I is_closed_on s2,P2
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,P1 holds
I is_closed_on s2,P2
let I be Program of SCM+FSA; :: thesis: ( DataPart s1 = DataPart s2 & I is_closed_on s1,P1 implies I is_closed_on s2,P2 )
set S1 = s1 +* (Initialize I);
set S2 = s2 +* (Initialize I);
A1: ProgramPart I = I by RELAT_1:209;
assume A2: DataPart s1 = DataPart s2 ; :: thesis: ( not I is_closed_on s1,P1 or I is_closed_on s2,P2 )
A3: Comput ((P2 +* I),(s2 +* (Initialize I)),0) = s2 +* (Initialize I) by EXTPRO_1:3;
A4: Comput ((P1 +* I),(s1 +* (Initialize I)),0) = s1 +* (Initialize I) by EXTPRO_1:3;
then A5: DataPart (Comput ((P1 +* I),(s1 +* (Initialize I)),0)) = DataPart s1 by SCMFSA8A:11
.= DataPart (Comput ((P2 +* I),(s2 +* (Initialize I)),0)) by A2, A3, SCMFSA8A:11 ;
assume A6: I is_closed_on s1,P1 ; :: thesis: I is_closed_on s2,P2
then A7: 0 in dom I by Th3;
defpred S₁[ Nat] means ( IC (Comput ((P1 +* I),(s1 +* (Initialize I)),$1)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),$1)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),$1))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),$1))) & DataPart (Comput ((P1 +* I),(s1 +* (Initialize I)),$1)) = DataPart (Comput ((P2 +* I),(s2 +* (Initialize I)),$1)) );

A8: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A9: Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)) = Following ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k)))),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) ;
assume A10: S₁[k] ; :: thesis: S₁[k + 1]
then A11: for f being FinSeq-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . f = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . f by SCMFSA6A:38;
for a being Int-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . a = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . a by A10, SCMFSA6A:38;
then A12: Comput ((P1 +* I),(s1 +* (Initialize I)),k), Comput ((P2 +* I),(s2 +* (Initialize I)),k) equal_outside NAT by A10, A11, SCMFSA10:91;
A13: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1))) in dom I by A6, SCMFSA7B:def 7, A1;
Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)) = Following ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k)))),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) ;
then A14: Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)), Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)) equal_outside NAT by A10, A12, A9, AMISTD_2:def 20;
A15: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1))) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1))) by COMPOS_1:24, A14;
A16: (P1 +* I) /. (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) = (P1 +* I) . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) by PBOOLE:158;
A17: (P2 +* I) /. (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)))) = (P2 +* I) . (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)))) by PBOOLE:158;
A18: I c= P1 +* I by FUNCT_4:26;
A19: I c= P2 +* I by FUNCT_4:26;
CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) = I . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) by A13, A16, GRFUNC_1:8, A18
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)))) by A15, A13, A17, GRFUNC_1:8, A19 ;
hence S₁[k + 1] by COMPOS_1:24, COMPOS_1:138, A14; :: thesis: verum

end;

A20: (P1 +* I) /. (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),0))) = (P1 +* I) . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),0))) by PBOOLE:158;
A21: (P2 +* I) /. (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),0))) = (P2 +* I) . (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),0))) by PBOOLE:158;
A22: IC in dom (Initialize I) by COMPOS_1:141;
then A23: IC (Comput ((P2 +* I),(s2 +* (Initialize I)),0)) = IC (Initialize I) by A3, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
A24: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),0)) = IC (Initialize I) by A22, A4, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),0))) = I . 0 by A7, A20, FUNCT_4:14
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),0))) by A23, A7, A21, FUNCT_4:14 ;
then A25: S₁[ 0 ] by A24, A23, A5;

now

let k be Element of NAT ; :: thesis: IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) in dom I
A26: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) in dom I by A6, SCMFSA7B:def 7, A1;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A25, A8);
hence IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) in dom I by A26; :: thesis: verum

end;

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