proposition: Lemma not_regular: forall (L:language), (forall p, p >= 1 -> Clogged L p) -> ~ Regular L.
proof: Proof. intros. intros N. apply pumping in N. destruct N as (p, (Hle, Hw)). assert (H := H _ Hle). inversion H as (w, Hin, Hlen, Hc); subst; clear H. assert (Hw := Hw w Hin Hlen). inversion Hw as (x, y, z, ?, ?, ?, Ha); subst; clear Hw. assert (Hi: exists i, ~ In (x ++ (pow y i) ++ z) L). { apply Hc. - reflexivity. - assumption. - assumption. } destruct Hi as (i, Hi). contradict Hi. apply Ha. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util