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

The two-parameter relaxation of anbncndn: case-sorted strings whose a- and c-counts agree and whose b- and d-counts agree — the diagonal pairs only, not all four counts equal. A strict superset of anbncndn, and the language [Shi85]'s argument that Swiss German is not weakly context-free actually requires.

Pumping runs on the diagonal witness makeString_anbncndn p, which lies in ambncmdn because equal-all-four implies the diagonal pairs match. Deleting the pumped window breaks one of the two diagonal equalities rather than all four — the substantive content beyond AnBnCnDn.

Main definitions

• makeString_ambncmdn m n: the witness word aᵐbⁿcᵐdⁿ.
• ambncmdn: the language {aᵐbⁿcᵐdⁿ | m, n ≥ 0}, as the range of makeString_ambncmdn.

Main results

• ambncmdn_not_pumpable: ambncmdn lacks the CFL pumping property.
• ambncmdn_not_contextFree: ambncmdn is not context-free.

def makeString_ambncmdn (m n : ℕ) : FourString

The witness word aᵐbⁿcᵐdⁿ.

Equations

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

def ambncmdn : Language FourSymbol

The language {aᵐbⁿcᵐdⁿ | m, n ≥ 0}, as the range of makeString_ambncmdn.

Equations

• ambncmdn = {w : List FourSymbol | ∃ (m : ℕ) (n : ℕ), w = makeString_ambncmdn m n}

theorem mem_ambncmdn_iff (w : FourString) : w ∈ ambncmdn ↔ ∃ (m : ℕ) (n : ℕ), w = makeString_ambncmdn m n

Membership characterization: every string in ambncmdn equals makeString_ambncmdn m n for some m, n.

theorem makeString_ambncmdn_in_language (m n : ℕ) : makeString_ambncmdn m n ∈ ambncmdn

theorem makeString_anbncndn_in_ambncmdn (n : ℕ) : makeString_anbncndn n ∈ ambncmdn

The diagonal witness lies in ambncmdn: aⁿbⁿcⁿdⁿ is aᵐbⁿcᵐdⁿ at m = n.

@[simp]

theorem count_a_makeString_ambncmdn (m n : ℕ) : List.count FourSymbol.a (makeString_ambncmdn m n) = m

@[simp]

theorem count_b_makeString_ambncmdn (m n : ℕ) : List.count FourSymbol.b (makeString_ambncmdn m n) = n

@[simp]

theorem count_c_makeString_ambncmdn (m n : ℕ) : List.count FourSymbol.c (makeString_ambncmdn m n) = m

@[simp]

theorem count_d_makeString_ambncmdn (m n : ℕ) : List.count FourSymbol.d (makeString_ambncmdn m n) = n

theorem pump_breaks_ambncmdn (p : ℕ) (_hp : 0 < p) (u v x y z : FourString) : makeString_anbncndn p = 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 ∉ ambncmdn

Pumping breaks ambncmdn membership. Deleting v and y must break either the a-count = c-count equality or the b-count = d-count equality, depending on which blocks the window meets.

theorem ambncmdn_not_pumpable : ¬HasCFLPumpingProperty ambncmdn

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

theorem ambncmdn_not_contextFree : ¬ambncmdn.IsContextFree

{aᵐbⁿcᵐdⁿ} is not context-free — the two-parameter relaxation that [Shi85]'s Swiss German argument requires.