proposition: Lemma eval_annot_shorten_clause : forall diff m u cl an (WF : wf_units_lit u m) (WFA: wf_pset m an) (EV : eval_annot_units u m) (WFC : has_watched_clause m cl) (WD: check_annot has_literal m diff) (ED : eval_annot eval_literal m diff) (EC : eval_pset m an -> eval_watched_clause cl), eval_annot eval_clause m (shorten_clause diff u an cl).
proof: Proof. unfold shorten_clause;intros. assert (HW1 : has_literal m (watch1 cl)). { inv WFC. auto. } assert (HW2 : has_literal m (watch2 cl)). { inv WFC. inv H2; auto. } assert (HUW : Forall (has_literal m) (unwatched cl)). { inv WFC. inv H2; auto. } destruct_in_goal OPP. - apply eval_annot_reduce with (m:=m); auto. apply wf_pset_union; auto. destruct WD;auto. intro U. apply eval_pset_union in U as (U1 & U2);auto. unfold eval_annot in ED. specialize (EC U2). apply eval_neg_literal_rec in EC; auto. apply eval_opp_literal with (m:=m) in OPP;auto. destruct WD;auto. destruct WD;auto. apply wf_deps0. apply WFA. - destruct_in_goal OPP1. apply eval_annot_reduce with (m:=m); auto. apply wf_pset_union; auto. destruct WD;auto. intro U. apply eval_pset_union in U as (U1 & U2);auto. unfold eval_annot in ED. specialize (EC U2). apply eval_literal_rec_swap in EC; auto. apply eval_opp_literal with (m:=m) in OPP1;auto. destruct WD;auto. destruct WD;auto. apply wf_deps0. apply WFA. 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