English
For a DFA with finite states and a sufficiently long accepted word x, there exist a decomposition x = a b c with a b nonempty and a b length bounded by the number of states, such that a b^* c is also accepted. This yields a standard pumping argument.
Русский
Для ДФА с конечным числом состояний и длинного принятого слова x существует разложение x = a b c с ненулевой частью b и ограниченной длиной a b, чтобы a b^* c тоже принималось. Это классический pumping-аргумент.
LaTeX
$$$\exists a,b,c \; x = a++b++c \land |a|+|b| \le |\sigma| \land b \neq \emptyset \land (\{a\} \cdot \{b\}^{*} \cdot \{c\}) \le M.accepts$$$
Lean4
theorem pumping_lemma [Fintype σ] {x : List α} (hx : x ∈ M.accepts) (hlen : Fintype.card σ ≤ List.length x) :
∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ { a } * { b }∗ * { c } ≤ M.accepts :=
by
obtain ⟨_, a, b, c, hx, hlen, hnil, rfl, hb, hc⟩ := M.evalFrom_split (s := M.start) hlen rfl
use a, b, c, hx, hlen, hnil
intro y hy
rw [Language.mem_mul] at hy
rcases hy with ⟨ab, hab, c', hc', rfl⟩
rw [Language.mem_mul] at hab
rcases hab with ⟨a', ha', b', hb', rfl⟩
rw [Set.mem_singleton_iff] at ha' hc'
substs ha' hc'
have h := M.evalFrom_of_pow hb hb'
rwa [mem_accepts, eval, evalFrom_of_append, evalFrom_of_append, h, hc]
