fact: Fixpoint deriv a (e: regex'): regex' := match e with | r_zer | r_one => 0 | r_pls e f => deriv a e + deriv a f | r_dot e f => deriv a e ⋅ f + eps e ⋅ deriv a f | r_str e => deriv a e ⋅ (e: regex')^* | r_var b => ofbool (eqb_pos a b) end.
imports: syntax kleene boolean lang lset sums normalisation