proposition: Lemma base0P C : C \in U -> prv ([af C] ---> \or_(L <- base [fset D in U | literalC D] C) [af L]).
proof: Proof. Proof with try solve [Lbase1|Lbase3|Lbase4] using sfc_F. apply: (@supp_aux _ ssub) => /= {C} ; last by move => ?; exact: sf_ssub. - move => [[|p|s t|s|s t|s t] [|]] //=; try exact: decomp_lit. - apply: (decomp_ab [fset [fset s^-]; [fset t^+]])... + simpl. rewrite -[fImp s t]/(s ---> t). rewrite -> (axIO s t). rule axOE. * rewrite -> af1n. apply: (bigOI xaf). by rewrite !inE eqxx. * rewrite -> (af1p t) at 1. apply: (bigOI xaf). by rewrite !inE eqxx. - apply: (decomp_ab [fset [fset s^+; t^-]])... + rewrite -[interp _]/(~~: (s ---> t)). rewrite -> dmI. rewrite -> (af1p s),(af1n t), <- andU at 1. apply: (bigOI xaf). by rewrite inE. - apply: (decomp_ab [fset [fset t^+; fAX (fAR s t)^+]; [fset t^+;s^+]])... + simpl. rewrite -> axAReq,axAODr at 1. rule axOE. * rewrite -> (af1p t),(af1p s),<- andU at 1. apply: (bigOI xaf). by rewrite !inE eqxx. * rewrite -> (af1p t),(af1p (AX (AR s t))),<- andU at 1. apply: (bigOI xaf). by rewrite !inE eqxx. - apply: (decomp_ab [fset [fset s^-; fAX (fAR s t)^-]; [fset t^-]])... + rewrite -[interp _]/(~~: AR s t). rewrite -> dmAR,axEUeq at 1. rule axOE. * rewrite -> (af1n t). apply: (bigOI xaf). by rewrite !inE eqxx. * rewrite <- dmAR, <- dmAX. rewrite -> (af1n s), (af1n (AX (AR s t))), <- andU at 1. apply: (bigOI xaf). by rewrite !inE eqxx. - apply: (decomp_ab [fset [fset s^+; fAX (fAU s t)^+]; [fset t^+]])... + simpl. rewrite -> axAUeq at 1. rule axOE. * rewrite -> (af1p t) at 1. apply: (bigOI xaf). by rewrite !inE eqxx. * rewrite -> (af1p s),(af1p (AX (AU s t))),<- andU at 1. apply: (bigOI xaf). by rewrite !inE eqxx. - apply: (decomp_ab [fset [fset t^-; fAX (fAU s t)^-]; [fset t^-;s^-]])... + rewrite -[interp _]/(~~: AU s t). rewrite -> dmAU, axERu, axAODr. rewrite <- dmAU, <- dmAX. rewrite /=. rule axOE. * rewrite -> af1n, af1n, <- andU. apply: (bigOI xaf). by rewrite !inE eqxx. * rewrite -> af1n, af1n, <- andU. apply: (bigOI xaf). by rewrite !inE eqxx. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.CTL(CTL_def dags demo hilbert relaxed_pruning)