1632
правки
Изменения
м
rollbackEdits.php mass rollback
Пусть <tex>N' = N \cup \{a' \mid a \in \Sigma\}</tex>.
Пусть <tex>\alpha = x_1x_2...\ldots x_n</tex> {{---}} часть правила, тогда <tex>\alpha' = y_1y_2...\ldots y_n</tex>, где
<tex>
y_i = \left\{\begin{array}{llcl}
Покажем, что <tex>L(\Gamma') = L(\Gamma)</tex>.
Пусть <tex>w \in L(\Gamma)</tex>. Тогда в <tex>\Gamma</tex> существует вывод <tex>S = w_0 \Rightarrow w_1 \Rightarrow ... \ldots \Rightarrow w_n \Rightarrow w</tex>.
Согласно конструкции <tex>P'</tex>, в <tex>\Gamma'</tex> существует вывод <tex>S = w_0' \Rightarrow w_1' \Rightarrow w_2' \Rightarrow ... \ldots \Rightarrow w_n' = v_0 \Rightarrow v_1 \Rightarrow v_2 \Rightarrow ... \ldots \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>a' \rightarrow a</tex> полученное <tex>a</tex> не может быть использовано при применении правил из <tex>P'</tex>.
Изменение порядка вывода не меняет язык, то есть в <tex>\Gamma'</tex> существует вывод: <tex>S = x_0' \Rightarrow x_1' \Rightarrow ... \ldots \Rightarrow x_r' \Rightarrow x' \Rightarrow y_1 \Rightarrow y_2 \Rightarrow ... \ldots \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>\Gamma</tex>: <tex>S = x_0 \Rightarrow x_1 \Rightarrow ... \ldots \Rightarrow x_n = x</tex>.
Тогда <tex>L(\Gamma') \subseteq L(\Gamma)</tex>.
