fact: Fixpoint pderiv a i (e: ugregex): list ugregex := match e with | u_prd _ => [] | u_var _ j => if eqb_pos i j then [u_one _] else [] | u_pls e f => union (pderiv a i e) (pderiv a i f) | u_dot e f => if epsilon a e then union (map (tod f) (pderiv a i e)) (pderiv a i f) else map (tod f) (pderiv a i e) | u_itr e => map (tod (u_str e)) (pderiv a i e) end.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex