211
правок
Изменения
м
Нет описания правки
Построим функцию <tex>f \colon \forall x \in L \Leftrightarrow f(x) \in TQBF</tex>.
Так как <tex>L \in \mathrm{PS}</tex>, то существует какая-то детерминированная машина Тьюринга <tex>M</tex>, которая его распознаёт за полиномиальное от размера входа время.
Пусть <tex>I</tex> — мгновенное описание <tex>M</tex>, тогда выражение <tex>\exists I</tex> обозначает <tex> (\exists x_1) (\exists x_2)\cdots(\exists x_n)</tex>, где <tex>\{x_i\}</tex> — все переменные мгновенного описания <tex>M</tex>. Аналогично выражение <tex> \forall I</tex> обозначает <tex> (\forall x_1) (\forall x_2)\dots(\forall x_n)</tex>. Теперь рассмотрим два мгновенных описание описания <tex>M: A</tex> и <tex>B</tex>. Напишем рекурсивную функцию <tex>\phi(A, B, t)</tex>, которая будет переводить утверждение <tex>A\vdash^tB</tex> в <tex>TQBF </tex> за полиномиальное относительно длины входа время.
<tex>\phi(A, B, t) = \\ (\exists R) (\forall U) (\forall V) \ \{\phi(U, V, t/2) \lor [\neg(A = U \land R = V) \land \neg(R = U \land B = V)]\}</tex>
