[math]\Longrightarrow[/math]
Докажем индукцией по исполнению алгоритма.
База индукции:
[math][S' \rightarrow \cdot S, 0] \in D_0[/math].
Индукционный переход:
Пусть предположение верно для всех списков ситуаций с номерами меньше [math] j [/math]. Разберемся, в результате применения какого правила ситуация [math] [A \rightarrow \alpha \cdot \beta, i] [/math] попала в [math]D_{j}[/math]
1. Включаем по правилу [math] \mathtt{scan}[/math].
Это произошло, если [math] \alpha = \alpha ' a[/math], [math]a = w_{j-1}[/math] и [math] [A \rightarrow \alpha ' \cdot a \beta, i] \in D_{j-1}[/math].
По предположению индукции [math]S' \Rightarrow^* w_0...w_{i-1} A \delta[/math] и [math]\alpha' \Rightarrow^* w_i...w_{j-2}[/math],
тогда в силу [math]a = w_{j-1}[/math] получаем [math]\alpha = \alpha ' a \Rightarrow^* w_i...w_{j-2}w_{j-1} = w_i...w_{j-1}[/math].
Таким образом условия: [math]S' \Rightarrow^* w_0...w_{i-1} A \delta[/math] и [math]\alpha \Rightarrow^* w_i...w_{j-1}[/math] выполняются.
2. Включаем по правилу [math] \mathtt{predict}[/math].
По построению: [math] \alpha = \varepsilon [/math] и [math]i=j[/math], что автоматически влечет второй пункт утверждения.
Кроме того [math]\exists i' \le i[/math] и ситуация [math][A' \rightarrow \alpha ' \cdot A \delta ', i'] \in D_i[/math], из чего по предположению индукции следует [math]S' \Rightarrow^* w_0...w_{i'-1} A' \delta ''[/math]
и [math] \alpha ' \Rightarrow^* w_{i'}...w_{i-1}[/math].
Получаем, что [math]S' \Rightarrow^* w_0...w_{i'-1} A' \delta ''[/math], значит [math]S \Rightarrow^* w_0...w_{i'-1} \alpha' A \delta' \delta '' [/math], следовательно [math] S' \Rightarrow^* w_0...w_{i'-1} w_{i'}...w_{i-1} A \delta' \delta ''
[/math], в итоге [math] S' \Rightarrow^* w_0...w_{i-1} A \delta[/math], что нам и требовалось.
3. Включаем по правилу [math] \mathtt{complete}[/math].
По построению: [math] \alpha = \alpha ' A' [/math] и [math]\exists i', \delta : [A \rightarrow \alpha ' \cdot A' \beta, i] \in D_{i'} \wedge [A' \rightarrow \eta \cdot, i'] \in D_j[/math].
Cледовательно [math]\alpha = \alpha ' A' \Rightarrow^* w_i...w_{i'-1} w_{i'}...w_{j} = w_i...w_{j-1}[/math], что дает нам второй пункт утверждения, а так как первый пункт следует из индукционного предположения, все хорошо.
[math]\Longleftarrow[/math]
В обратную сторону будем доказывать индукцией по суммарной длине вывода [math]w_0...w_{i-1} A \delta[/math] из [math]S'[/math] и [math]w_i...w_{j-1}[/math] из [math]\alpha[/math]. После чего применим
индукцию по длине вывода [math]w_i...w_{j-1}[/math] из [math]\alpha[/math].
Рассмотрим три случая последнего символа [math]\alpha[/math]:
1. [math]\alpha = \alpha ' a[/math], тогда [math]a = w_{j-1}[/math] и [math]\alpha ' \Rightarrow^* w_i...w_{j-2}[/math].
По предположению индукции: [math][A \rightarrow \alpha ' \cdot a \beta, i] \in D_{j-1}[/math], а отсюда по правилу [math] \mathtt{scan}[/math] получаем [math][A \rightarrow \alpha ' a \cdot \beta, i] \in D_{j}[/math].
2. [math]\alpha = \alpha ' B[/math], тогда [math]\exists i' : \alpha ' \Rightarrow^* w_i...w_{i'-1} \wedge B ' \Rightarrow^* w_{i'}...w_{j-1}[/math].
Тогда имеем [math][A \rightarrow \alpha ' a \cdot \beta, i] \in D_{j}[/math]. Также можно записать [math]S' \Rightarrow^* w_0...w_{i-1} A \delta[/math], как [math]S' \Rightarrow^* w_0...w_{i-1} w_i...w_{i'-1}B \beta \delta[/math],
а также [math]B \rightarrow \eta \wedge \eta \rightarrow w_{i'}...w_{j-1}[/math].
Применяя индукцию по второму параметру получим [math][B \rightarrow \eta \cdot, i'] \in D_j[/math], откуда по правилу [math] \mathtt{complete}[/math] получаем [math][A \rightarrow \alpha ' B \cdot \beta, i] \in D_{j}[/math].
3. [math]\alpha = \varepsilon [/math], тогда [math]i=j[/math].
Тогда либо [math]i = 0 \wedge A = S \wedge \delta = \varepsilon[/math], что доказывает базу индукции,
либо вывод можно записать в виде [math]S' \Rightarrow^* w_0...w{i'-1}w_{i'}...w{i-1} A \delta ' \delta '' = w_0...w_{i-1} A \delta[/math] для некоторого правила [math](A' \rightarrow w_{i'}...w_{i-1} A \delta ') \in P[/math].
Отсюда по предположению индукции [math][A' \rightarrow \cdot w_{i'}...w_{i-1} A \delta ', i'] \in D_{i'}[/math],
что после нескольких применений правила [math] \mathtt{scan}[/math] приводит к [math][A' \rightarrow w_{i'}...w_{i-1} \cdot A \delta ', i'] \in D_{i}[/math],
после чего по правилу [math] \mathtt{predict}[/math] получим [math][A \rightarrow \cdot \beta, i] \in D_{j}[/math], что и требовалось. |