fact: Fixpoint pumping_constant (re : regex) : nat := match re with | r_void => 1 | r_nil => 1 | r_char _ => 2 | r_app re1 re2 => pumping_constant re1 + pumping_constant re2 | r_union re1 re2 => pumping_constant re1 + pumping_constant re2 | r_star r => pumping_constant r end.
imports: Coq.micromega.Lia Turing.Util Turing.Lang