69
правок
Изменения
Нет описания правки
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>, <br/> тогда в силу <tex>a = w_{j-1}</tex> получаем <tex>\alpha = \alpha ' a \Rightarrow^* w_i...w_{j-2}w_{j-1} = w_i...w_{j-1}</tex>.<br/>
Таким образом условия: <tex>S \Rightarrow^* w_0...w_{i-1} A \delta</tex> и <tex>\alpha \Rightarrow^* w_i...w_{j-1}</tex> выполняются.
2. Включаем по правилу <tex> \mathtt{predict}</tex>.<br/>
По построению: <tex> \alpha = \varepsilon </tex> и <tex>i=j</tex>, что автоматически влечет второй пункт утверждения.<br/>
Кроме того <tex>\exists i' \le i</tex> и ситуация <tex>[A' \rightarrow \alpha ' \cdot A \delta ', i'] \in D_i</tex>, из чего по предположению индукции следует <tex>S \Rightarrow^* w_0...w_{i'-1} A' \delta ''</tex> и <tex> \alpha ' \Rightarrow^* w_{i'}...w_{i-1})</tex>.<br/>Получаем, что <tex>S \Rightarrow^* w_0...w_{i'-1} A' \delta '' \Longrightarrow </tex>, значит <tex>S \Rightarrow^* w_0...w_{i'-1} \alpha' A \delta' \delta '' \Longrightarrow </tex>, следовательно <tex> S \Rightarrow^* w_0...w_{i'-1} w_{i'}...w_{i-1} A \delta' \delta ''\Longrightarrow </tex>, в итоге <tex> S \Rightarrow^* w_0...w_{i-1} A \delta</tex>, что нам и требовалось.
=====В каждый список попадут все ситуации, которые ему принадлежат:=====
