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

The single-parameter four-symbol witness anbncndn = {aⁿbⁿcⁿdⁿ | n ≥ 0}.

Non-context-freeness is derived by closure, not re-proved by pumping: the erasing homomorphism dropD : d ↦ ε maps anbncndn exactly onto the counting core anbnc = {aⁿbⁿcⁿ}, so anbncndn_not_contextFree follows from anbnc_not_contextFree through Language.IsContextFree.stringMap. aⁿbⁿcⁿdⁿ is the nested-counting case; the genuinely crossing witness is the two-parameter ambncmdn sibling, which does not reduce by single-symbol erasure.

This file also hosts the FourSymbol substrate shared with NonContextFree.AmBnCmDn: the alphabet, the witness-form bridge to BlockWitness, and the two adjacency consequences.

Main definitions

• FourSymbol, FourString: the shared four-letter alphabet and its words.
• makeString_anbncndn n: the witness word aⁿbⁿcⁿdⁿ.
• anbncndn: the language {aⁿbⁿcⁿdⁿ | n ≥ 0}, as the range of makeString_anbncndn.
• dropD: the erasing homomorphism d ↦ ε witnessing the reduction to anbnc.

Main results

• not_a_and_c_in_vxy / not_b_and_d_in_vxy: a window of length ≤ p cannot meet two blocks that are not adjacent.
• stringMap_dropD_anbncndn: dropD maps anbncndn onto anbnc.
• anbncndn_not_contextFree: anbncndn is not context-free.

inductive FourSymbol : Type

Alphabet for the four-symbol counting witness languages.

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

@[instance_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✝

@[instance_reducible]

instance instReprFourSymbol : Repr FourSymbol

Equations

• instReprFourSymbol = { reprPrec := instReprFourSymbol.repr }

@[reducible, inline]

abbrev FourString : Type

Words over the four-symbol alphabet.

Equations

• FourString = List FourSymbol

def makeString_anbncndn (n : ℕ) : FourString

The witness word 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 the range of makeString_anbncndn.

Equations

• anbncndn = {w : List FourSymbol | ∃ (n : ℕ), w = makeString_anbncndn n}

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.

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

@[simp]

theorem count_makeString_anbncndn (n : ℕ) (s : FourSymbol) : List.count s (makeString_anbncndn n) = n

Each of the four symbols occurs exactly n times in the witness. Shared with AmBnCmDn, which pumps over the same diagonal witness.

@[simp]

theorem length_makeString_anbncndn (n : ℕ) : List.length (makeString_anbncndn n) = 4 * n

theorem fourSymbol_count_total (l : FourString) : List.count FourSymbol.a l + List.count FourSymbol.b l + List.count FourSymbol.c l + List.count FourSymbol.d l = List.length l

The four symbol counts of a word sum to its length.

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)

Non-context-freeness by homomorphic reduction to {aⁿbⁿcⁿ}

def dropD : FourSymbol → List ThreeSymbol

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

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 anbnc_not_contextFree via the erasing homomorphism dropD, rather than re-proved by pumping.