[proofplan] Given regular grammars $G, G'$ for $L, L'$ with disjoint variable sets, we construct a regular grammar $H$ for $LL'$ by "chaining": rewrite every terminal rule $A \to a$ in $P$ as the nonterminal rule $A \to aS'$, producing a modified rule set $P^\star$, and let $H$ use $P^\star \cup P'$ with start symbol $S$. The shape and structure theorems for regular sentential forms ([Shape of Regular Sentential Forms](/theorems/1786), [Structure of Terminal Derivations](/theorems/1787)) force every $H$-derivation of a terminal word to begin with rules from $P^\star$ (which act on $V$-variables), transition exactly once from the $V$-phase to the $V'$-phase at the unique step where a $P^\star$-rule of the new form $A \to aS'$ introduces $S'$, and then continue with $P'$-rules (which act on $V'$-variables) until the derivation terminates. This rigid split produces a unique factorisation $u = vw$ with $v \in L$, $w \in L'$, establishing $\mathcal{L}(H) = LL'$; the explicit rule shapes confirm that $H$ is regular. [/proofplan]

[step:Reduce to the case where $L, L'$ are generated by regular grammars with disjoint variables] Since $L$ and $L'$ are regular, pick regular grammars $G = (\Sigma, V, P, S)$ and $G' = (\Sigma, V', P', S')$ with $\mathcal{L}(G) = L$ and $\mathcal{L}(G') = L'$. If $V \cap V' \ne \varnothing$, apply the [renaming theorem](/theorems/???) to $G'$: replace each variable of $V'$ by a fresh symbol disjoint from $V$ (and from $\Sigma$), producing an equivalent regular grammar with disjoint variable alphabet. Renaming variables preserves the structural form of each rule (it only relabels the variable symbols appearing in left- and right-hand sides), so the grammar remains regular. We henceforth assume $V \cap V' = \varnothing$. [/step]

[step:Construct the chained grammar $H$] Define the modified rule set \begin{align*} P^\star &:= \{A \to a S' : (A \to a) \in P\} \cup \{A \to aB : (A \to aB) \in P\}. \end{align*} That is, replace every terminal rule $A \to a$ in $P$ by the rule $A \to a S'$, and keep every nonterminal rule unchanged. Define \begin{align*} H &:= (\Sigma,\; V \cup V',\; P^\star \cup P',\; S). \end{align*} We verify that $H$ is a regular grammar. Every rule of $P^\star \cup P'$ has one of the two regular shapes $A \to a$ or $A \to aB$: rules of the form $A \to aB$ (where $B \in V \cup V'$) already have this shape; rules of the form $A \to aS'$ (the new rules produced from $P$-terminal rules) have this shape with $B := S' \in V'$; rules of $P'$ retain whatever regular shape they had in $G'$. No rule of $P^\star$ has the pure terminal shape $A \to a$, because we replaced all such rules. The rules of $P'$ may include terminal rules $B \to b$ and nonterminal rules $B \to bC$, both regular. Hence every rule of $H$ is regular, and $H$ is a regular grammar with start symbol $S \in V$ (so $S \in V \cup V'$). [/step]

[step:Show $LL' \subseteq \mathcal{L}(H)$] Let $v \in L$ and $w \in L'$. We construct an $H$-derivation of $vw$ from $S$. Since $v \in L = \mathcal{L}(G)$, the [Structure of Terminal Derivations](/theorems/1787) theorem applied to $G$ gives a $G$-derivation \begin{align*} S &= \sigma_0 \to_G \sigma_1 \to_G \cdots \to_G \sigma_{|v|} = v, \end{align*} in which steps $0, 1, \dots, |v| - 2$ use nonterminal rules of $G$ and step $|v| - 1$ uses a terminal rule of $G$. The nonterminal rules of $G$ belong to $P^\star$ (they were kept unchanged). Hence the first $|v| - 1$ steps of the $G$-derivation are also valid $H$-steps. After these steps the current sentential form is $\sigma_{|v|-1}$, which (by the structure theorem) has the shape $v' A$ for some $v' \in \Sigma^{|v|-1}$, $A \in V$, with $v = v' a$ where $a \in \Sigma$ is the terminal produced by the final $G$-step. Concretely, $\sigma_{|v|-1} = v' A$ and the final $G$-step $\sigma_{|v|-1} \to_G \sigma_{|v|} = v$ uses a $G$-terminal rule $A \to a$. Instead of applying $A \to a$, we apply the corresponding $H$-rule $A \to aS' \in P^\star$ to $\sigma_{|v|-1} = v'A$: \begin{align*} v'A &\to_H v'aS' = vS'. \end{align*} Hence $S \xrightarrow{H} vS'$ via the $|v| - 1$ nonterminal $P^\star$-steps followed by one "chaining" $P^\star$-step of shape $A \to aS'$. This uses exactly $|v|$ $H$-steps and produces the sentential form $vS'$. Next, since $w \in L' = \mathcal{L}(G')$, there is a $G'$-derivation $S' \xrightarrow{G'} w$ of length $|w|$. The rules of $G'$ all lie in $P' \subseteq P^\star \cup P'$, so every $G'$-step is an $H$-step (applied with leading context $v \in \Sigma^\star$). Hence \begin{align*} vS' &\xrightarrow{H} vw. \end{align*} Concatenating, $S \xrightarrow{H} vw$, so $vw \in \mathcal{L}(H)$. Hence $LL' \subseteq \mathcal{L}(H)$. [/step]

[step:Record two consequences of the shape theorem applied to $H$] Fix an $H$-derivation $S = \tau_0 \to_H \tau_1 \to_H \cdots \to_H \tau_N = u$ with $u \in \Sigma^\star$. Since $H$ is regular (second step), the [Shape of Regular Sentential Forms](/theorems/1786) theorem applies: each $\tau_i \in \mathbb{W} \cup \mathbb{W}(V \cup V')$, with $\mathbb{W} = \Sigma^\star$. The [Structure of Terminal Derivations](/theorems/1787) theorem then says $N = |u|$ and the derivation consists of $|u| - 1$ nonterminal-rule steps followed by one terminal-rule step. [claim:Each $\tau_i$ for $0 \leq i \leq N - 1$ has the shape $w_i A_i$ with $w_i \in \Sigma^\star$ and $A_i \in V \cup V'$] By the [Shape of Regular Sentential Forms](/theorems/1786) theorem $\tau_i \in \mathbb{W} \cup \mathbb{W}(V \cup V')$. If $\tau_i \in \mathbb{W}$, then $\tau_i$ contains no variable, and no further $H$-step is possible (regular rules have single-variable left-hand sides). Since $i < N$, a subsequent step exists, so $\tau_i \notin \mathbb{W}$. Hence $\tau_i \in \mathbb{W}(V \cup V')$, and we may write $\tau_i = w_i A_i$ with $w_i \in \Sigma^\star$ and $A_i \in V \cup V'$. The final sentential form $\tau_N = u \in \Sigma^\star$ lies in $\mathbb{W}$. [/claim] [proof] The argument is in the claim: combining $\tau_i \in \mathbb{W} \cup \mathbb{W}(V \cup V')$ with the requirement that a further step exists. [/proof] Record further: because every rule of $H$ has a single-variable left-hand side and $\tau_i = w_i A_i$ contains only the one variable $A_i$ (at its last position), the derivation step $\tau_i \to_H \tau_{i+1}$ acts on $A_i$ and uses a rule of the form $A_i \to a$ (terminal, which by $P^\star$'s construction would have to lie in $P'$, since $P^\star$ has no pure terminal rules of this form from $P$) or $A_i \to a B_i$ (nonterminal, with $B_i \in V \cup V'$). In the former case $\tau_{i+1} = w_i a \in \mathbb{W}$; in the latter $\tau_{i+1} = w_i a B_i \in \mathbb{W}(V \cup V')$. [/step]

[step:Show each $A_i$ is either in $V$ or in $V'$, with a unique transition point] Classify each index $i \in \{0, 1, \dots, N - 1\}$ as: - a **$V$-index** if $A_i \in V$, equivalently if the rule applied at step $i$ has left-hand side in $V$; - a **$V'$-index** if $A_i \in V'$. Every index falls into exactly one class because $V$ and $V'$ are disjoint (first step, after the renaming reduction). [claim:The set of $V$-indices is a prefix $\{0, 1, \dots, k\}$ of $\{0, \dots, N - 1\}$ for some $k$] We prove that once an index is a $V'$-index, all subsequent indices are $V'$-indices. Equivalently: if $A_i \in V'$ then $A_{i+1} \in V'$ (for $i < N - 1$). Suppose $A_i \in V'$. Then the rule applied at step $i$ has $A_i \in V'$ as left-hand side; by inspection, this rule must lie in $P'$ (rules of $P^\star$ have left-hand side in $V$ — they were derived from $P$-rules, whose left-hand sides lie in $V$ by construction of $G$). Hence the rule is either $A_i \to a \in P'$ (terminal) or $A_i \to a B_i \in P'$ (nonterminal), with $B_i \in V'$ because $G'$ has variables $V'$. In the terminal case, $\tau_{i+1} = w_i a \in \mathbb{W}$ has no variable, so $i = N - 1$ (there is no $A_{i+1}$ to consider, and by the [Structure of Terminal Derivations](/theorems/1787) theorem the terminal step is the last). In the nonterminal case, $A_{i+1} = B_i \in V'$, so $i+1$ is a $V'$-index. Combining, if index $i$ is a $V'$-index, either $i = N - 1$ (no successor to worry about) or $A_{i+1} \in V'$. By induction, all indices $\geq i$ are $V'$-indices. [/claim] [proof] See the case analysis in the claim: a $V'$-index is followed either by termination or by another $V'$-index, by inspection of the two rule types of $P'$. [/proof] [claim:The set of $V$-indices is nonempty] The initial variable is $A_0 = S \in V$ (since the first sentential form is $\tau_0 = S = \varepsilon S$, with $w_0 = \varepsilon$ and $A_0 = S$). Hence $0$ is a $V$-index. [/claim] [proof] Direct from $S \in V$. [/proof] Combining the two claims: the $V$-indices form $\{0, 1, \dots, k\}$ for some $0 \leq k \leq N - 1$, and the $V'$-indices form $\{k+1, k+2, \dots, N - 1\}$ (possibly empty if $k = N - 1$). We show below that $k < N - 1$, i.e., the transition to $V'$ occurs strictly before the end. [/step]

[step:Identify the transition step as the use of a chaining rule $A \to aS'$] The step at index $k$ is a $V$-step: $A_k \in V$, so the rule used at step $k$ has left-hand side in $V$, hence belongs to $P^\star$. If $k = N - 1$, the rule used would be the final step's rule; by the [Structure of Terminal Derivations](/theorems/1787) theorem, the final step uses a terminal rule, i.e., a rule of shape $A \to a$. But $P^\star$ contains no rule of shape $A \to a$ (the original terminal rules of $P$ were replaced by chaining rules $A \to aS'$; and $P^\star$'s nonterminal rules all have the form $A \to aB$). Hence step $k$ is not a terminal step, so $k < N - 1$. Moreover, step $k$'s rule is a nonterminal rule of $P^\star$. The nonterminal rules of $P^\star$ come in two flavours: chaining rules $A \to aS'$ (new, introducing $S' \in V'$) and original nonterminal rules $A \to aB$ from $P$ (with $B \in V$). If step $k$ used an original $P$-nonterminal rule $A \to aB$ with $B \in V$, then $A_{k+1} = B \in V$, meaning index $k+1$ is also a $V$-index, contradicting the definition of $k$ as the largest $V$-index. Hence step $k$ uses a chaining rule \begin{align*} A_k &\to a S', \end{align*} for some $a \in \Sigma$, with $A_{k+1} = S' \in V'$. In particular, at step $k$ the sentential form transitions from $\tau_k = w_k A_k$ (with $A_k \in V$, $w_k \in \Sigma^\star$) to $\tau_{k+1} = w_k a S'$ (with $S' \in V'$). Set $v := w_k a \in \Sigma^\star$ and observe $\tau_{k+1} = v S'$ with $|v| = k + 1$. [/step]

[step:Extract the $G$- and $G'$-sub-derivations]Consider the prefix $\tau_0, \tau_1, \dots, \tau_{k+1}$ of the $H$-derivation. Each step from $\tau_i$ to $\tau_{i+1}$ for $i \in \{0, \dots, k\}$ uses a rule of $P^\star$ with $V$-left-hand side. We translate these steps back to $G$-steps as follows. Define the $G$-rule corresponding to a $P^\star$-rule: \begin{align*} (A \to aB) &\in P^\star \text{ (with } A, B \in V) &&\longleftrightarrow && (A \to aB) \in P, \\ (A \to aS') &\in P^\star \text{ (chaining rule)} &&\longleftrightarrow && (A \to a) \in P. \end{align*} The first correspondence is identity; the second strips the trailing $S'$. For the final step $k$ (which uses a chaining rule $A_k \to aS'$), this yields the $G$-rule $A_k \to a$. Define $\tilde\tau_i$ for $i = 0, 1, \dots, k, k+1$ by \begin{align*} \tilde\tau_i &:= \begin{cases} \tau_i & \text{if } i \leq k \text{ (note } \tau_i \in (\Sigma \cup V)^\star\text{)}, \\ w_k a = v & \text{if } i = k + 1. \end{cases} \end{align*} We verify $\tilde\tau_0, \dots, \tilde\tau_{k+1}$ is a valid $G$-derivation. For $i < k$, $\tilde\tau_i \to \tilde\tau_{i+1}$ uses the corresponding $G$-rule (which is either the identical $P$-nonterminal rule or — in the case step $i$ used a chaining rule — a $G$-terminal rule). By the analysis of step $k$, only step $k$ uses a chaining rule, so for $i < k$ the rule is a $G$-nonterminal rule and $\tilde\tau_i = \tau_i \to_G \tau_{i+1} = \tilde\tau_{i+1}$. For $i = k$, $\tilde\tau_k = \tau_k = w_k A_k$ and the $G$-step uses rule $A_k \to a$ giving $\tilde\tau_{k+1} = w_k a = v$. Hence \begin{align*} S = \tilde\tau_0 \xrightarrow{G} \tilde\tau_{k+1} = v, \end{align*} a $G$-derivation of $v$. Hence $v \in L$. Now consider the suffix $\tau_{k+1}, \tau_{k+2}, \dots, \tau_N$. We have $\tau_{k+1} = vS'$; every step from index $\geq k + 1$ uses a $P'$-rule (because indices $\geq k+1$ are $V'$-indices, and the rule used has left-hand side in $V'$, which by inspection means it belongs to $P'$ — the rules of $P^\star$ have left-hand side in $V$). The string $\tau_{k+1}$ has a leading terminal block $v$ and a trailing variable $S' \in V'$. A $P'$-rule acting on $\tau_{k+1}$ rewrites the $V'$-variable; $v$ is frozen terminal context. Hence we may strip the leading $v$ from every $\tau_j$ for $j \geq k + 1$ and obtain a sequence \begin{align*} \hat\tau_j &:= \tau_j \text{ with the leading } v \text{ removed}, \quad k + 1 \leq j \leq N. \end{align*} Explicitly $\hat\tau_{k+1} = S'$ and $\hat\tau_N = u / v$ (the unique string such that $u = v \hat\tau_N$); since the leading $v$ of $\tau_j$ is preserved through every step (no $P'$-rule affects the $V$-side since there is no $V$-variable in $\tau_j$), $\hat\tau_N$ is well-defined. Each step $\hat\tau_j \to \hat\tau_{j+1}$ uses the same $P'$-rule that was used in the corresponding $H$-step $\tau_j \to \tau_{j+1}$, applied at the position of the $V'$-variable — now at position $0$ in $\hat\tau_j$ (after stripping $v$), or more generally at the position where the variable lies. This is a valid $G'$-step. Hence $S' = \hat\tau_{k+1} \xrightarrow{G'} \hat\tau_N$, a $G'$-derivation of $\hat\tau_N$. Since the $H$-derivation ends with a terminal $\tau_N = u \in \Sigma^\star$, we have $\hat\tau_N \in \Sigma^\star$, so $\hat\tau_N \in \mathcal{L}(G') = L'$. Call $w := \hat\tau_N$. Then $u = \tau_N = v \hat\tau_N = vw$ with $v \in L$, $w \in L'$. Hence $u \in LL'$. This shows $\mathcal{L}(H) \subseteq LL'$.[/step]

[guided]The converse direction is the delicate half. The structural fact driving it is that a $H$-derivation of a terminal word $u$ is *rigid*: by the [Shape of Regular Sentential Forms](/theorems/1786) and [Structure of Terminal Derivations](/theorems/1787) theorems, the sentential forms are always $w_i A_i$ with $w_i$ an ever-growing terminal prefix and $A_i$ the single trailing variable that is the only site of rule application. This lets us follow a single "trail" through the derivation: at each step, the variable $A_i$ is either replaced by $aB$ (nonterminal rule, variable continues to exist at the end of a slightly longer string) or by $a$ (terminal rule, the derivation ends). Now the key observation about $H$'s rules: the left-hand sides of $P^\star$-rules are in $V$, and the left-hand sides of $P'$-rules are in $V'$. Since $V \cap V' = \varnothing$, the variable $A_i$ uniquely determines which rule set is used. Moreover, the right-hand side of a $P$-style nonterminal rule keeps the variable in $V$, and the right-hand side of a $P'$ nonterminal rule keeps it in $V'$. The *only* way to transition from a $V$-variable to a $V'$-variable is via a chaining rule $A \to aS' \in P^\star$, which was specifically engineered to introduce $S'$. Hence the derivation has the structure: a prefix of $P^\star$-steps with $A_i \in V$ at every stage, ending with a chaining step $A_k \to aS'$ at some index $k$, followed by a suffix of $P'$-steps with $A_j \in V'$ at every stage, ending with a terminal $P'$-step $B \to b$ at step $N - 1$. The prefix (including the chaining step) mirrors a $G$-derivation of some word $v$: replace the chaining rule $A_k \to aS'$ by $G$'s corresponding terminal rule $A_k \to a$ to get exactly the $G$-derivation guaranteed by the [Structure of Terminal Derivations](/theorems/1787) theorem for the word $v$ of length $k + 1$. The suffix (starting from $\tau_{k+1} = vS'$) mirrors a $G'$-derivation of some word $w$: strip the frozen leading $v$ and follow the derivation from $S'$. The derivation thus cleanly splits at a *unique* chaining step, yielding $u = vw$ with $v \in L$, $w \in L'$. The uniqueness of the chaining step is the mathematical content of "there is a unique $k$ such that index $k$ is the last $V$-index".[/guided]

[step:Combine the inclusions and conclude $LL'$ is regular] From the third step, $LL' \subseteq \mathcal{L}(H)$. From the previous step, $\mathcal{L}(H) \subseteq LL'$. Hence $\mathcal{L}(H) = LL'$. Since $H$ is a regular grammar (second step), $LL' = \mathcal{L}(H)$ is a regular language. This completes the proof that the class of regular languages is closed under concatenation. [/step]