proposition: Lemma MStar'' : forall T (s : list T) (re : reg_exp T), s =~ Star re -> exists ss : list (list T), s = fold app ss [] /\ forall s', In s' ss -> s' =~ re.
proof: Proof. Admitted. Module Pumping. Fixpoint pumping_constant {T} (re : reg_exp T) : nat := match re with | EmptySet => 0 | EmptyStr => 1 | Char _ => 2 | App re1 re2 => pumping_constant re1 + pumping_constant re2 | Union re1 re2 => pumping_constant re1 + pumping_constant re2 | Star _ => 1 end. Fixpoint napp {T} (n : nat) (l : list T) : list T := match n with | 0 => [] | S n' => l ++ napp n' l end. Lemma napp_plus: forall T (n m : nat) (l : list T), napp (n + m) l = napp n l ++ napp m l. Proof. intros T n m l. induction n as [|n IHn]. - reflexivity. - simpl. rewrite IHn, app_assoc. reflexivity. Qed.
imports: Logic