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

The two-parameter relaxation of anbncndn: case-sorted strings with a-count = c-count and b-count = d-count (the diagonal pairs only — not all four counts equal). Strict superset of anbncndn; this is the language @cite{shieber-1985}'s argument that Swiss German is not weakly context-free actually requires.

Pumping

The witness is the diagonal makeString_anbncndn p (which lies in ambncmdn, since equal-all-four implies the diagonal pairs match). Pumping breaks one of the two diagonal equalities rather than all four — hence the substantive content of this file beyond AnBnCnDn.

The proof uses the shared adjacency lemmas (not_a_and_c_in_vxy, not_b_and_d_in_vxy) and filter machinery (filter_count, filter_eq_nil_of_not_mem, fourSymbol_filter_total) re-exported from AnBnCnDn.

def isInLanguage_ambncmdn (w : FourString) : Bool

The language {aᵐbⁿcᵐdⁿ | m, n ≥ 0}: case-sorted strings with a-count = c-count and b-count = d-count. Membership requires the case-sorted shape AND the two diagonal-count equalities.

Equations

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

def makeString_ambncmdn (m n : ℕ) : FourString

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

Equations

• ambncmdn = {w : List FourSymbol | isInLanguage_ambncmdn w = true}

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

The diagonal witness makeString_anbncndn n lies in ambncmdn (since na = nb = nc = nd = n satisfies the weaker na = nc ∧ nb = nd).

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

Asymmetric witness makeString_ambncmdn m n lies in ambncmdn.

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 pump_breaks_ambncmdn (p : ℕ) (_hp : p > 0) : have w := makeString_anbncndn p; ∀ (u v x y z : FourString), w = 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. The witness is the diagonal makeString_anbncndn p. Deleting v and y must break either the a-count = c-count equality or the b-count = d-count equality, depending on which two adjacent blocks vxy intersects.

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 @cite{shieber-1985}'s Swiss German argument actually requires.