[proofplan] We construct a grammar $G' = (\Sigma, V', P', S')$ on the new variable set together with a bijection $f: \Omega \to \Omega'$ which satisfies all four clauses of the definition of a grammar isomorphism. The bijection is defined by fixing any bijection $V \to V'$ on the variables and extending by the identity on terminals. We then choose $S'$ and $P'$ to be the images of $S$ and $P$ under the induced map on strings, so that clauses (ii) and (iv) of the isomorphism definition are forced to hold. Once $G'$ is shown to be a grammar isomorphic to $G$, the Isomorphic Grammars are Equivalent theorem yields $\mathcal{L}(G) = \mathcal{L}(G')$. [/proofplan] [step:Fix a bijection on variables and extend by the identity on terminals] By hypothesis $|V| = |V'|$, so there exists a bijection \begin{align*} f_0: V &\to V'. \end{align*} Write $\Omega := \Sigma \cup V$ and $\Omega' := \Sigma \cup V'$ for the full symbol alphabets of $G$ and of the prospective $G'$. We extend $f_0$ to a map on $\Omega$ by the identity on $\Sigma$: \begin{align*} f: \Omega &\to \Omega' \\ x &\mapsto \begin{cases} f_0(x) & \text{if } x \in V, \\ x & \text{if } x \in \Sigma. \end{cases} \end{align*} The definition is unambiguous provided $\Sigma \cap V = \varnothing$, which holds by the grammar definition. The map $f$ is a bijection: its restriction $f|_\Sigma = \operatorname{id}_\Sigma$ is a bijection $\Sigma \to \Sigma$, its restriction $f|_V = f_0$ is a bijection $V \to V'$, and the codomain decomposes disjointly as $\Omega' = \Sigma \sqcup V'$, so $f$ pairs the two halves of $\Omega$ with the two halves of $\Omega'$ bijectively. [/step] [step:Extend $f$ to a monoid homomorphism on strings] We promote $f: \Omega \to \Omega'$ to a map on finite strings by applying it letterwise: \begin{align*} \hat{f}: \Omega^\star &\to \Omega'^\star \\ a_1 a_2 \cdots a_k &\mapsto f(a_1) f(a_2) \cdots f(a_k), \end{align*} with $\hat{f}(\varepsilon) = \varepsilon$ on the empty string. For any $u, v \in \Omega^\star$ we have $\hat{f}(uv) = \hat{f}(u) \hat{f}(v)$, so $\hat{f}$ is a monoid homomorphism with respect to concatenation. [/step] [step:Define $S'$ and $P'$ as the images of $S$ and $P$ under $\hat{f}$] Set \begin{align*} S' &:= f(S) \in V', \\ P' &:= \{\, \hat{f}(\alpha) \to \hat{f}(\beta) \;\big|\; (\alpha \to \beta) \in P \,\}. \end{align*} Then $S' \in V'$ because $S \in V$ and $f(V) = V'$, so $S'$ is a valid choice of start symbol. Each element of $P'$ is a pair of strings in $\Omega'^\star$ because $\hat{f}(\Omega^\star) \subseteq \Omega'^\star$. Hence \begin{align*} G' &:= (\Sigma, V', P', S') \end{align*} is a grammar on the alphabet $\Sigma$ with variable set $V'$. [/step] [step:Verify the four isomorphism conditions] We check that $f: \Omega \to \Omega'$ is a grammar isomorphism from $G$ to $G'$ by verifying each of the four defining conditions. (i) **Identity on terminals.** By construction, $f(a) = a$ for all $a \in \Sigma$, so $f|_\Sigma = \operatorname{id}_\Sigma$. (ii) **Start symbols correspond.** By the definition of $S'$ in the previous step, $f(S) = S'$. (iii) **Bijection on variables.** By construction $f|_V = f_0$, which is a bijection $V \to V'$. (iv) **Rules correspond.** We must show \begin{align*} (\alpha \to \beta) \in P &\iff (\hat{f}(\alpha) \to \hat{f}(\beta)) \in P'. \end{align*} The forward implication holds immediately from the definition of $P'$. For the reverse, suppose $(\hat{f}(\alpha) \to \hat{f}(\beta)) \in P'$. By definition of $P'$ there exists a rule $(\alpha_0 \to \beta_0) \in P$ with $\hat{f}(\alpha_0) = \hat{f}(\alpha)$ and $\hat{f}(\beta_0) = \hat{f}(\beta)$. Since $\hat{f}$ is injective (being the letterwise extension of the bijection $f$, so a string is recoverable letter-by-letter by applying $f^{-1}$), $\alpha_0 = \alpha$ and $\beta_0 = \beta$, so $(\alpha \to \beta) \in P$. [guided] The four clauses partition into two groups: conditions (i) and (iii), which concern the bijection on symbols, and conditions (ii) and (iv), which concern the preservation of the grammar's data (start symbol and rules). We set up the bijection in the first two steps so that (i) and (iii) held automatically; we then defined $S'$ and $P'$ in the third step to *force* (ii) and (iv) to hold. All that remains is to verify this works. Clauses (i), (ii), (iii) are immediate from the way we defined $f$, $S'$, and $P'$. Clause (iv), the rule-preservation clause, needs slightly more care because it is a biconditional. The forward direction $\Rightarrow$ is the definition of $P'$: every rule of $G$ is turned into a rule of $G'$ by applying $\hat{f}$. The reverse direction $\Leftarrow$ needs an injectivity argument: if $\hat{f}(\alpha) \to \hat{f}(\beta)$ lies in $P'$, the *a priori* concern is that it might come from a different rule of $G$ whose image happens to coincide. But the letterwise map $\hat{f}$ is injective because $f$ is: if $\hat{f}(u) = \hat{f}(v)$ then $u$ and $v$ have the same length (read off from the length of the image), and letter-by-letter we recover $u_i = f^{-1}(\hat{f}(u)_i) = f^{-1}(\hat{f}(v)_i) = v_i$. So no two distinct rules of $G$ can produce the same image rule, and the pre-image rule is uniquely $(\alpha \to \beta)$. [/guided] [/step] [step:Invoke the isomorphism-to-equivalence theorem and conclude] The previous step shows that $f$ is a grammar isomorphism from $G$ to $G'$. Both $G$ and $G'$ are grammars on the same terminal alphabet $\Sigma$. By the [Isomorphic Grammars are Equivalent](/theorems/1777) theorem, \begin{align*} \mathcal{L}(G) &= \mathcal{L}(G'). \end{align*} Thus the grammar $G' = (\Sigma, V', P', S')$ constructed in the first three steps satisfies the conclusion of the theorem, completing the proof. [/step]