proposition: Lemma oplus_unary_sec_intersection: forall (X:Type) (p:WFT X) (q:WFT X) (C : X -> X -> Prop) (A : X -> Prop) (B : X -> Prop), SecureBy (fun y z => C y z \/ A y) p -> SecureBy (fun y z => C y z \/ B y) q -> SecureBy (fun y z => C y z \/ (A y /\ B y)) (oplus_unary p q).
proof: Proof. intros X p. induction p. simpl. intros. eapply sec_strengthen. 2: apply H0. intros. simpl in H1. destruct (H x y). left. apply H2. destruct H1. left. apply H1. right. split. apply H2. apply H1. intro q. induction q. intros. simpl. simpl in H1. intro x. simpl in H0. remember (H0 x). eapply sec_strengthen. 2: apply s. intros. simpl in H2. destruct H2. destruct H2. destruct (H1 x y). left. left. apply H2. left. left. apply H2. destruct (H1 x0 y). left. left. apply H3. left. right. split. apply H2. apply H3. destruct (H1 x x0). right. left. apply H3. destruct H2. right. left. apply H2. right. right. auto. intros. rewrite oplus_unary_sup_sup. rewrite sup_rewrite. intro x. assert (SecureBy (fun y z => (C y z \/ C x y \/ A y /\ B y) \/ (A x /\ B x)) (oplus_nullary (oplus_unary (w x) (SUP w0)) (oplus_unary (SUP w) (w0 x)))). apply oplus_nullary_sec_intersection. simpl in H1. remember (H1 x) as G1. clear HeqG1. clear H1. remember (@H x (SUP w0) C (fun y => C x y \/ A y \/ A x) B). eapply sec_strengthen. 2: { apply s. eapply sec_strengthen. 2: eapply G1. intros. simpl in H1. destruct H1. destruct H1. left; apply H1. right; right; left; apply H1. destruct H1. right; left; apply H1. right; right; right; apply H1. apply H2. } intros. destruct H1. left; left; auto. destruct H1. destruct H1. left; right; left; auto. destruct H1. left; right; right; auto. right; auto. simpl in H2. remember (H2 x) as G2. clear HeqG2. remember (@H0 x C A (fun y => C x y \/ B y \/ B x)). eapply sec_strengthen. 2: { apply s. eapply sec_strengthen. 2: apply H1. intros. simpl in H3. auto. eapply sec_strengthen. 2: eapply G2. intros. simpl in H3. destruct H3. destruct H3. left. apply H3. right. right. left. apply H3. destruct H3. right. left. apply H3. right. right. right. apply H3. } 2: { eapply sec_strengthen. 2: apply H3. intros. simpl in H4. destruct H4. destruct H4. left. left. apply H4. destruct H4. right. left. apply H4. left. right. apply H4. right. right. apply H4. } intros. destruct H3. left; left; auto. destruct H3; destruct H4. left; right; left; auto. destruct H4. left; right; right; auto. right; auto. Qed.
imports: Coq(Lia) AlmostFull.Default(AlmostFull)