proposition: Lemma not_regular_ex: forall (L:language), (forall p, p >= 1 -> exists w, ( In w L /\ length w >= p /\ ( forall x y z, (w = x ++ y ++ z -> y <> [] -> length (x ++ y) <= p -> exists i, ~ In (x ++ pow y i ++ z) L )))) -> ~ Regular L.
proof: Proof. intros. apply not_regular. intros. destruct (H _ H0) as (w, (Ha, (Hb, Hc))); clear H. apply clogged_def with (w:=w); auto. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util