proposition: Lemma wf_augment_cnf : forall b l st (HL : has_literal (hconsmap st) l) (WF : wf_state st), wf_result_state (augment_cnf b l st).
proof: Proof. unfold augment_cnf. intros. destruct (cnf_of_literal l b (fst (defs st)) (snd (defs st)) (arrows st) nil (elt (form_of_literal l)) (form_of_literal l)) as (((cp,cm),ar),acc) eqn:EQ. apply wf_cnf_of_literal with (m:=hconsmap st) in EQ; auto. { apply fold_update_correct with (Q:= fun st cl => has_watched_clause (hconsmap st) cl). - intros. revert H0. apply has_watched_clause_mono. generalize (hconsmap_insert_fresh_watched_clause a st0). unfold hconsmap_progress. rewrite H. simpl. intuition congruence. - intros. apply wf_insert_fresh_watched_clause; auto. - destruct EQ. revert H0. apply Forall_Forall. intros. unfold insert_defs; simpl; auto. - apply wf_insert_defs;auto. tauto. } destruct WF; auto. apply has_form_of_literal; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause