Изменения

<tex>f(M, w) = (\exists I_{st}) (\exists I_{fin}) (x_0^{I_{st}} = start \land x_1^{I_{st}} = w[1] \land \dots \land x_{|w|}^{I_{st}} = w[|w|]) \land (\exists i \, x_i^{I_{fin}} = finish) \land \phi(I_{st}, I_{fin}, log_2(2^{O(p(n))})))</tex>.

Если <tex>w \in L</tex>, то существует путь из стартовой конфигурации в финишную, причём длины не более, чем <tex>2^{O(p(n))}</tex>, а значит формула <tex>\phi</tex> верна.