The pumping lemma for linear languages

A linear language L has a constant p such that every w ∈ L with |w| ≥ p can be written w = u v x y z with v y nonempty, |u v y z| ≤ p (the pumped pieces and outer pieces are confined to the two ends), and u vⁱ x yⁱ z ∈ L for all i.

The decisive difference from the context-free pumping lemma is the bound: here the outer material u v y z is bounded, forcing v to lie near the start of w and y near its end.

theorem exists_pump_indices {α : Type u_1} [DecidableEq α] (S : Finset α) (root : ℕ → α) (cnt : ℕ → ℕ) (c : ℕ) (hroot : ∀ (k : ℕ), root k ∈ S) (hmono : Monotone cnt) (hstep : ∀ (k : ℕ), cnt (k + 1) ≤ cnt k + c) (h0 : cnt 0 = 0) (N : ℕ) (hN : S.card * (c + 1) ≤ cnt N) : ∃ (i : ℕ) (j : ℕ), i < j ∧ root i = root j ∧ cnt i < cnt j ∧ cnt j ≤ (S.card + 1) * (c + 1)

Pigeonhole core. Given a "root" colouring landing in a finite set S, a monotone "count" with bounded increments starting at 0, and a depth N whose count is at least S.card * (c+1), there are two depths i < j with the same root, strictly increasing count, and cnt j ≤ (S.card + 1) * (c + 1).

theorem deri_ctx {T : Type} {g : grammar T} {C : g.nt} {β p q : List (symbol T g.nt)} (h : grammar_derives g [symbol.nonterminal C] β) : grammar_derives g (p ++ [symbol.nonterminal C] ++ q) (p ++ β ++ q)

A derivation C ⇒* β can be performed inside a terminal context p · q.

theorem pump_derives {T : Type} {g : grammar T} {C : g.nt} {v x : List T} (h : grammar_derives g [symbol.nonterminal C] (List.map symbol.terminal v ++ [symbol.nonterminal C] ++ List.map symbol.terminal x)) (n : ℕ) : grammar_derives g [symbol.nonterminal C] (List.map symbol.terminal (v ^+^ n) ++ [symbol.nonterminal C] ++ List.map symbol.terminal (x ^+^ n))

Iterating a self-embedding derivation C ⇒* v · C · x pumps both ends.

theorem is_Linear.pumping {T : Type} {L : Language T} (hL : is_Linear L) : ∃ (p : ℕ), ∀ w ∈ L, w.length ≥ p → ∃ (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 ∧ (u ++ v ++ y ++ z).length ≤ p ∧ ∀ (n : ℕ), u ++ v ^+^ n ++ x ++ y ^+^ n ++ z ∈ L

Pumping lemma for linear languages. Every linear language L has a constant p such that any w ∈ L with |w| ≥ p factors as w = u v x y z with v y nonempty, the outer material u v y z bounded by p, and u vⁱ x yⁱ z ∈ L for all i.