69
правок
Изменения
Нет описания правки
{{Теорема
|statement = Приведенный алгоритм правильно строит все списки ситуаций.
То есть алгоритм поддерживает инвариант <tex> [A \rightarrow \alpha \cdot \beta, i] \in D_{j} \Longleftrightarrow \exists \delta \in \Sigma \cup N : ((S \Rightarrow^* w_0...w_i w_{i-1} A \delta) \wedge A \Rightarrow^* w_i...w_jw_{j-1})</tex>
|proof =
=====<tex>\Longrightarrow</tex>=====
Докажем индукцией по исполнению алгоритма.<br/>
База {{---}}} <tex>[S' \rightarrow \cdot S, 0] \in D_0</tex>. Осталось разобраться, в результате применения какого правила ситуация <tex> [A \rightarrow \alpha \cdot \beta, i] </tex> попала в <tex>D_{j}</tex><br/>
1. Включаем по правилу <tex> \mathtt{scan}</tex>.<br/>
Это произошло, если <tex> \alpha = \alpha ' a</tex>, <tex>a = w_{j-1}</tex> и <tex> [A \rightarrow \alpha ' \cdot a \beta, i] \in D_{j-1}</tex>.<br/>
По предположению индукции <tex>S \Rightarrow^* w_0...w_{i-1} A \delta</tex> и <tex>\alpha' \Rightarrow^* w_i...w_{j-2}</tex>, тогда в силу a = w_{j-1} получаем <tex>\alpha = \alpha ' a \Rightarrow^* w_i...w_{j-2}w{j-1} = w_i...w{j-1}</tex>, что нам и требовалось.
1. Включаем по правилу <tex>(1)</tex>.<br/>
