fact: Fixpoint der x e := match e with | Void => Void | Eps => Void | Dot => Eps | Atom y => if x == y then Eps else Void | Star e1 => Conc (der x e1) (Star e1) | Plus e1 e2 => Plus (der x e1) (der x e2) | And e1 e2 => And (der x e1) (der x e2) | Conc e1 e2 => if has_eps e1 then Plus (Conc (der x e1) e2) (der x e2) else Conc (der x e1) e2 | Not e1 => Not (der x e1) end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)