proposition: Lemma oplus_binary_sec_intersection : forall (X:Type) (p : WFT X) (q : WFT X) (A : X -> X -> Prop) (B : X -> X -> Prop), SecureBy A p -> SecureBy B q -> SecureBy (fun x y => A x y /\ B x y) (oplus_binary p q).
proof: Proof. intros X p. induction p. intros. simpl in H. simpl. eapply sec_strengthen. intros. split. apply H. apply H1. apply H0. intro q. induction q. intros. simpl in H0. simpl in H1. simpl. intros. eapply sec_strengthen. 2: apply H0. intros. simpl in H2. destruct H2. left. split. apply H2. apply H1. right. split. apply H2. apply H1. intros. rewrite oplus_binary_sup_sup. rewrite sup_rewrite. intro x. remember H1 as G1. clear HeqG1. simpl in G1. remember (@H _ _ _ _ (G1 x) H2) as IHp. clear HeqIHp. remember H2 as G2. clear HeqG2. simpl in G2. remember (@H0 _ _ _ H1 (G2 x)) as IHq. clear HeqIHq. clear H0. simpl in IHp. assert (SecureBy (fun x0 y : X => A x0 y /\ B x0 y \/ B x x0) (oplus_binary (SUP w) (w0 x))) as IHqSimpler. eapply sec_strengthen. 2: apply IHq. intros. simpl in H0. firstorder. clear IHq. clear G1. clear G2. clear H1. clear H. clear H2. eapply oplus_unary_sec_intersection. eapply sec_strengthen. 2: apply IHp. intros. simpl in H. destruct H. destruct H. left. auto. right. auto. eapply sec_strengthen. 2: eapply IHqSimpler. intros. simpl in H. destruct H. left. auto. right. auto. Defined.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)