proposition: Lemma frag_AR C : C |> s^- -> fAX (fAR s t)^- \in C -> fAX (fAR s t)^- \in Fs S -> C \in S -> {G : rGraph clause | fragment S T G (fAX (fAR s t)^-) C & #|G| <= 2 * size T}.
proof: Proof. Proof using demoST. move => C1 C2 C3 C4. have C4' : C \in T. exact: demoSsubT demoST _ _. have CinARl : C \in [fset C in T | fulfillsAR S T s t C] by rewrite inE C4' demo3. pose x0 : AR_T0 := inl (Sub C CinARl). pose V := { x : AR_T0 | connect AR_rel x0 x }. pose v0 : V := Sub x0 (connect0 _ x0). pose E (x y : V) := AR_rel (val x) (val y). pose L (x : V) : clause := AR_label (sval x). pose G := Graph E L. have rP (v : G) : connect E v0 v. exact: connect_subtype. pose rG := RGraph rP. have lf (x : seq_sub ARr) p : @leaf _ rG (Sub (inr x) p). by apply/negP => /existsP [y] //. have nlf (x : seq_sub ARl) p : ~~ @leaf _ rG (Sub (inl x) p). rewrite negbK. apply/existsP. case: (inhab_Req (@label _ rG (Sub (inl x) p))) => D. case/AR_rel_succ => y y1 y2. suff H: connect AR_rel x0 y by exists (Sub y H). exact: connect_trans p (connect1 _). exists rG. split. - done. - move => x. exact: sn_preimage (AR_rel_term (val x)). - case => [[x|x]] p /=; last by rewrite lf. move => _ D /AR_rel_succ [y] y1 y2. have conn: connect AR_rel x0 y. exact: connect_trans (connect1 y1). by exists (exist _ y conn). - move => x y. case: x => [[[x Hx]|[x Hx]]]; case: y => [[[y Hy]|[y Hy]]] Hx' Hy' ; rewrite //= /E /L /=; try bcase. - rewrite /ev_cond /v0 /L /= /L /= C2 C1 /= => _. split. + case => [[x|x]] p; rewrite ?lf // -[exist _ _ _]/(Sub (inl x) p). move => _. case/connectP : p (p). elim/last_ind => [_ -> p //|pth z IH]. rewrite last_rcons rcons_path => /andP [p1 p2] ? p; subst. move: p2. exact: AR_rel_supp. + case: (AR_ev_cond (Sub C CinARl)) => y y1 y2. by exists (Sub y y1). - exact: nlf. - move => x. case: x => [[x|x]] p. - rewrite -[exist _ _ _]/(Sub (inl x) p) (negbTE (nlf _ _)). move: (ssvalP x). rewrite inE; by bcase. - rewrite -[exist _ _ _]/(Sub (inr x) p) lf. exact: (ssvalP x). - rewrite card_sig. apply: leq_trans (max_card _) _. rewrite card_sum mul2n -addnn leq_add // card_seq_sub ?funiq //. + exact: subset_size (subsep _ _). + apply: (@leq_trans (size S)); apply: subset_size => //. exact: subxx. apply/subP. exact: demoSsubT. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)