proposition: Lemma normalise_watched_clause_correct : forall diff m u cl an (WF: wf m) (EV : eval_units m u) (HL : ohold (Annot.lift (has_literal m)) diff) (EL : ohold (Annot.lift eval_literal) diff) (WFC : has_watched_clause m cl) (EC : eval_watched_clause cl), Annot.lift eval_clause (normalise_watched_clause diff u an cl).
proof: Proof. unfold normalise_watched_clause. intros. destruct diff. - simpl in HL. eapply shorten_clause_correct;eauto. - eapply eval_reduce_lits with (an:=an) in EC; eauto. eapply has_reduce_lits with (an:=an) (u:=u) in WFC; eauto. destruct ((reduce_lits u an (watch1 cl :: watch2 cl :: unwatched cl))) eqn:EQ. + unfold Annot.lift. simpl. eapply no_dup_clause_correct with (hm:=m); eauto. + exact I. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause