proposition: Lemma split_polarity_no_vars : forall p cl1 cl2 lp ln lo, ~ is_var_of_cnf p cl1 -> Elim.split_polarity p cl2 = (lp,ln,lo) -> Elim.split_polarity p (cl1 ++ cl2) = (lp, ln, map_filter Elim.normalise cl1++lo).
proof: Proof. induction cl1. - simpl. auto. - simpl. intros. apply IHcl1 in H0. rewrite H0. destruct (Elim.normalise a) eqn:N. apply normalise_vars with (p:=p) in N. rewrite is_var_of_cnf_cons in H. rewrite get_polarity_spec_not_var by tauto. reflexivity. reflexivity. rewrite is_var_of_cnf_cons in H. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause