{0ⁿ1ⁿ2ᵐ3ᵐ} is context-free

L4 is context-free as a concatenation of two context-free factors map f4 {aⁿbⁿ} and map g4 {aⁿbⁿ}. The generic lemma map_anbn_is_CF and the membership characterizations mem_map_anbn / eq_of_mem_map_anbn for map f {aⁿbⁿ} are exposed because the not-linear proof in Langlib.Classes.Linear.Examples.L4 reuses them.

theorem map_anbn_is_CF {T : Type} (f : Bool → T) : is_CF ((Language.map f) anbn)

map f {aⁿbⁿ} is context-free for any letter map f.

theorem L4_is_CF : is_CF L4

{0ⁿ1ⁿ2ᵐ3ᵐ} is context-free.

theorem mem_map_anbn {T : Type} (f : Bool → T) (k : ℕ) : List.replicate k (f false) ++ List.replicate k (f true) ∈ (Language.map f) anbn

(f false)ᵏ (f true)ᵏ ∈ map f {aⁿbⁿ}.

theorem eq_of_mem_map_anbn {T : Type} {f : Bool → T} {s : List T} (hs : s ∈ (Language.map f) anbn) : ∃ (k : ℕ), s = List.replicate k (f false) ++ List.replicate k (f true)

Membership in map f {aⁿbⁿ} is exactly (f false)ᵏ (f true)ᵏ.

theorem Lwit_is_CF {T : Type} (e : Fin 4 ↪ T) : is_CF ((Language.map ⇑e) L4)

The Fin 4 witness, relabelled along an embedding, is context-free.