proposition: Lemma simple_frag s C : (forall G, label (root G) = C -> ev_cond s G) -> C \in S -> { G : rGraph clause | fragment S T G s C & #|G| <= 2 * size T}.
proof: Proof. Proof using demoST. move => ev_s inDD. pose xs : seq clause := [fset D in S | suppC D (R C)]. pose V := option (seq_sub xs). pose E := [rel x y : V | ~~ isSome x && isSome y]. pose L (x:V) : clause := if x is Some v then val v else C. pose G := Graph E L. have rP (x:G) : connect E None x. case: x => // x. exact: connect1. pose rG := RGraph rP. have s_cond_C D : D \in Req C -> exists2 y : option (seq_sub xs), y & suppC (L y) D. move => inReq. case/(demo1 demoST) : (inReq) => // D' /andP[D1 D2]. suff in_xs : D' \in xs by exists (Some (Sub D' in_xs)). rewrite inE D1. exact: suppC_sub (Req_RC _ ) D2. exists rG. split. - done. - have H x : sn (erel rG) (Some x) by constructor. case; first exact: H. constructor => [[y _|//]]. exact: H. - move => [x|] H D //= inReq; first by rewrite negbK in H; case/existsP : H. exact: s_cond_C. - move => [x|] [y|] //=. move: (ssvalP y). by rewrite inE; bcase. - exact: ev_s. - rewrite negbK. apply/existsP. case: (inhab_Req C) => D /= inReq. case/s_cond_C : inReq. eauto. - move => x. suff H : label x \in S. rewrite H [_ \in T](_ : _ = true) ?if_same //. move: H. exact: demoSsubT. case: x => [v|//]. move : (ssvalP v). rewrite inE; by bcase. - rewrite card_option mul2n -addnn -addn1 leq_add ?card_seq_sub ?funiq //. + apply: subset_size. apply: sub_trans (subsep _ _) _. apply/subP. exact: demoSsubT. + apply: (@leq_trans (size [fset C])); first by rewrite fset1Es. apply subset_size. rewrite fsub1. exact: demoSsubT demoST _ _. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)