proposition: Lemma unfulfilledAR_refute s t C : C \in S -> fAX (fAR s t)^- \in C -> ~~ fulfillsAR S S0 s t C -> prv ([af C] ---> Bot).
proof: Proof. Proof using coref_S sfc_F sub_S. move: C => C0 H1 H2 H3. have inF : fAX (fAR s t)^- \in F. apply: Fsub (ssub_refl _) H2 _ => //. move/(subP sub_S) : H1. by case/sepP. pose I : {fset clause} := [fset D in S | ~~ fulfillsAR S S0 s t D]. pose u : form := \or_(D<-I) [af D]. rewrite /= in I u. have C0u: prv ([af C0] ---> u) by apply: (bigOI xaf); rewrite inE H1. have C0x: prv ([af C0] ---> ~~: AX (AR s t)) by rewrite -> (bigAE _ H2); exact: axI. suff sf: prv (u ---> fAX (fAR s t)) by Intro; ApplyH C0x; ApplyH sf; ApplyH C0u. have I1 C : C \in I -> (exists2 D : clause, D \in Req C & ~~ suppS S D) \/ base S (s^- |` R C) `<=` I /\ ~~ suppS S (t^- |` R C). { rewrite inE => /andP [HL1 HL3]. rewrite /fulfillsAR fulfillsARE inE !negb_and negb_or (subP sub_S _ HL1) /= in HL3. case/orP : HL3 => [L1|/andP[L1 L2]];[left;exact/allPn|right]. split => //. apply/subP => X /sepP. rewrite !inE suppCU suppC1 => [[inS] /andP [sX sR]]. rewrite inS /=. apply: contraNN L2 => rnk. apply/hasP; exists X => //. + exact: (subP sub_S). + by rewrite !suppCU !suppC1 !sX sR. } apply: AXR_ind. apply: bigOE => L LinD. have LinU : L \in U. apply: (SsubU sub_S). move: L LinD. apply/subP. exact: subsep. move/I1 : (LinD) => [[E E1 E2]|[L1 L2]]. - suff W: prv ([af L] ---> Bot) by rewrite -> W; exact: axBE. apply: ax_ReqR (E1) _. apply: coref_supp E2. exact: ReqU E1. - rewrite -> box_request. apply: rNorm. apply: rAI. + apply: refE1n. apply: coref_supp => //. rewrite powersetU RinU // andbT powersetE fsub1. by case/and3P :(sfc_F (sfc_F inF)). + rewrite /Or. apply: rAIL => /=. rewrite -> af1n, <- andU. rewrite fsetUC. rewrite -> baseP; first (apply: or_sub; exact/subP). rewrite powersetU RinU // andbT powersetE fsub1. by case/and3P :(sfc_F (sfc_F inF)). 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)