proposition: Lemma cnf_of_op_minus_correct : forall acc g o l hf (EQ : hf.(elt) = LOP o l) (ACC : (Forall eval_watched_clause acc -> eval_ohformula g) -> eval_ohformula g), (Forall eval_watched_clause (cnf_of_op_minus (is_classic g) o l hf acc) -> eval_ohformula g) -> eval_ohformula g.
proof: Proof. intros. apply ACC. intros. apply H. clear ACC H. destruct o ; simpl. - unfold cnf_minus_and. rewrite xmap_rev. apply Forall_app. split ; auto. rewrite Forall_forall. intros. rewrite in_map_iff in H. destruct H. destruct H. subst. unfold eval_watched_clause. simpl. rewrite EQ. rewrite eval_formula_rew. simpl. rewrite eval_and_list_eq. intros. left. rewrite <- in_rev in H1. revert x0 H1. rewrite <- Forall_forall. rewrite <- eval_and_list'_Forall. auto. - unfold cnf_minus_or. destruct l; auto. constructor ; auto. unfold eval_watched_clause. simpl. rewrite EQ. rewrite eval_formula_rew. unfold eval_op_list. rewrite eval_or_list_eq. simpl. unfold rev_map. rewrite xmap_rev. rewrite app_nil_r. rewrite eval_literal_list_POS. rewrite eval_or_list_rev. simpl. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause