proposition: Theorem small_models S T u (inF : u \in Fs S) : demo S T -> exists2 M : fmodel, #|M| <= 2 * size (Fs S) * (size T)^2 & forall C, C \in S -> exists (w : M), forall s, C |> s -> eval (interp' s) w.
proof: Proof. move => H. pose FD := (DD_demo H). pose FB := DD_fragment_bound H. exists (MD FD) => [|C inS]. - apply: leq_trans (MD_size FB) _. rewrite -!mulnA leq_mul2l mulnA [size T * _]mulnC -mulnA expnS expn1 !leq_mul2l. rewrite subset_size //. apply/subP. exact: demoSsubT. - pose p := (SeqSub _ inF, SeqSub _ inS). exists (Mstate (root (Frag FD p))). move => s ?. apply: supp_eval => //. by rewrite /= label_root. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)