proposition: Lemma r_star_to_pow: forall r s, Accept (r_star r) s -> exists n, Accept (r_pow r n) s.
proof: Proof. intros. remember (r_star r) as r1. generalize dependent r. induction H; intros; inversion Heqr1; subst; clear Heqr1. - exists 0. apply accept_nil. - assert (Hx := IHAccept2 r). destruct Hx as (n, Hr); auto. eauto using r_pow_succ. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang