proposition: Lemma finite_pred_der_star : forall E, Finite (set_of_der E) -> Finite (set_of_der_star E ).
proof: Proof. move => E hE. have hsim : Finite (@f_set (regexp*regexp*seq regexp) regexp sim fStar (Prod (Prod (set_of_der E) (pred_singl E)) (gpred_list (set_of_der E)))). - apply: (@Bar_fun _ _ eqtemp). + by apply: fStar_compat. apply: (@Bar_grel_incl _ _ (r_prod (r_prod nsim nsim) neqs)). + apply : Bar_gset_prod. * apply: Bar_gset_prod; first done. by apply : finite_pred_singl. apply (@Bar_grel_incl _ _ (neq (eql sim))). * apply: Bar_gpred_list; last done. by apply: sim_dec. rewrite /E_compat. by apply set_of_der_compat. move => x y; apply : neql2n_eql. by apply: sim_dec. by apply: fpred_conc_incl. apply: (@Bar_gset_incl _ (f_set sim fStar (Prod (Prod (set_of_der E) (pred_singl E)) (gpred_list (set_of_der E))))); first done. move => x. rewrite /set_of_der_star. case => e [l [h1 [h2 h3]]]. rewrite /f_set. exists (e,E,l). split => //. split => //. by rewrite /pred_singl; reflexivity. move :h3; rewrite /sim /fStar. by symmetry. Qed.
imports: Coq(RelationClasses Setoid Morphisms Permutation) Coq(SetoidList Mergesort Orders) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp)