TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-31

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.

The subset construction preserves the recognized language

Statement

Let $N$ be an NFA with epsilon-moves, and let $D_{N}$ be its subset-construction DFA. Then $L (D_{N}) = L (N) .$

Facts & Assumptions

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

[L1]

By Subset construction tracks exactly the reachable NFA state set, for every word $w$ the DFA state reached in $D_{N}$ on $w$ is exactly the NFA reachable state set on $w$ .

[L2]

By Acceptance of a word by a DFA and the recognized language, $D_{N}$ accepts $w$ exactly when its reached DFA state is accepting.

[L3]

By Acceptance of a word by an NFA and the recognized language, $N$ accepts $w$ exactly when its reachable state set on $w$ contains an accepting state.

Proof

technique · direct

1.1

Let $w \in Σ^{*}$ . By [L1], the state reached by $D_{N}$ on $w$ is the subset $\hat{δ} (q_{0}, w)$ of NFA states.

L1given

2.1

In the subset construction, a DFA state is accepting exactly when it contains an accepting NFA state. Therefore [L2] and step 1.1 show that $D_{N}$ accepts $w$ exactly when $\hat{δ} (q_{0}, w)$ contains an accepting state.

L2step 1.1

3.1

By [L3], the condition from step 2.1 is exactly the statement that $N$ accepts $w$ . Thus $D_{N}$ accepts precisely the words that $N$ accepts, so $L (D_{N}) = L (N)$ .

L3step 2.1∎

Depends on

Used by

DFAs and NFAs recognize the same languages Corollary

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)