LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-12

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Subset construction tracks exactly the reachable NFA state set

Statement

Let $N = (Q, Σ, δ, q_{0}, F)$ be an NFA with epsilon-moves, and let $D_{N} = (P (Q), Σ, μ, S_{0}, G)$ be its subset-construction DFA.

Then for every word $w \in Σ^{*}$ , $μ^{*} (S_{0}, w) = \hat{δ} (q_{0}, w),$ where $μ^{*}$ is the extended transition of $D_{N}$ .

Facts & Assumptions

Given: An NFA $N$ and its subset-construction DFA $D_{N}$ .

[L1]

By The subset-construction DFA, the start state of $D_{N}$ is $S_{0} = ECl (q_{0})$ and its one-letter transition is $μ (S, a) = ECl (⋃_{q \in S} δ (q, a))$ .

[L2]

By The extended transition function of an NFA, the extended NFA transition satisfies $\hat{δ} (q_{0}, ε) = ECl (q_{0})$ and $\hat{δ} (q_{0}, w a) = ECl (⋃_{q \in \hat{δ} (q_{0}, w)} δ (q, a))$ .

Proof

technique · direct

1.1L1L2givenbase

For the empty word, $μ^{*} (S_{0}, ε) = S_{0}$ by the DFA recursion, while [L1] and [L2] identify both sides with $ECl (q_{0})$ .

1.2given

Fix a successor word of the form $w a$ .

2.1L1step 1.2ih

Assume $μ^{*} (S_{0}, w) = \hat{δ} (q_{0}, w)$ . Then for the successor word from step 1.2 the DFA recursion gives $μ^{*} (S_{0}, w a) = μ (μ^{*} (S_{0}, w), a)$ , so [L1] turns this into $ECl (⋃_{q \in μ^{*} (S_{0}, w)} δ (q, a))$ .

3.1L2step 2.1

Substituting the induction hypothesis into step 2.1 yields $μ^{*} (S_{0}, w a) = ECl (⋃_{q \in \hat{δ} (q_{0}, w)} δ (q, a))$ , and [L2] identifies that set with $\hat{δ} (q_{0}, w a)$ .

4.1step 1.1step 1.2step 2.1step 3.1discharge-induction: on |w|∎

Steps 1.1, 1.2, 2.1, and 3.1 prove by induction on $∣ w ∣$ that $μ^{*} (S_{0}, w) = \hat{δ} (q_{0}, w)$ for every word $w$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jean Gallier and Jocelyn Quaintance, Introduction to the Theory of Computation: Some Notes for CIS511 (standard reference, not scraped)
John Watrous, Introduction to the Theory of Computing, Lecture 3: Nondeterministic finite automata (standard reference, not scraped)