structure Sipser.NFA (Q : Type u_1) (σ : Type u_2) [DecidableEq Q] : Type (max u_1 u_2)

Nondeterministic Finite Automaton (Sipser-style).

An NFA is a 5-tuple (Q, Σ, δ, q₀, F) where Q is a finite set of states, Σ an alphabet, q₀ ∈ Q the start state, F ⊆ Q the accept states, and δ : Q × Σ_ε → 𝒫(Q) the transition function (where Σ_ε = Σ ∪ {ε}).

Here δ q (some a) gives the transitions on input symbol a, while δ q none gives the ε-transitions. Successor sets are represented as Finset Q. The alphabet Σ and the implicit Q are tracked by the type parameters.

• δ : Q → Option σ → Finset Q
• q₀ : Q
• accept : Finset Q

def Sipser.NFA.toεNFA {Q : Type u_1} {σ : Type u_2} [DecidableEq Q] (M : NFA Q σ) : εNFA σ Q

Convert a Sipser-style NFA into Mathlib's εNFA σ Q by coercing each finset of successor states to a Set, and packaging the singleton start set {q₀} and accept set F.

def Sipser.NFA.εClosure {Q : Type u_1} {σ : Type u_2} [DecidableEq Q] (M : NFA Q σ) (S : Set Q) : Set Q

The ε-closure of a set of states S ⊆ Q: all states reachable from S by zero or more ε-transitions.

def Sipser.NFA.accepts {Q : Type u_1} {σ : Type u_2} [DecidableEq Q] (M : NFA Q σ) (w : List σ) : Prop

M accepts the input word w iff some computation branch of the underlying ε-NFA reaches an accept state after reading w.

def Sipser.NFA.language {Q : Type u_1} {σ : Type u_2} [DecidableEq Q] (M : NFA Q σ) : Language σ

The language recognized by an NFA M: the set of words it accepts.

theorem Sipser.NFA.language_eq_toεNFA_accepts {Q : Type u_1} {σ : Type u_2} [DecidableEq Q] (M : NFA Q σ) : M.language = M.toεNFA.accepts

The language of M is, by definition, the accepting language of the underlying Mathlib εNFA.

theorem Sipser.NFA.language_isRegular {Q : Type u_1} {σ : Type u_2} [DecidableEq Q] [Fintype Q] (M : NFA Q σ) : M.language.IsRegular

NFA to DFA conversion (Sipser). If an NFA M with finite state space Q recognizes a language A, then A is regular.

The proof passes through Mathlib's εNFA → NFA → DFA subset construction: the resulting DFA has state space Set Q, which is finite since Q is.