{aⁿbⁿcⁿdⁿ}: a four-symbol non-context-free witness language

The single-parameter four-symbol witness anbncndn = {aⁿbⁿcⁿdⁿ | n ≥ 0}, proven non-context-free via the CFL pumping lemma + the unified adjacency lemma in BlockWitness.

Membership requires na = nb = nc = nd (all four counts equal) and the sorted shape aⁿbⁿcⁿdⁿ. Pumping breaks at least one count equality.

This file also hosts the shared FourSymbol substrate consumed by the two-parameter relaxation in NonContextFree.AmBnCmDn:

• The alphabet (FourSymbol, FourString, LawfulBEq).
• Witness-form bridges (makeString_anbncndn_eq_blockwitness).
• Three adjacency consequences via BlockWitness.not_both_in_vxy (not_a_and_d_in_vxy, not_a_and_c_in_vxy, not_b_and_d_in_vxy).
• Filter-count machinery (filter_count, filter_eq_nil_of_not_mem, fourSymbol_filter_total).

Closure properties for IsContextFree (homomorphism, regular intersection) live in Linglib.Core.Computability.ContextFreeGrammar.Closure.

inductive FourSymbol : Type

Alphabet for cross-serial dependency patterns.

• a : FourSymbol
• b : FourSymbol
• c : FourSymbol
• d : FourSymbol

@[implicit_reducible]

instance instDecidableEqFourSymbol : DecidableEq FourSymbol

Equations

• instDecidableEqFourSymbol x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprFourSymbol.repr : FourSymbol → ℕ → Std.Format

Equations

• instReprFourSymbol.repr FourSymbol.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FourSymbol.a")).group prec✝
• instReprFourSymbol.repr FourSymbol.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FourSymbol.b")).group prec✝
• instReprFourSymbol.repr FourSymbol.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FourSymbol.c")).group prec✝
• instReprFourSymbol.repr FourSymbol.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FourSymbol.d")).group prec✝

@[implicit_reducible]

instance instReprFourSymbol : Repr FourSymbol

Equations

• instReprFourSymbol = { reprPrec := instReprFourSymbol.repr }

instance instLawfulBEqFourSymbol : LawfulBEq FourSymbol

@[reducible, inline]

abbrev FourString : Type

Equations

• FourString = List FourSymbol

def isInLanguage_anbncndn (w : FourString) : Bool

The language {aⁿbⁿcⁿdⁿ | n ≥ 0}, modeling Dutch cross-serial dependencies.

Equations

• One or more equations did not get rendered due to their size.
• isInLanguage_anbncndn [] = true

def makeString_anbncndn (n : ℕ) : FourString

Generate aⁿbⁿcⁿdⁿ.

Equations

• makeString_anbncndn n = List.replicate n FourSymbol.a ++ List.replicate n FourSymbol.b ++ List.replicate n FourSymbol.c ++ List.replicate n FourSymbol.d

def anbncndn : Language FourSymbol

The language {aⁿbⁿcⁿdⁿ | n ≥ 0} as a mathlib Language.

Equations

• anbncndn = {w : List FourSymbol | isInLanguage_anbncndn w = true}

theorem filter_count (n : ℕ) (s : FourSymbol) : (List.filter (fun (x : FourSymbol) => x == s) (makeString_anbncndn n)).length = n

Each symbol's filter count in makeString_anbncndn n equals n. Shared with AmBnCmDn (which pumps over the same diagonal witness).

theorem makeString_anbncndn_eq_blockwitness (n : ℕ) : makeString_anbncndn n = BlockWitness [FourSymbol.a, FourSymbol.b, FourSymbol.c, FourSymbol.d] n

The four-symbol witness is structurally BlockWitness [a, b, c, d] n.

theorem not_a_and_d_in_vxy (p : ℕ) (u vxy z : FourString) (hw : makeString_anbncndn p = u ++ vxy ++ z) (hvxy : List.length vxy ≤ p) : ¬(FourSymbol.a ∈ vxy ∧ FourSymbol.d ∈ vxy)

theorem not_a_and_c_in_vxy (p : ℕ) (u vxy z : FourString) (hw : makeString_anbncndn p = u ++ vxy ++ z) (hvxy : List.length vxy ≤ p) : ¬(FourSymbol.a ∈ vxy ∧ FourSymbol.c ∈ vxy)

theorem not_b_and_d_in_vxy (p : ℕ) (u vxy z : FourString) (hw : makeString_anbncndn p = u ++ vxy ++ z) (hvxy : List.length vxy ≤ p) : ¬(FourSymbol.b ∈ vxy ∧ FourSymbol.d ∈ vxy)

theorem filter_eq_nil_of_not_mem (l : FourString) (s : FourSymbol) (h : s ∉ l) : List.filter (fun (x : FourSymbol) => x == s) l = []

theorem fourSymbol_filter_total (l : FourString) : (List.filter (fun (x : FourSymbol) => x == FourSymbol.a) l).length + (List.filter (fun (x : FourSymbol) => x == FourSymbol.b) l).length + (List.filter (fun (x : FourSymbol) => x == FourSymbol.c) l).length + (List.filter (fun (x : FourSymbol) => x == FourSymbol.d) l).length = List.length l

theorem makeString_in_language (n : ℕ) : makeString_anbncndn n ∈ anbncndn

makeString_anbncndn n is always in {aⁿbⁿcⁿdⁿ}.

theorem mem_anbncndn_iff (w : FourString) : w ∈ anbncndn ↔ ∃ (n : ℕ), w = makeString_anbncndn n

Membership characterization: every string in anbncndn is makeString_anbncndn n for some n. The converse to makeString_in_language.

theorem pump_breaks_anbncndn (p : ℕ) (_hp : p > 0) : have w := makeString_anbncndn p; ∀ (u v x y z : FourString), w = u ++ v ++ x ++ y ++ z → List.length (v ++ x ++ y) ≤ p → List.length v + List.length y ≥ 1 → ∃ (i : ℕ), u ++ (List.replicate i v).flatten ++ x ++ (List.replicate i y).flatten ++ z ∉ anbncndn

Pumping breaks membership in {aⁿbⁿcⁿdⁿ}.

theorem anbncndn_not_pumpable : ¬HasCFLPumpingProperty anbncndn

{aⁿbⁿcⁿdⁿ} does NOT have the CFL pumping property.

theorem anbncndn_not_contextFree : ¬anbncndn.IsContextFree

{aⁿbⁿcⁿdⁿ} is not context-free.