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

The classical three-symbol witness anbnc = {aⁿbⁿcⁿ | n ≥ 0}, shown non-context-free by the CFL pumping lemma together with the adjacency lemma of BlockWitness: a pumped window short enough to fit inside the witness cannot meet both the a-block and the c-block, so pumping down leaves some symbol's count untouched while shortening the word.

Independent of AnBnCnDn and AmBnCmDn: it uses its own ThreeSymbol alphabet.

Main definitions

• makeString_anbnc n: the witness word aⁿbⁿcⁿ.
• anbnc: the language {aⁿbⁿcⁿ | n ≥ 0}, as the range of makeString_anbnc.

Main results

• anbnc_not_pumpable: anbnc lacks the CFL pumping property.
• anbnc_not_contextFree: anbnc is not context-free.

inductive ThreeSymbol : Type

Alphabet for {aⁿbⁿcⁿ}.

• a : ThreeSymbol
• b : ThreeSymbol
• c : ThreeSymbol

@[instance_reducible]

instance instDecidableEqThreeSymbol : DecidableEq ThreeSymbol

Equations

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

@[instance_reducible]

instance instReprThreeSymbol : Repr ThreeSymbol

Equations

• instReprThreeSymbol = { reprPrec := instReprThreeSymbol.repr }

def instReprThreeSymbol.repr : ThreeSymbol → ℕ → Std.Format

Equations

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

def makeString_anbnc (n : ℕ) : List ThreeSymbol

The witness word aⁿbⁿcⁿ.

Equations

• makeString_anbnc n = List.replicate n ThreeSymbol.a ++ List.replicate n ThreeSymbol.b ++ List.replicate n ThreeSymbol.c

def anbnc : Language ThreeSymbol

The language {aⁿbⁿcⁿ | n ≥ 0}, as the range of makeString_anbnc.

Equations

• anbnc = {w : List ThreeSymbol | ∃ (n : ℕ), w = makeString_anbnc n}

theorem mem_anbnc_iff (w : List ThreeSymbol) : w ∈ anbnc ↔ ∃ (n : ℕ), w = makeString_anbnc n

Membership characterization: every string in anbnc is makeString_anbnc n for some n. Consumed by the homomorphic reduction aⁿbⁿcⁿdⁿ → aⁿbⁿcⁿ in AnBnCnDn.

theorem makeString_anbnc_mem (n : ℕ) : makeString_anbnc n ∈ anbnc

@[simp]

theorem count_makeString_anbnc (n : ℕ) (s : ThreeSymbol) : List.count s (makeString_anbnc n) = n

Each of the three symbols occurs exactly n times in the witness.

@[simp]

theorem length_makeString_anbnc (n : ℕ) : (makeString_anbnc n).length = 3 * n

theorem anbnc_not_pumpable : ¬HasCFLPumpingProperty anbnc

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

Pumping down to i = 0 gives u ++ x ++ z = makeString_anbnc m, so every symbol occurs m times there. The pumped-out window is too short to meet both the a- and the c-block, so one of those two symbols is absent from v and y — forcing m = p, while the removed window makes the word strictly shorter.

theorem anbnc_not_contextFree : ¬anbnc.IsContextFree

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