proposition: Lemma l4_not_regular: ~ Regular Turing.Lang.Examples.L4.
proof: Proof. apply not_regular. intros. rewrite Turing.Lang.Examples.l4_spec. apply clogged_def with (w:=(pow1 "a" p ++ pow1 "b" p) % list). - unfold In. exists p. reflexivity. - Search (length (_ ++ _)). rewrite app_length. Search (length (pow1 _ _)). rewrite pow1_length. lia. - Search (In _ (Clogs _ _)). apply in_clogs. intros x y z Ha Hneq Hlen. exists 2. unfold In. intros N. destruct N as (n, N). simpl in N. Search (_ ++ []). rewrite app_nil_r in N. apply xyz_rw in Ha; auto. destruct Ha as (b, (_, Hb)). apply pow1_plus_xy in Hb. destruct Hb as (Hx, Hyz). symmetry in Hyz. apply pow1_plus_xy in Hyz. destruct Hyz as (Hy, Hz). rewrite Hy in N. rewrite Hx in N. rewrite Hz in N. repeat rewrite app_assoc in *. repeat rewrite pow1_plus in N. assert ("a" <> "b") by (intros M; inversion M). apply pow1_a_b_inv_eq in N; auto. destruct N as (L, R). subst. repeat rewrite <- Nat.add_assoc in *. apply plus_inv_eq_r in R. apply plus_inv_eq_r in R. apply plus_inv_zero_l in R. destruct y. { contradiction. } inversion R. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util