[proofplan] Given a deterministic automaton $D = (\Sigma, Q, \delta, q_0, F)$, we exhibit a regular grammar $G$ with $\mathcal{L}(G) = \mathcal{L}(D)$. The construction takes states of $D$ as variables of $G$ and converts each transition $\delta(p, a) = q$ into a regular rule: a nonterminal rule $p \to aq$ in general, and additionally a terminal rule $p \to a$ whenever $q \in F$ (so the derivation can finish by "landing" in an accepting state on the next letter). The key technical bridge is an induction on word length that puts state sequences of $D$-runs in bijection with $G$-derivations: the state $q_{i+1} = \delta(q_i, a_i)$ corresponds to the rule $q_i \to a_i q_{i+1}$, and the final accept step $q_{n+1} \in F$ triggered by the letter $a_n$ corresponds to the terminal rule $q_n \to a_n$. The [Structure of Terminal Derivations](/theorems/1787) theorem tells us every $G$-derivation of a terminal word has exactly this shape — $|w| - 1$ nonterminal rules followed by a single terminal rule — so no extraneous derivations exist. The two directions combine to give $\mathcal{L}(D) = \mathcal{L}(G)$, and since $G$ is regular by construction, $\mathcal{L}(D)$ is a regular language. [/proofplan]

[step:Construct the regular grammar $G$ from the automaton $D$] Fix the deterministic automaton $D = (\Sigma, Q, \delta, q_0, F)$. Define the grammar \begin{align*} G &:= (\Sigma, Q, P, q_0), \end{align*} where the variable set is $Q$ (states of $D$ become nonterminals of $G$), the start variable is $q_0$, and the production set is \begin{align*} P &:= \{p \to aq : p, q \in Q,\ a \in \Sigma,\ \delta(p, a) = q\} \cup \{p \to a : p \in Q,\ a \in \Sigma,\ \delta(p, a) \in F\}. \end{align*} We verify that $G$ is a regular grammar. Every rule of $P$ has one of the two regular shapes: rules in the first set have the nonterminal shape $A \to aB$ (with $A = p$, $B = q \in Q = V$, $a \in \Sigma$), and rules in the second set have the terminal shape $A \to a$ (with $A = p \in V$, $a \in \Sigma$). The start variable $q_0 \in Q$ lies in the variable set. Hence $G$ is regular. [/step]

[step:Translate an accepting run of $D$ into a $G$-derivation] Let $w \in \mathcal{L}(D)$; we show $w \in \mathcal{L}(G)$. Since $w$ is accepted by $D$, it has length $|w| \geq 1$ (the empty word is accepted only when $q_0 \in F$, but even then $\mathcal{L}(D)$ may or may not contain $\varepsilon$; we address $\varepsilon$ separately below). Write $w = a_0 a_1 \cdots a_n$ with $n = |w| - 1 \geq 0$ and each $a_i \in \Sigma$. Define the run of $D$ on $w$ as the state sequence \begin{align*} q_0,\ q_1,\ \dots,\ q_{n+1}, \qquad q_{i+1} := \delta(q_i, a_i) \text{ for } i = 0, 1, \dots, n. \end{align*} (Here $q_0$ on the right is the start state of $D$, already fixed by the definition of $D$, matching our notation above.) By the [extended transition function](/theorems/???) computation, $\hat{\delta}(q_0, w) = q_{n+1}$. Since $w \in \mathcal{L}(D)$, $q_{n+1} \in F$. We construct a $G$-derivation of $w$ from $q_0$ in $|w|$ steps. *First $n$ steps (nonterminal rules).* For each $i = 0, 1, \dots, n - 1$, the transition $\delta(q_i, a_i) = q_{i+1}$ supplies the $G$-rule $q_i \to a_i q_{i+1} \in P$. Applying these rules in order, starting from $q_0$: \begin{align*} q_0 &\to_G a_0 q_1 \to_G a_0 a_1 q_2 \to_G \cdots \to_G a_0 a_1 \cdots a_{n-1} q_n. \end{align*} Each step rewrites the unique trailing variable, using the nonterminal rule corresponding to the next transition of $D$. *Final step (terminal rule).* The transition $\delta(q_n, a_n) = q_{n+1} \in F$ satisfies the second clause of $P$'s construction, so $q_n \to a_n \in P$. Applying this rule: \begin{align*} a_0 a_1 \cdots a_{n-1} q_n &\to_G a_0 a_1 \cdots a_{n-1} a_n = w. \end{align*} Concatenating, $q_0 \xrightarrow{G} w$, so $w \in \mathcal{L}(G)$. In the degenerate case $|w| = 0$, i.e., $w = \varepsilon$: $\varepsilon \in \mathcal{L}(D)$ requires $q_0 \in F$. But $G$ has no rules with empty right-hand side (every rule in $P$ produces at least one terminal), so $\varepsilon \notin \mathcal{L}(G)$. For this theorem it suffices to observe that this edge case is not part of the construction's target; for the full result one may either (i) restrict attention to $w \neq \varepsilon$ or (ii) extend the grammar to include a rule $q_0 \to \varepsilon$ when $q_0 \in F$ and use the extended notion of regular grammars permitting $\varepsilon$-rules from the start variable. This edge case does not affect the regularity conclusion; we take $w$ with $|w| \geq 1$ henceforth, noting that the regular languages are closed under adjunction of $\{\varepsilon\}$ (see [Closure Under Union](/theorems/???)). Hence $\{w \in \mathcal{L}(D) : |w| \geq 1\} \subseteq \mathcal{L}(G)$. [/step]

[step:Translate a $G$-derivation of $w$ into an accepting run of $D$]Conversely, suppose $w \in \mathcal{L}(G)$ with $|w| \geq 1$. By the [Structure of Terminal Derivations](/theorems/1787) theorem applied to the regular grammar $G$, any $G$-derivation of $w$ from $q_0$ has exactly $|w|$ steps, consisting of $|w| - 1$ nonterminal rules followed by a single terminal rule. Write $w = a_0 a_1 \cdots a_n$ with $n = |w| - 1$ as before. By the shape theorem, the derivation takes the form \begin{align*} q_0 \to_G b_0 A_1 \to_G b_0 b_1 A_2 \to_G \cdots \to_G b_0 b_1 \cdots b_{n-1} A_n \to_G b_0 b_1 \cdots b_{n-1} b_n = w, \end{align*} where $A_1, A_2, \dots, A_n \in Q$ are variables (nonterminals of $G$, i.e., states of $D$), the first $n$ steps use nonterminal rules $A_{i-1} \to b_{i-1} A_i$ (with $A_0 := q_0$), and the final step uses a terminal rule $A_n \to b_n$. Matching against $w = a_0 a_1 \cdots a_n$, we read off $b_i = a_i$ for $i = 0, 1, \dots, n$. We decode each rule back into a $D$-transition: - The nonterminal rule $A_{i-1} \to a_{i-1} A_i$ (used at step $i - 1$ for $i = 1, \dots, n$) lies in $P$'s first clause, so $\delta(A_{i-1}, a_{i-1}) = A_i$. Setting $q_i := A_i$ for $i = 0, 1, \dots, n$ (with $q_0 = A_0$ matching the start state), we have $q_{i+1} = A_{i+1} = \delta(A_i, a_i) = \delta(q_i, a_i)$ for $i = 0, \dots, n - 1$. - The terminal rule $A_n \to a_n$ (used at step $n$) lies in $P$'s second clause, so $\delta(A_n, a_n) \in F$. Setting $q_{n+1} := \delta(q_n, a_n)$, we have $q_{n+1} \in F$. Hence the sequence $q_0, q_1, \dots, q_{n+1}$ is the run of $D$ on $w$, and $q_{n+1} = \hat{\delta}(q_0, w) \in F$. This establishes $w \in \mathcal{L}(D)$. Hence $\mathcal{L}(G) \subseteq \{w \in \mathcal{L}(D) : |w| \geq 1\}$.[/step]

[guided]The correspondence between a $G$-derivation and a $D$-run is tight enough to deserve a direct examination. The rules of $G$ were crafted so that reading a transition $\delta(p, a) = q$ of $D$ is exactly the same as applying the rule $p \to aq$ of $G$. The only subtlety is the terminal step: in a $G$-derivation, the derivation must end with a terminal rule (by the [Structure of Terminal Derivations](/theorems/1787) theorem, the very last step of any $G$-derivation of a terminal word is a $p \to a$ rule), and by construction of $P$, such a rule exists in $G$ precisely when the corresponding transition $\delta(p, a) \in F$ — that is, when $D$ is about to enter an accepting state. The "end the derivation" event in $G$ thus corresponds exactly to the "accept by landing in $F$" event in $D$. For the reverse direction, why do we invoke the [Structure of Terminal Derivations](/theorems/1787) theorem? Because without it we would have to rule out exotic $G$-derivations — perhaps ones in which a terminal rule fires early and leaves trailing variables that somehow disappear, or ones with multiple terminal rules. But regular grammars are structurally rigid: the shape theorem forces every derivation of a terminal string to have the form "a chain of nonterminal rules extending the word one letter at a time with a single trailing variable, terminated by exactly one terminal rule at the end". This rigidity is what makes the decoding unambiguous. Once the shape is fixed, each rule of the $G$-derivation determines a transition of $D$: nonterminal rules $A_{i-1} \to a_{i-1} A_i$ unambiguously encode the transitions $\delta(A_{i-1}, a_{i-1}) = A_i$ by inspection of $P$'s first clause, and the terminal rule $A_n \to a_n$ encodes the final transition $\delta(A_n, a_n) \in F$ by inspection of $P$'s second clause. Reassembling the $A_i$ into the state sequence $q_0 = A_0, q_1 = A_1, \dots, q_n = A_n, q_{n+1} = \delta(A_n, a_n)$, we see this sequence is precisely the unique run of $D$ on $w$, and this run ends in $F$. The shape theorem also plays a decisive role in a failure mode we must rule out: could there be a $G$-derivation of $w$ that does not correspond to any $D$-run? The answer is no, because the shape theorem says the derivation must have exactly $|w| - 1$ nonterminal rules followed by a single terminal rule. This forces the $A_i$'s to form a sequence of $D$-states in which each successive pair is linked by a $D$-transition, as encoded by the rule used at that step. There is no freedom left.[/guided]

[step:Handle the empty-word case and combine the two inclusions] Combining the previous two steps, \begin{align*} \mathcal{L}(G) &= \{w \in \mathcal{L}(D) : |w| \geq 1\}. \end{align*} If $\varepsilon \notin \mathcal{L}(D)$, this already equals $\mathcal{L}(D)$, and we set $G_{\text{final}} := G$. If $\varepsilon \in \mathcal{L}(D)$ (equivalently, $q_0 \in F$), we form $G_{\text{final}}$ by extending the class of regular grammars to allow the single additional rule $q_0 \to \varepsilon$ (permissible because it acts only on the start variable; see the [regular grammar](/theorems/???) definition, which allows this extension without loss of regularity). The modified grammar generates all strings in $\mathcal{L}(G)$ plus the empty string, matching $\mathcal{L}(D)$ exactly. In either case, $\mathcal{L}(G_{\text{final}}) = \mathcal{L}(D)$, and $G_{\text{final}}$ is a regular grammar. Therefore $\mathcal{L}(D)$ is a regular language. This completes the proof. [/step]