68
правок
Изменения
м
Нет описания правки
<tex>f(M, w) = (\exists I_s) (\exists I_f) (x_{I_s, 0} = start \land x_{I_s, 1} = w[1] \land \dots \land x_{I_s, |w|} = w[|w|]) \land ((\exists i) x_{I_f, i} = finish) \land \phi(Start, Finish, 2^{log_2(c^{1+p(n)}})</tex>
Докажем, что получившаяся булева формула с кванторами удовлетворима тогда и только тогда, когда <tex>w \in L</tex>.
Если <tex>w \in L</tex>, то стартовое и финишное состояние задано корректно. Также из стартового состояния можно попасть в финишное за полиномиальное время.
Если <tex>w \not\in L</tex>, то если мы задодим корректное стартовое состояние, то пути до корректного финишного состояния существовать не может.
}}
