TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09

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 and its exact reachability invariant

Statement

Let $N = (Q, Σ, δ, q_{0}, F)$ be an epsilon-NFA, with $E = ECl$ and $\hat{δ}$ as in Epsilon-NFAs, finite epsilon closure, and extended word transition. Define $D_{N} = (P (Q), Σ, μ, S_{0}, G), S_{0} = E ({q_{0}}), G = {T \subseteq Q : T \cap F \neq \emptyset},$ $μ (T, a) = E (⋃_{q \in T} δ (q, a)) .$ This is a total DFA with $2^{∣ Q ∣}$ states. Its extended transition satisfies, for every $S \subseteq Q$ and $w \in Σ^{*}$ , $μ^{*} (E (S), w) = \hat{δ} (S, w) .$ In particular $μ^{*} (S_{0}, w) = \hat{δ} (q_{0}, w)$ and $L (D_{N}) = L (N)$ . The empty subset is a legitimate absorbing state, whether or not it is reachable from $S_{0}$ .

Facts & Assumptions

Given: The epsilon-NFA $N$ above, and the displayed definitions of $μ, S_{0}, G$ .

[F1]

Epsilon closure maps subsets to subsets, has $E (\emptyset) = \emptyset$ , and the NFA word transition satisfies the initial and successor equations and the final-set intersection test (Epsilon-NFAs, finite epsilon closure, and extended word transition).

[F2]

For finite $Q$ , its power set is finite with cardinality $2^{∣ Q ∣}$ ( $∣ P (A) ∣ = 2^{∣ A ∣}$ for finite $A$ ).

[F3]

A DFA requires a finite state set, an element chosen as start, a subset of accepting states, and a total letter transition into its state set (Deterministic finite automata).

[F4]

Every DFA has a unique extended transition with $d^{*} (q, ε) = q$ and $d^{*} (q, u a) = d (d^{*} (q, u), a)$ (The extended transition function exists and is unique).

[F5]

A DFA accepts $w$ exactly when its extended transition from the start belongs to its accepting set (Acceptance of a word by a DFA and the recognized language).

[F6]

Zero and successor establish a property for every natural length (The principle of mathematical induction).

Proof

1.1

Since $Q$ is finite, $P (Q)$ is finite with $2^{∣ Q ∣}$ elements. It is nonempty because $\emptyset \subseteq Q$ . For every $T \subseteq Q$ and $a \in Σ$ , all $δ (q, a)$ lie in $P (Q)$ , so their union and its closure are subsets of $Q$ . Thus $μ$ is defined on all $P (Q) \times Σ$ and takes values in $P (Q)$ . Moreover $S_{0} \subseteq Q$ and $G \subseteq P (Q)$ . These verify the DFA hypotheses and give its extended transition $μ^{*}$ .

F1F2F3F4

1.2

Fix any $S \subseteq Q$ . At length zero, $μ^{*} (E (S), ε) = E (S) = \hat{δ} (S, ε)$ . This includes $S = \emptyset$ and subsets that are not epsilon-closed.

F1F4base

1.3

Assume the equality holds for every word $u$ of length $k$ , and write a word of length $k + 1$ uniquely as $u a$ . Then $μ^{*} (E (S), u a) = μ (μ^{*} (E (S), u), a) = μ (\hat{δ} (S, u), a) = E (⋃_{q \in \hat{δ} (S, u)} δ (q, a)) = \hat{δ} (S, u a)$ . The second equality uses the induction hypothesis, and the last uses the NFA recursion.

F1F4ihgiven

2.1

Induction on length proves the equality for every $w$ ; since $S$ was arbitrary, it holds for every subset. Taking $S = {q_{0}}$ gives $μ^{*} (S_{0}, w) = \hat{δ} (q_{0}, w)$ .

step 1.2step 1.3F6discharge-induction

3.1

If $D_{N}$ accepts $w$ , then $μ^{*} (S_{0}, w) \in G$ , so $\hat{δ} (q_{0}, w) \cap F \neq \emptyset$ and $N$ accepts $w$ . Conversely if $N$ accepts $w$ , that intersection is nonempty, so $μ^{*} (S_{0}, w) \in G$ and $D_{N}$ accepts $w$ . This proves equality of the two languages, also for $F = \emptyset$ (neither accepts) and $F = Q$ (acceptance is exactly nonemptiness of the reached subset).

step 2.1F1F5given

4.1

For any letter $a$ , the union indexed by the empty set is empty, whence $μ (\emptyset, a) = E (\emptyset) = \emptyset$ . Its extended transition stays empty: the empty-word value is empty, and if the value at $u$ is empty, the successor value is $μ (\emptyset, a) = \emptyset$ . Induction gives absorption for every word. If $Σ = \emptyset$ , the transition has empty domain and the same empty-word calculation applies; a one-state $Q$ causes no exception to the power-set count or the proof.

F1F4F6step 1.1step 3.1discharge-induction∎

Source conventions

Aho, Lecture 3 §2 uses the full power set as here. Gallier, §3.5, pp. 33–34 restricts to epsilon-closed subsets. Our invariant starts at $E (S)$ ; replacing that by an arbitrary unclosed $S$ would already make the empty-word equality false. No minimization claim is made.

Depends on

Used by

Dropping epsilon closure changes the accepted language Counterexample
A complete determinisation table for a three-state epsilon-NFA Example

Dependency tree · two levels

28 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, Introduction to the Theory of Computation (2018), §§3.3–3.5 (standard reference, not scraped)
Alfred Aho, COMS W3261 Lecture 3, §§1–2 (standard reference, not scraped)