proposition: Lemma unfulfilledAU_refute s t L : L \in S -> (fAX (fAU s t)^+ \in L) -> ~~ fulfillsAU S S0 s t L -> mprv ([af L] ---> Bot).
proof: Proof. Proof using coref_S sfc_F sub_S. move => H1 H2 H3. pose I : {fset clause} := [fset X in S | ~~ fulfillsAU S S0 s t X]. pose u : form := \or_(D <- I) [af D]. rewrite /= in I u. suff sf : prv (u ---> ~~: fAX (fAU s t)). { Intro. ApplyH sf; Rev. - apply: (bigOI xaf). by rewrite inE H1. - rewrite ->(bigAE _ H2). exact: axI. } have HI C : C \in I -> exists2 D : clause, D \in Req C & base S (s^+ |` D) `<=` I /\ ~~ suppS S (t^+ |` D). { rewrite inE => /andP [L1' L3']. rewrite /fulfillsAU fulfillsAUE inE (subP sub_S _ L1') /= in L3'. case/allPn : L3' => D DReq. rewrite negb_or => /andP [HS /hasPn HS']. exists D => //. split => //. apply/subP => X. rewrite !inE => /andP [inS sXC]. move: (HS' _ (subP sub_S _ inS)). by rewrite inS sXC. } rewrite -> (axDNI (fAU s t)), dmAU. apply: EXR_ind. apply: bigOE => X XinD. case: (HI _ XinD) => C inReq [base1 base2]. have XinU : X \in U. apply: (SsubU sub_S). by case/sepP : XinD. move/(subP sub_S) : H1. rewrite inE => /and3P [H1 _ _]. rewrite -> (ax_Req inReq). apply: rEXn. ApplyH axAI. - have inU : t^+ |` C \in U. rewrite powersetU (ReqU sfc_F XinU inReq) powersetE fsub1 andbT. apply: Fsub H2 H1 => //. by rewrite /= !inE ssub_refl. apply: rAIL. rewrite -> (af1p t), <- andU, fsetUC. exact: coref_supp. - rewrite {1}/Or. apply: rAIL. rewrite -> modular_hilbert.axDN, (af1p s), <- andU, fsetUC. rewrite -> baseP. apply: or_sub. exact/subP. rewrite powersetU (ReqU sfc_F XinU inReq) powersetE fsub1 /= andbT. apply: Fsub H2 H1 => //. by rewrite /= !inE ssub_refl. 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)