proposition: Lemma eval_annot_make_clause : forall m u cl an (EV: eval_annot_units u m) (WFU: wf_units_lit u m) (HL: Forall (has_literal m) cl) (WF: wf_pset m an) (EC: eval_pset m an -> eval_literal_list cl), eval_annot eval_clause m (make_clause u an cl).
proof: Proof. unfold has_conflict_clause. induction cl; simpl; auto. intros. destruct (find_lit a u) eqn:FD. - inv HL. assert (FD':=FD). apply eval_annot_units_find_lit with (m:=m) in FD; auto. apply check_annot_find_lit with (hm:=m) in FD'; auto. unfold eval_annot, Annot.map in FD. simpl in FD. destruct (Annot.elt t0) ; simpl ; auto. + apply eval_annot_TRUE. + apply IHcl ; auto. apply wf_pset_union;auto. intros. apply eval_pset_union in H; auto. destruct H. intuition. eapply eval_neg_literal_rec; eauto. destruct FD' ; auto. destruct WF;auto. - inv HL. eapply eval_annot_reduce ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause