Изменения
→Лемма о разрастании для КС-грамматик
*Рассмотрим стартовый нетерминал <tex>S</tex>. Из <tex>S</tex> выведена строка <tex>\omega</tex>. При этом <tex>S \Rightarrow^{*} \alpha A \beta \Rightarrow^{*} \omega </tex>, где <tex>A</tex> {{---}} выбранный ранее нетерминал. Из <tex>A</tex> в данном дереве разбора выведена строка <tex>vxy</tex>. Пусть <tex>u</tex> и <tex>z</tex> {{---}} строки, состоящие из терминалов, которые выведены соответственно из <tex>\alpha</tex> и <tex>\beta</tex> в данном дереве разбора. Тогда <tex>S \Rightarrow^{*} uAz \Rightarrow^{*} uvAyz \Rightarrow^{*} \omega</tex>.
Покажем, что <tex>|vxy| \leqslant n</tex>. Допустим, что <tex>|vxy|>n</tex>. Тогда высота поддерева с корнем в вершине, соответствующей выбранному <tex>A</tex>, не меньше <tex>m+2</tex>. Рассмотрим поддерево вершины, в которой котором содержится нетерминал <tex>A</tex>. Тогда высота этого поддерева не меньше <tex>m+1</tex>. Рассмотрим путь максимальной длины от корня этого поддерева к листу. В нем содержится не менее <tex>m+1</tex> нетерминалов, причем не содержится стартовый нетерминал. Следовательно, на этом пути найдутся два одинаковых нетерминала, что противоречит условию наибольшей удаленности от корня выбранного ранее нетерминала <tex>A</tex>. Получили противоречие. Поэтому <tex>|vxy|\leqslant n</tex>.
Таким образом, в рамках нашей грамматики мы можем построить цепочку вывода: <tex>S \Rightarrow^{*} uAz \Rightarrow^{*} uvAyz \Rightarrow^{*} uvvAyyz \Rightarrow^{*} uv^{k}Ay^{k}z \Rightarrow^{*} uv^{k}xy^{k}z</tex>.
}}
