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 => 1 | EmptyStr => 1 | Char _ => 2 | App re1 re2 => pumping_constant re1 + pumping_constant re2 | Union re1 re2 => pumping_constant re1 + pumping_constant re2 | Star r => pumping_constant r end. Lemma pumping_constant_ge_1 : forall T (re : reg_exp T), pumping_constant re >= 1. Proof. intros T re. induction re. - apply le_n. - apply le_n. - apply le_S. apply le_n. - simpl. apply le_trans with (n:=pumping_constant re1). apply IHre1. apply le_plus_l. - simpl. apply le_trans with (n:=pumping_constant re1). apply IHre1. apply le_plus_l. - simpl. apply IHre. Qed.
imports: Coq(Lia)