proposition: Theorem informative_completeness t : prv (fImp t fF) + ({ M: fmodel & #|M| <= 2^(4 * sizef t) & { w: M | eval t w}}).
proof: Proof. set s := cnf t. set F := FL s. have sfc_s := @FL_closed s. case: (@pruning_completeness F _ [fset s^+]) => //. - move => u E uinE inP. apply: (@FL_cnf s); first by apply is_cn_mut. apply: flip_drop_sign. rewrite powersetE in inP. by move/(subP inP) : uinE. - by rewrite powersetE fsub1 flipcl_refl // FL_refl. - move => /href_of H. left. rewrite /href in H. rewrite <- H => //. apply: bigAI => u. rewrite inE => /eqP ->. rewrite /s /=. rewrite -> ax_cnf. exact: axI. - move => H. right. move: H => [M] [w] /(_ (s^+) (fset11 _)) /= A S. exists M. - apply: leq_trans S _. rewrite leq_exp2l // -[4]/(2 * 2) -mulnA ?leq_mul //. by apply: (leq_trans (n := sizef s)); rewrite ?FL_size ?size_cnf. - exists w. exact: (soundness (ax_cnfE t)). Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CPDL(PDL_def demo)