proposition: Lemma eval_insert_watched_clause : forall diff i cl st (WF : wf_state st) (WFC : Annot.lift (has_watched_clause (hconsmap st)) cl) (CA : ohold (Annot.lift (has_literal (hconsmap st))) diff) (ED : ohold (Annot.lift eval_literal) diff) (ES : eval_state st) (EW : Annot.lift eval_watched_clause cl) , eval_result_state (insert_watched_clause diff i cl st).
proof: Proof. unfold insert_watched_clause. intros. unfold insert_normalised_clause. generalize (normalise_watched_clause_correct diff (hconsmap st) (units st) (Annot.elt cl) (Annot.deps cl) (wf_hm st WF) (ev_units st ES) CA ED WFC EW). destruct (normalise_watched_clause diff (units st) (Annot.deps cl) (Annot.elt cl));simpl;auto. destruct elt0 ; simpl ; auto. unfold Annot.lift, Annot.set. simpl. intros. apply eval_insert_unit; auto. intros. apply eval_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