Theorems · Theorem · computer science

DFA.pumping_lemma

∀ {α : Type u} {σ : Type v} (M : DFA α σ) [inst : Fintype σ] {x : List α},
  x ∈ M.accepts →
    Fintype.card σ ≤ x.length →
      ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * KStar.kstar {b} * {c} ≤ M.accepts

Defined in

Mathlib.Computability.DFA

Cited by

1 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fintype