proposition: Lemma eval_insert_fresh_watched_clause : forall cl st (WF : wf_state st) (ES : eval_state st) (EC : eval_watched_clause cl) (HS : has_watched_clause (hconsmap st) cl) , eval_result_state (insert_fresh_watched_clause cl st).
proof: Proof. unfold insert_fresh_watched_clause. intros. destruct (get_fresh_clause_id st) eqn:EQ. change s with (snd (i,s)). rewrite <- EQ. unfold insert_watched_clause. apply eval_insert_normalised_clause;auto. unfold Annot.deps. unfold Annot.elt. rewrite hconsmap_get_fresh_clause_id. - destruct WF. apply check_annot_normalise_watched_clause;simpl; auto. apply wf_pset_empty. - apply wf_get_fresh_clause_id;auto. - apply eval_get_fresh_clause; auto. - unfold Annot.deps. unfold Annot.elt. destruct WF, ES. eapply normalise_watched_clause_correct; eauto. simpl; auto. simpl;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause