[proofplan] Given a nondeterministic automaton $N = (\Sigma, Q, \delta, q_0, F)$, we perform the *subset construction*: build a deterministic automaton $D$ whose states are subsets of $Q$, whose start state is $\{q_0\}$, and whose transition function collects all possible $N$-transitions from every state in the current subset. The accepting subsets are those that intersect $F$. The correctness proof rests on one structural observation, proved by induction on $|w|$: the single deterministic state of $D$ reached after reading $w$ is exactly the *set* of all $N$-states that some nondeterministic run on $w$ could reach. Acceptance in $N$ (some run ends in $F$) and acceptance in $D$ (the reached subset intersects $F$) are then two phrasings of the same condition, giving $\mathcal{L}(N) = \mathcal{L}(D)$. [/proofplan]

[step:Construct the deterministic automaton $D$ via the subset construction] Fix the nondeterministic automaton \begin{align*} N &= (\Sigma, Q, \delta, q_0, F), \end{align*} where the transition function has signature $\delta: Q \times \Sigma \to \mathcal{P}(Q)$. Extend $\delta$ to the extended nondeterministic transition function $\hat{\delta}: \mathcal{P}(Q) \times \Sigma^\star \to \mathcal{P}(Q)$ in the usual way: $\hat{\delta}(X, \varepsilon) = X$, and $\hat{\delta}(X, wa) = \bigcup_{q \in \hat{\delta}(X, w)} \delta(q, a)$; write $\hat{\delta}(q, w)$ for $\hat{\delta}(\{q\}, w)$. Recall $w \in \mathcal{L}(N) \iff \hat{\delta}(q_0, w) \cap F \neq \varnothing$. Define the [deterministic automaton](/theorems/???) \begin{align*} D &:= (\Sigma,\ \mathcal{P}(Q),\ \Delta,\ \{q_0\},\ G), \end{align*} where the state set is the power set $\mathcal{P}(Q)$, the start state is the singleton $\{q_0\}$, and the transition function and accepting set are \begin{align*} \Delta: \mathcal{P}(Q) \times \Sigma &\to \mathcal{P}(Q), & \Delta(X, a) &:= \bigcup_{q \in X} \delta(q, a), \\ G &\subseteq \mathcal{P}(Q), & G &:= \{X \in \mathcal{P}(Q) : X \cap F \neq \varnothing\}. \end{align*} The map $\Delta$ is single-valued (for each $(X, a)$, the right-hand side is a specific subset of $Q$), so $D$ is deterministic. Since $\mathcal{P}(Q)$ is finite (with $|\mathcal{P}(Q)| = 2^{|Q|}$), $D$ is a finite deterministic automaton. Let $\hat{\Delta}: \mathcal{P}(Q) \times \Sigma^\star \to \mathcal{P}(Q)$ be its extended transition function: $\hat{\Delta}(X, \varepsilon) = X$, and $\hat{\Delta}(X, wa) = \Delta(\hat{\Delta}(X, w), a)$. [/step]

[step:Prove $\hat{\Delta}(\{q_0\}, w) = \hat{\delta}(q_0, w)$ by induction on $|w|$] [claim:For every $X \in \mathcal{P}(Q)$ and every $w \in \Sigma^\star$, $\hat{\Delta}(X, w) = \hat{\delta}(X, w)$] We induct on $|w|$. *Base case*, $w = \varepsilon$. By definition, $\hat{\Delta}(X, \varepsilon) = X = \hat{\delta}(X, \varepsilon)$. *Inductive step.* Fix $n \geq 0$ and suppose the identity holds for every word of length $n$. Let $w \in \Sigma^\star$ have length $n + 1$, and write $w = ua$ with $|u| = n$, $a \in \Sigma$. By the recursive definition of $\hat{\Delta}$, \begin{align*} \hat{\Delta}(X, ua) &= \Delta(\hat{\Delta}(X, u), a) = \bigcup_{q \in \hat{\Delta}(X, u)} \delta(q, a), \end{align*} using the definition $\Delta(Y, a) = \bigcup_{q \in Y} \delta(q, a)$ in the second equality. By the inductive hypothesis applied to $u$ (of length $n$), $\hat{\Delta}(X, u) = \hat{\delta}(X, u)$. Substituting, \begin{align*} \hat{\Delta}(X, ua) &= \bigcup_{q \in \hat{\delta}(X, u)} \delta(q, a) = \hat{\delta}(X, ua), \end{align*} using the recursive definition of the extended nondeterministic transition function $\hat{\delta}(X, ua) = \bigcup_{q \in \hat{\delta}(X, u)} \delta(q, a)$ in the last equality. This closes the induction. [/claim] [proof] See the inductive argument stated in the claim. [/proof] Specialising to $X = \{q_0\}$, for every $w \in \Sigma^\star$, \begin{align*} \hat{\Delta}(\{q_0\}, w) &= \hat{\delta}(\{q_0\}, w) = \hat{\delta}(q_0, w). \end{align*} The second equality is notation: $\hat{\delta}(q_0, w)$ denotes $\hat{\delta}(\{q_0\}, w)$, the set of $N$-states reachable from $q_0$ by reading $w$. [/step]

