Изменения

Так как <tex>L \in PSPACE</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> в TQBFза полиномиальное относительно длины входа время.

<tex>\phi(A, B, t) = \\ (\exists R) (\forall U) (\forall V) \\ \qquad (\neg{\phi(U, V, t/2) \rightarrow lor [\neg(A = U \neq S \lor V \neq land B = R) \land \neg(U \neq A = R \lor land B = V \neq S)])\}</tex>

Заметим, что размер функции <tex>\phi(a, B, t)</tex> равен размеру <tex>\phi(A, B, t/2)</tex> с константной добавкой из-за <tex>(\exists R) (\forall U) (\forall V) \ \{\ * \rightarrow lor [\neg(A = U \neq S \lor V \neq land B = R) \land \neg(U \neq A = R \lor land B = V \neq S)])\}</tex> .