{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}. Membership requires na = nb = nc = nd (all four counts equal) and the sorted shape aⁿbⁿcⁿdⁿ.

Non-context-freeness is derived by closure, not re-proved by pumping: the erasing homomorphism dropD : d ↦ ε maps anbncndn exactly onto the irreducible counting core anbnc = {aⁿbⁿcⁿ} (AnBnCn), so anbncndn_not_contextFree follows from anbnc_not_contextFree through Language.IsContextFree.stringMap (the hom-closure root in Map, run contrapositively via Closure). aⁿbⁿcⁿdⁿ is the nested-counting case; the genuinely crossing witness that [Shi85]'s Swiss-German argument requires is the two-parameter ambncmdn sibling, which does not reduce by single-symbol erasure.

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).
• Adjacency consequences via BlockWitness.not_both_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).

inductive FourSymbol : Type

Alphabet for the four-symbol counting witness languages.

• 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 ⋯

@[implicit_reducible]

instance instReprFourSymbol : Repr FourSymbol

Equations

• instReprFourSymbol = { reprPrec := instReprFourSymbol.repr }

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✝

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}: the pedagogical four-symbol counting language. The genuinely crossing witness that [Shi85]'s Swiss-German non-context-freeness argument requires is the two-parameter ambncmdn sibling; this single-parameter language is the nested-counting case (cf. [BKPZ82] on Dutch cross-serial word order, which is itself only weakly context-free).

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_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.

def dropD : FourSymbol → List ThreeSymbol

The erasing homomorphism d ↦ ε (per-symbol map; the string action is List.flatMap dropD, the free-monoid lift), relabelling the surviving a/b/c into the ThreeSymbol alphabet. The witness for the reduction aⁿbⁿcⁿdⁿ → aⁿbⁿcⁿ.

Equations

• dropD FourSymbol.a = [ThreeSymbol.a]
• dropD FourSymbol.b = [ThreeSymbol.b]
• dropD FourSymbol.c = [ThreeSymbol.c]
• dropD FourSymbol.d = []

@[simp]

theorem dropD_makeString (n : ℕ) : List.flatMap dropD (makeString_anbncndn n) = makeString_anbnc n

dropD erases the dⁿ block and relabels, sending the witness to makeString_anbnc n.

theorem stringMap_dropD_anbncndn : (Language.stringMap dropD) anbncndn = anbnc

dropD maps anbncndn exactly onto the counting core anbnc. This image equality is what powers the closure reduction.

theorem anbncndn_not_contextFree : ¬anbncndn.IsContextFree

{aⁿbⁿcⁿdⁿ} is not context-free — derived by closure from the counting core anbnc_not_contextFree via the erasing homomorphism dropD, rather than re-proved by pumping.