proposition: Lemma wf_cnf_list : forall (m : hmap) l ar acc b1 b2 cp cm m' ar' w (H : forall x : t LForm, In x l -> forall (b1 b2 : bool) (cp cm : IntMap.ptrie unit) (ar : list literal) (acc : list watched_clause) (hf : HFormula) (m' : IntMap.ptrie unit * IntMap.ptrie unit) (ar' : list literal) (w : list watched_clause), Forall (has_literal m) ar -> Forall (has_watched_clause m) acc -> has_form m hf -> elt hf = elt x -> cnf b1 b2 cp cm ar acc (elt x) hf = (m', ar', w) -> Forall (has_literal m) ar' /\ Forall (has_watched_clause m) w) (HA : Forall (has_literal m) ar) (ACC : Forall (has_watched_clause m) acc) (HF : Forall (has_form m) l) (EQ : cnf_list cnf b1 b2 cp cm ar acc l = (m', ar', w)), (Forall (has_literal m) ar' /\ Forall (has_watched_clause m) w).
proof: Proof. induction l; simpl. - intros. destruct b1; inv EQ. + split ; auto. + split ; auto. - intros. destruct (cnf b1 b2 cp cm ar acc (elt a) a) as (((cp',cm'),ar2),acc') eqn:EQ1. revert EQ. apply H in EQ1;auto. destruct EQ1. apply IHl; auto. intros x IN. apply H; tauto. inv HF; auto. inv HF; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause