English
For an NFA M with alphabet σ, any sufficiently long word x accepted by M can be decomposed as x = a b c with b nonempty and the pumped words a b^k c belong to the language for all k ≥ 0, with a bound depending on |Set σ|.
Русский
Для НКА M над алфавитом σ любое достаточно длинное слово x, принимаемое M, может быть разложено как x = a b c, при этом b не пусто и слова a b^k c принадлежат языку для всех k ≥ 0, с ограничением, зависящим от |Set σ|.
LaTeX
$$$\forall [inst : Fintype \sigma] \; {x : List \alpha},\; x \in M.accepts \Rightarrow \exists a,b,c, x = a \cdot b \cdot c \wedge |a|+|b| \le |Set\,\sigma| \wedge b \neq \emptyset \wedge \{ a \} \cdot \{ b \}^* \cdot \{ c \} \subseteq 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 :=
by
rw [← toDFA_correct] at hx ⊢
exact M.toDFA.pumping_lemma hx hlen
