proposition: Lemma eval_annot_insert_watched_clause : forall diff i cl st (WF : wf_state st) (WFC : check_annot has_watched_clause (hconsmap st) cl) (ED : ohold (eval_annot eval_literal (hconsmap st)) diff) (CD : ohold (check_annot has_literal (hconsmap st)) diff) (ES : eval_annot_state st) (EW : eval_annot eval_watched_clause (hconsmap st) cl) , eval_annot_result_state (insert_watched_clause diff i cl st).
proof: Proof. unfold insert_watched_clause. intros. unfold insert_normalised_clause. generalize (eval_annot_normalise_watched_clause diff (hconsmap st) (units st) (Annot.elt cl) (Annot.deps cl) (wf_hm st WF) (wf_units st WF) (wf_deps _ _ _ WFC) (ev_an_units st ES) ED CD (wf_elt _ _ _ WFC) EW ). destruct (normalise_watched_clause diff (units st) (Annot.deps cl) (Annot.elt cl));simpl;auto. destruct elt0 ; simpl ; auto. - intro. apply eval_annot_insert_unit; auto. - intros. apply eval_annot_add_watched_clause; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause