fact: Fixpoint mem_reg e := match e with | Void => void char | Eps => eps char | Dot => dot char | Atom x => atom x | Star e1 => star (mem_reg e1) | Plus e1 e2 => plus (mem_reg e1) (mem_reg e2) | And e1 e2 => prod (mem_reg e1) (mem_reg e2) | Conc e1 e2 => conc (mem_reg e1) (mem_reg e2) | Not e1 => compl (mem_reg e1) end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)