proposition: Lemma wf_update_watched_clause : forall diff i cl st (WF: wf_result_state st) (WFD : Annot.lift_deps (wf_pset (hconsmap_result st)) diff) (WFA : Annot.lift_deps (wf_pset (hconsmap_result st)) cl) (HAS : Annot.lift (has_watched_clause (hconsmap_result st)) cl), wf_result_state (update_watched_clause diff i cl st ).
proof: Proof. intros. destruct st ; simpl in * ; auto. unfold insert_watched_clause. apply wf_insert_normalised_clause; auto. - apply check_annot_normalise_watched_clause. + unfold remove_watched_clause; simpl. destruct WF ; auto. + unfold remove_watched_clause ; simpl. auto. + rewrite hconsmap_remove_watched_clause; simpl;auto. + rewrite hconsmap_remove_watched_clause; simpl;auto. - apply wf_remove_watched_clause;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause