proposition: Lemma eval_annot_normalise_watched_clause : forall diff m u cl an (WFM : wf m) (WF : wf_units_lit u m) (WFA: wf_pset m an) (EV : eval_annot_units u m) (EA : ohold (eval_annot eval_literal m) diff) (CA : ohold (check_annot has_literal m) diff) (WFC : has_watched_clause m cl) (EC : eval_pset m an -> eval_watched_clause cl), eval_annot eval_clause m (normalise_watched_clause diff u an cl).
proof: Proof. unfold normalise_watched_clause. intros. destruct diff. - apply eval_annot_shorten_clause;auto. - apply eval_annot_reduce_lits with (u:=u) in EC; auto. apply has_reduce_lits with (an:=an)(u:=u) in WFC; auto. destruct_in_goal R; auto. unfold eval_annot. simpl. intro. eapply no_dup_clause_correct with (hm:=m) ; eauto. apply eval_annot_TRUE. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause