proposition: Lemma l4_not_regular_v3: ~ 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. - unfold In. unfold Clogs. intros. exists 2. unfold In. intros N. destruct N as (n, N). simpl in N. Search (_ ++ []). rewrite app_nil_r in N. apply xyz_rw_ex in H0; auto. destruct H0 as (b, (Hz, (_,(Hb,(Hc,Hd))))). clear H2. rewrite Hz in Hd; clear Hz. rewrite Hb in N; clear Hb. rewrite Hc in N; clear Hc. rewrite Hd in N; clear Hd. 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. rewrite app_length in *. 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