Изменения

*Рассмотрим нетерминал <tex>A</tex>, содержащийся в поддереве выбранного нетерминала. Тогда <tex>x</tex> - строка терминалов которая выводится выведена из рассмотренного нетерминала в данном дереве разбора. <tex>A \Rightarrow^{*} x</tex>. *Рассмотрим выбранный нетерминал <tex>A</tex>. Пусть <tex>t</tex> - строка терминальных символов, которая выводится выведена из рассмотренного нетерминала в данном дереве разбора. Тогда <tex>A \Rightarrow^{*}\alpha A \beta \Rightarrow^{*} t</tex>, где <tex>\alpha,\beta</tex> - строки, состоящие из терминалов, которые могут содержать как терминалы, так и нетерминалы. При этом, как минимум одна из строк <tex>\alpha,\beta</tex> не пуста, так как грамматика языка записана в НФХ. Пусть <tex>v,y</tex> - строки, состоящие из терминалов, которые выводятся выведены из <tex>\alpha,\beta</tex> соответственно, в данном дереве разбора. Тогда <tex>t = vxy</tex>. Так как хотя бы одна из строк <tex>\alpha,\beta</tex> не пуста, то <tex>vy\neq \varepsilon</tex>. Тогда Получаем <tex>t = A \Rightarrow^{*} vAy \Rightarrow^{*} vxy</tex>. Получаем *Рассмотрим стартовый нетерминал <tex>S</tex>. Из <tex>S</tex> выведена строка <tex>\omega</tex>. При этом <tex>A S \Rightarrow^{*} vAy \alpha A \beta \Rightarrow^{*} \omega </tex>, где <tex>A</tex> - выбранный ранее нетерминал. Из <tex>A</tex> в данном дереве разбора выведена строка <tex>vxy</tex>.Пусть <tex>u,z</tex> - строки, состоящие из терминалов, которые выведены из <tex>\alpha,\beta</tex> соответственно, в данном дереве разбора. Тогда <tex>S \Rightarrow^{*} uAz \Rightarrow^{*} uvAyz \Rightarrow^{*} \omega</tex>.

рассмотрим путь от предпоследнего повторения нетерминала <tex> A</tex> до последнего его вхождения в дерево. Если из вершины был сделан переход в левое поддерево, то строка, выведенная из правого поддерева, будет частью <tex>y</tex>. Аналогично из левых поддеревьев получаем <tex>v</tex>. Так как грамматика записана в НФХ, то либо <tex>v</tex>, либо <tex>y</tex> не будет пустой строкой, то есть условие <tex>|vy|>0</tex> выполнено.Таким образом, в рамках нашей грамматики мы можем построить цепочку вывода: <tex>S \Rightarrow^{*} uAz \Rightarrow^{*} uvAyz \Rightarrow^{*} uvvAyyz \Rightarrow^{*} uv^{k}Ay^{k}z \Rightarrow^{*} uv^{k}xy^{k}z</tex>.