Изменения

Пусть <tex>I</tex> — мгновенное описание <tex>M</tex>, тогда выражение <tex>\exists I</tex> обозначает <tex> ( \exists x_1 )\land( \exists x_2 )\land\dots\landcdots( \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) (\neg(\phi(U, V, t/2)) \rightarrow ([(U \neq S \lor V \neq R) \land (U \neq R \lor V \neq S)])</tex>  Заметим, что размер функции <tex>\phi(a, B, t)</tex> равен размеру <tex>\phi(A, B, t/2)</tex> с константной добавкой.Теперь мы можем записать функцию <tex>f(M, w)</tex> которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в <tex>TQBF</tex>. <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>, то если мы задодим корректное стартовое состояние, то пути до корректного финишного состояния существовать не может.