proposition: Lemma wf_split_polarity: forall (p : HFormula) (l lp ln lo : cnf) (WF : Forall wf l) , Elim.split_polarity p l = (lp, ln, lo) -> Forall wf lp /\ Forall wf ln /\ Forall wf lo.
proof: Proof. induction l. - simpl; intros. inv H. simpl. tauto. - intros. simpl in H. destruct (Elim.split_polarity p l) as [[lp' ln'] lo'] eqn:E. inv WF. specialize (IHl lp' ln' lo' H3 eq_refl). destruct (Elim.normalise a) eqn:N; simpl. + apply wf_normalise in N; auto. destruct (Elim.get_polarity_rec p c) eqn:GP. * destruct p0 as [b cl']. apply get_polarity_rec_sublist in GP. destruct GP. apply wf_sublist in H0;auto. destruct b; inv H; intuition. * inv H. intuition. + inv H;intuition. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause