{aⁿbⁿcᵐ} is context-free

The language lang_eq_any = {aⁿbⁿcᵐ | n,m ∈ ℕ} is context-free, presented as the concatenation of the context-free factors {aⁿbⁿ} and {cᵐ}.

lang_aux_ab (the {aⁿbⁿ} factor over Fin 3) and its context-freeness are exposed because the witness {aⁿbᵐcᵐ} reuses them via a letter permutation; see Langlib.Classes.ContextFree.Examples.AnBmCm.

def lang_aux_ab : Language (Fin 3)

The {aⁿbⁿ} factor over the Fin 3 alphabet.

Equations

• lang_aux_ab w = ∃ (n : ℕ), w = List.replicate n a_ ++ List.replicate n b_

theorem CF_lang_aux_ab : is_CF lang_aux_ab

theorem CF_lang_eq_any : is_CF lang_eq_any