211
правок
Изменения
м
Нет описания правки
Теперь мы можем записать функцию <tex>f(M, w)</tex>, которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в формулу из <tex>TQBF</tex>.
<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>f</tex> верное.
