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

The classical three-symbol non-context-free witness anbnc = {aⁿbⁿcⁿ | n ≥ 0}, proven non-context-free via the CFL pumping lemma + the unified adjacency lemma in BlockWitness.

Independent of AnBnCnDn and AmBnCmDn — uses its own ThreeSymbol alphabet and parallel filter-count machinery.

inductive ThreeSymbol : Type

Alphabet for {aⁿbⁿcⁿ}.

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

@[implicit_reducible]

instance instDecidableEqThreeSymbol : DecidableEq ThreeSymbol

Equations

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

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✝

@[implicit_reducible]

instance instReprThreeSymbol : Repr ThreeSymbol

Equations

• instReprThreeSymbol = { reprPrec := instReprThreeSymbol.repr }

instance instLawfulBEqThreeSymbol : LawfulBEq ThreeSymbol

def isInLanguage_anbnc (w : List ThreeSymbol) : Bool

The language {aⁿbⁿcⁿ | n ≥ 0}.

Equations

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

def makeString_anbnc (n : ℕ) : List ThreeSymbol

Generate 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 a mathlib Language.

Equations

• anbnc = {w : List ThreeSymbol | isInLanguage_anbnc w = true}

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. Mirror of mem_anbncndn_iff; consumed by the homomorphic reduction aⁿbⁿcⁿdⁿ → aⁿbⁿcⁿ in AnBnCnDn.

theorem anbnc_not_pumpable : ¬HasCFLPumpingProperty anbnc

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

theorem anbnc_not_contextFree : ¬anbnc.IsContextFree

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