Изменения

Получившаяся формула верна только когда верно <tex>\phi(U, V, \lceil t/2\rceil)</tex> и ложно <tex>\neg[(U = A \land V = R) \lor (U = R \land V = B)]</tex>. Это равносильно тому, что <tex>V</tex> достижима из <tex>U</tex> не более, чем за <tex>\lceil t/2\rceil</tex> шагов, и либо <tex>U = A \land V = R</tex>, либо <tex>U = R \land V = B</tex>. А если верно и то, и другое, то конфигурация <tex>B</tex> достижима из конфигурации <tex>A</tex> не более, чем за <tex>t</tex> шагов.

Теперь мы можем записать функцию <tex>f(M, w)</tex>, которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в формулу из <tex>\mathrm{TQBF}</tex>.