nfa_accepts_is_regular
theoremverified
The language accepted by any finite-state nondeterministic finite automaton is regular.
Statement
theorem nfa_accepts_is_regular {α : Type*} {σ : Type*} [Fintype σ] (M : NFA α σ) : M.accepts.IsRegular
- Source
- Sipser, Corollary 1.40
- Verified
- 07 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext
Read back from the Lean
For any types α and σ, where σ is a finite type ([Fintype σ]), and for any nondeterministic finite automaton M : NFA α σ, the language accepted by M (M.accepts) is regular (Language.IsRegular).
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- The language accepted by any finite-state nondeterministic finite automaton is regular. -/ theorem nfa_accepts_is_regular {α : Type*} {σ : Type*} [Fintype σ] (M : NFA α σ) : M.accepts.IsRegular := Language.isRegular_iff.2 ⟨Set σ, inferInstance, M.toDFA, NFA.toDFA_correct⟩