[step:Translate acceptance in $D$ into acceptance in $N$ via the accepting set $G$]Fix $w \in \Sigma^\star$. We chain the defining equivalences of $\mathcal{L}(D)$ and $\mathcal{L}(N)$ through the identity from the previous step: \begin{align*} w \in \mathcal{L}(D) &\iff \hat{\Delta}(\{q_0\}, w) \in G && \text{(definition of } \mathcal{L}(D)\text{)} \\ &\iff \hat{\Delta}(\{q_0\}, w) \cap F \neq \varnothing && \text{(definition of } G\text{)} \\ &\iff \hat{\delta}(q_0, w) \cap F \neq \varnothing && \text{(previous step)} \\ &\iff w \in \mathcal{L}(N). && \text{(definition of } \mathcal{L}(N)\text{)} \end{align*} The second biconditional unpacks membership in $G = \{X \in \mathcal{P}(Q) : X \cap F \neq \varnothing\}$ applied to $X := \hat{\Delta}(\{q_0\}, w)$. The third substitutes the identity from the previous step. Since the chain holds for every $w \in \Sigma^\star$, we conclude $\mathcal{L}(N) = \mathcal{L}(D)$.[/step]

[guided]The subset construction is the classical way to "determinise" a nondeterministic automaton, and the key intuition is this: a nondeterministic run on $w$ is really a branching tree of possible state sequences. At each step, every state the nondeterminism could currently be in gives rise to a fan-out of next states (via $\delta(q, a)$). The *set* of all states the nondeterminism could reach after reading a prefix $w$ is a well-defined object that evolves deterministically: given the current reachable set $X$ and the next letter $a$, the next reachable set is $\bigcup_{q \in X} \delta(q, a)$. This is exactly the deterministic transition $\Delta(X, a)$. So the deterministic automaton $D$ tracks the "frontier" of the nondeterministic computation of $N$ — in a single deterministic state, it encodes *all* the possibilities that $N$ could be pursuing simultaneously. The state space grows to $\mathcal{P}(Q)$ (size $2^{|Q|}$), which is the cost of determinisation; this blow-up is not a proof artefact but a genuine phenomenon — in the worst case, no smaller deterministic automaton suffices. To formalise "the state of $D$ after reading $w$ is the set of reachable $N$-states after reading $w$", we induct on $|w|$: - For $w = \varepsilon$, the state of $D$ is its start state $\{q_0\}$, and the set of $N$-states reachable via the empty word from $q_0$ is $\{q_0\}$. They match. - For $w = ua$, we assume by induction that after reading $u$, $D$ is in state $\hat{\delta}(q_0, u)$. Reading $a$ from this state, $D$ transitions to $\Delta(\hat{\delta}(q_0, u), a) = \bigcup_{q \in \hat{\delta}(q_0, u)} \delta(q, a)$. But this is precisely the definition of $\hat{\delta}(q_0, ua)$ via its recursive clause: the nondeterministic transition function unfolds to the same union. So the identity propagates from $u$ to $ua$. Once we know the state of $D$ after reading $w$ is the set of $N$-reachable states, the two notions of acceptance become tautologically equivalent. $N$ accepts $w$ iff *some* $N$-state reachable from $q_0$ via $w$ lies in $F$ (that is, $\hat{\delta}(q_0, w) \cap F \neq \varnothing$). $D$ accepts $w$ iff its single state after reading $w$ lies in its accepting set $G$, which was defined as the collection of subsets $X \subseteq Q$ with $X \cap F \neq \varnothing$. The accepting sets $G$ of $D$ are the *answer to the reachability question about $F$* — they encode: "does any state of the nondeterministic frontier land in $F$?" Every design choice in the construction is forced by this logic. The state set $\mathcal{P}(Q)$: because we must track arbitrary frontiers. The start state $\{q_0\}$: because at time zero the nondeterminism has not fanned out yet. The transition $\Delta(X, a) = \bigcup_{q \in X} \delta(q, a)$: because that is how the frontier evolves. The accepting set $G$: because $N$-acceptance is "frontier meets $F$".[/guided]

[step:State the conclusion] We have exhibited a deterministic automaton $D$ over the same alphabet $\Sigma$ with $\mathcal{L}(D) = \mathcal{L}(N)$. Since $N$ was an arbitrary nondeterministic automaton, this establishes the equivalence: for every nondeterministic automaton there exists a deterministic one recognising the same language. This completes the proof. [/step]