Изменения

Пусть <tex>N' = N \cup \{a' | : a \in T\}</tex>.

Пусть <tex>w \in L(G)</tex>. Тогда в G существует вывод <tex>S = w_0 => \Rightarrow w_1 => \Rightarrow ... => \Rightarrow w_n => \Rightarrow w</tex>.

Согласно конструкции <tex>P'</tex>, в <tex>G'</tex> существует вывод <tex>S = w_0' => \Rightarrow w_1' => \Rightarrow w_2' => \Rightarrow ... => \Rightarrow w_n' = v_0 => \Rightarrow v_1 => \Rightarrow v_2 => \Rightarrow ... => \Rightarrow v_m = w</tex>.

Для <tex>0 \leqslant i \leqslant n - 1</tex> в переходах <tex>w_i' => \Rightarrow w_{i + 1}'</tex> используем правило <tex>\alpha' \rightarrow \beta'</tex>, так как правило <tex>\alpha \rightarrow \beta</tex> было использовано при выводе <tex>w_i => \Rightarrow w_{i + 1}</tex>.

Для <tex>0 \leqslant j \leqslant m - 1</tex> в переходах <tex>v_j => \Rightarrow v_{j + 1}</tex> используем правила вида <tex>a' \rightarrow a</tex>.

Пусть <tex>x \in L(G')</tex>. Тогда в <tex>G'</tex> существует вывод <tex>S =>\Rightarrow^* x</tex>. Мы можем поменять порядок применения правил в этом выводе: сначала применяем только правила вида <tex>\alpha' \rightarrow \beta'</tex>, а потом только правила вида <tex>a' \rightarrow a</tex>.

Изменение порядка вывода не меняет язык, то есть в <tex>G'</tex> существует вывод: <tex>S = x_0' => \Rightarrow x_1' => \Rightarrow ... => \Rightarrow x_r' => \Rightarrow x' => \Rightarrow y_1 => \Rightarrow y_2 => \Rightarrow ... => \Rightarrow y_s = x</tex>, где для <tex>0 \leqslant i \leqslant r - 1 x_{i + 1}' \in (N')^*</tex> и в переходе <tex>x_i' \rightarrow x_{i + 1}'</tex> было использовано правило вывода <tex>\alpha' \rightarrow \beta'</tex> и для <tex>1 \leqslant j \leqslant s</tex> было использовано правило <tex>a' \rightarrow a</tex>, чтобы получить <tex>y_j \rightarrow y_{j + 1}</tex>.

Получаем вывод в <tex>G</tex>: <tex>S = x_0 => \Rightarrow x_1 => \Rightarrow ... => \Rightarrow x_n = x</tex>.

* шаг вывода <tex>\gamma_1AB\alpha'\gamma_2 => \Rightarrow \gamma_1CDE\beta'\gamma_2</tex>, благодаря правилу <tex>p = AB\alpha \rightarrow CDE\beta' \in P_2</tex> в <tex>G</tex>может быть использавано в <tex>G'</tex> с помощью трех шагов:<tex>\gamma_1AB\alpha'\gamma_2 => \Rightarrow \gamma_1A_pB_p\alpha'\gamma_2 => \Rightarrow \gamma_1CB_p\alpha'\gamma_2 => \Rightarrow \gamma_1CDE\beta\gamma_2</tex>, с использованием правил из <tex>P_p</tex> и вывода <tex>\gamma_1A\gamma_2 => \Rightarrow \gamma_1CDE\beta'\gamma_2</tex> на основе правила <tex>p = A\alpha \rightarrow CDE\beta' \in P_3</tex> в <tex>G</tex>, которое может быть применено в <tex>G'</tex> с помощью трех шагов вывода:<tex>\gamma_1A\alpha1'\gamma_2 => \Rightarrow \gamma_1A_pB_p\alpha'\gamma_2 => \Rightarrow \gamma_1CB_p\alpha'\gamma_2 => \Rightarrow \gamma_1CDE\beta\gamma_2</tex>.

Данный вывод имеет вид (1) : <tex>S =>\Rightarrow^* \gamma_1AB\alpha'\gamma_2 => \Rightarrow \gamma_1A_pB_p\alpha'\gamma_2 =>(\Rightarrow^q_1) \gamma_1'A_pB_p\alpha'\gamma_2' => \Rightarrow \gamma_1'CB_p\alpha'\gamma_2' =>(\Rightarrow^q_2) \gamma_1''B_p\alpha'\gamma_2'' => \Rightarrow \gamma_1''DE\beta'\gamma_2'' =>\Rightarrow^* w \in T^*</tex>,

где <tex>q_1</tex> {{---}} последовательность правил, примененых после <tex>AB \rightarrow A_pB_p</tex> и до <tex>A_p \rightarrow C</tex>, которая осуществляет <tex>\gamma_1 =>\Rightarrow^* \gamma_1'</tex> и <tex>\gamma_2 =>\Rightarrow^* \gamma_2'</tex>,

где <tex>q_2</tex> {{---}} последовательность правил, осуществляющих <tex>\gamma_1'C =>\Rightarrow^* \gamma_1''</tex> и <tex>\gamma_2' =>\Rightarrow^* \gamma_2''</tex>.

Или вид (2) : <tex>S =>\Rightarrow^* \gamma_1AB\alpha'\gamma_2 => \Rightarrow \gamma_1A_pB_p\alpha'\gamma_2 =>(\Rightarrow^{q_1}') \gamma_1'A_pB_p\alpha'\gamma_2' => \Rightarrow \gamma_1'A_pDE\beta'\alpha'\gamma_2' =>(\Rightarrow^{q_2') } \gamma_1''A_p\gamma_2'' => \Rightarrow \gamma_1''C\gamma_2'' =>\Rightarrow^* w \in T^*</tex>,

где <tex>q_1'</tex> {{---}} последовательность правил, которая осуществляет <tex>\gamma_1 =>\Rightarrow^* \gamma_1'</tex> и <tex>\gamma_2 =>\Rightarrow^* \gamma_2'</tex>,

где <tex>q_2'</tex> {{---}} последовательность правил, осуществляющих <tex>\gamma_1' =>\Rightarrow^* \gamma_1''</tex> и <tex>DE\beta'\gamma_2' =>\Rightarrow^* \gamma_2''</tex>.

Таким образом, существует вывод:<tex>S =>\Rightarrow^* \gamma_1AB\alpha'\gamma_2 => \Rightarrow \gamma_1CDE\beta'\gamma_2 => (\Rightarrow^{q_1) } \gamma_1'CDE\beta'\gamma_2' => (\Rightarrow^{q_2) } \gamma_1''DE\beta'\gamma_2'' =>\Rightarrow^* w \in T^*</tex>, который получается из (1) заменой правил <tex>P_p</tex> на применение <tex>p = AB\alpha' \rightarrow CDE\beta \in P</tex>. Аналогично, в случае (2) мы можем заменить применение <tex>P_p</tex> на <tex>p</tex>. Кроме того, это верно и для применения <tex>P_q,</tex> где <tex>q \in P_3</tex>.