English
If σ is finite and a word x is accepted by M with length at least the cardinality of Set σ, then x can be decomposed as x = a b c with certain length constraints and b nonempty, such that the words a b^i c are all accepted by M for all i ≥ 0.
Русский
Если множество состояний σ конечно, и слово x принимается M и имеет длину не меньше кардинала множества Set σ, то x можно разложить на x = a b c так, что длина a + b не превосходит |Set σ|, b непусто, и для любых i ≥ 0 строка a b^i c принадлежит M.accepts.
LaTeX
$$$x \\in M.accepts \\land |x| \\ge |Set(\\sigma)| \\Rightarrow \\exists a\,b\,c,\; x = a ++ b ++ c \\land a.length + b.length \\le |Set(\\sigma)| \\land b \\neq [] \\land { a } * { b }^* * { c } \\le M.accepts$$$
Lean4
theorem pumping_lemma [Fintype σ] {x : List α} (hx : x ∈ M.accepts) (hlen : Fintype.card (Set σ) ≤ List.length x) :
∃ a b c,
x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ { a } * { b }∗ * { c } ≤ M.accepts :=
M.toNFA.pumping_lemma hx hlen
