proposition: Lemma wf_cnf : forall m f b1 b2 cp cm ar acc hf m' ar' w (HA : Forall (has_literal m) ar) (ACC: Forall (has_watched_clause m) acc) (HF : has_form m hf) (HFF: hf.(elt) = f) (EQ : cnf b1 b2 cp cm ar acc f hf = (m',ar',w)), Forall (has_literal m) ar' /\ Forall (has_watched_clause m) w.
proof: Proof. induction f using form_ind; simpl ; intros. - destruct (is_cons (id hf) (if b1 then cp else cm)). + inv EQ. split; auto. + inv EQ. split ; auto. - destruct (is_cons (id hf) (if b1 then cp else cm)). + inv EQ. split; auto. + revert EQ. assert (HFL : Forall (has_form m) l). { inv HF; try discriminate. simpl in *; auto. congruence. } apply wf_cnf_list; auto. destruct b1. apply wf_cnf_of_op_plus;auto. apply wf_cnf_of_op_minus;auto. - destruct (is_cons (id hf) (if b1 then cp else cm)). + inv EQ. split; auto. + destruct (cnf_list cnf (negb b1) b2 cp cm (if negb (lazy_or b2 (fun _ : unit => forallb is_dec l)) && b1 then POS hf :: ar else ar) ((if b1 then cnf_plus_impl b2 else cnf_minus_impl) l r hf acc) l) as (((cp1,cm1),ar1),acc1) eqn:ACC1. revert EQ. assert (HF' : Forall (has_form m) l). { inv HF; try discriminate. simpl in HFF. congruence. } assert (HR : has_form m r). { inv HF; try discriminate. simpl in HFF. congruence. } apply wf_cnf_list with (m:=m) in ACC1;auto. apply IHf;auto. tauto. tauto. destruct (negb (lazy_or b2 (fun _ : unit => forallb is_dec l)) && b1); auto. destruct b1. apply wf_cnf_plus_impl;auto. apply wf_cnf_minus_impl;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause