Elementary Pumping Lemmas

This file states the context-free pumping lemma for the project's is_CF predicate. CF_pumping transports Language.IsContextFree.pumping (proved in Pumping/Pumping.lean via Chomsky-normal-form parse trees) across is_CF_iff_isContextFree.

Main declarations

• CF_pumping

theorem CF_pumping {T : Type} {L : Language T} (cf : is_CF L) : ∃ (n : ℕ), ∀ w ∈ L, w.length ≥ n → ∃ (u : List T) (v : List T) (x : List T) (y : List T) (z : List T), w = u ++ v ++ x ++ y ++ z ∧ (v ++ y).length > 0 ∧ (v ++ x ++ y).length ≤ n ∧ ∀ (i : ℕ), u ++ v ^ i ++ x ++ y ^ i ++ z ∈ L

Pumping lemma for context-free languages.