proposition: Theorem pruning_completeness F (sfc_F : sf_closed F) (C: clause) : (forall s E, s \in E -> E \in PU F -> is_cnf (drop_sign s)) -> C \in PU F -> pref F C + { M: fmodel & satT M C & #|{: M}| <= 2 ^ (2 * size F)}.
proof: Proof. move => cnf_S inPU. case: (boolP ((DD F) |> C)) => H; [right|left; exact: DD_refute]. exists (model_of (DD F)). - case/hasS : H => D D1 /subP D2. exists (SeqSub _ D1) => s inC. move: inPU. move/powersetP => sub. case: s inC => s b inC. apply: demo_eval => //=; last exact: D2. move => t E inE H. apply: cnf_S inE _. move: H. apply/subP. apply: sub_trans (prune_sub _ _) _. exact: subsep. - rewrite card_seq_sub ?funiq //. apply: leq_trans; last by apply: (leq_pexp2l _ (size_flipcl F)). rewrite -powerset_size subset_size /DD /S0 //=. apply: sub_trans; [exact: prune_sub | exact: subsep]. Qed.
imports: Relations Classical_Pred_Type mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.CPDL(PDL_def)