Изменения

1) <tex>S</tex> отвечает за правильный старт, то есть символ <tex>q_{0,0}</tex> должен быть начальным состоянием <tex>q_0\,\!#_s</tex> машины <tex>m\,\!</tex>, символы с <tex>q_{0,1}\,\!</tex> по <tex>q_{0,|x|}\,\!</tex> &mdash; образовывать цепочку <tex>x\,\!</tex>, а оставшиеся <tex>q_{0,i}\,\!</tex> &mdash; быть пробелами <tex>B\,\!</tex>. Таким образом, <tex>S = Y_{0,0,\#_s} \land Y_{0,1,x_1} \land \ldots \land Y_{0,|x|+1,B} \land \ldots \land Y_{0,t,B}</tex>.

2) <tex>T</tex> отвечает за правильный финиш, то есть в МО <tex>q_t</tex> должно присутствовать допускающее состояние <tex>\#_y\,\!</tex>, следовательно <tex>T = Y_{t,0,\#_y} \lor Y_{t,1,\#_y} \lor \ldots \lor Y_{t,t,\#_y}</tex>.

3) <tex>N</tex> отвечает за то, что машина <tex>m\,\!</tex> делает правильные переходы. <tex>q_{i,j}</tex> зависит только от четырех символов над ним, то есть от <tex>q_{i-1,j-1}</tex>, <tex>q_{i-1,j}</tex>, <tex>q_{i-1,j+1}</tex> и <tex>q_{i-1,j+2}</tex>. Тогда для проверки корректности переходов требуется перебрать все четверки символов <tex>q_{i-1,j-1}</tex>, <tex>q_{i-1,j}</tex>, <tex>q_{i-1,j+1}</tex> и <tex>q_{i-1,j+2}</tex> из таблицы и проверить, что из них возможно получить символ <tex>q_{i,j}</tex>. Если четверка символов выходит за границу таблицы, то указывается меньшее количество позиций. <tex>N = \land_{i=0..t,j=0..t} \land_{c_1 \ldots c_4} (( Y_{i-1,j-1,c_1} \land Y_{i-1,j,c_2} \land Y_{i-1,j+1,c_3} \land Y_{i-1,j+2,c_4} ) \to (Y_{i,j,c_1^`} \lor Y_{i,j,c_2^`} \lor \ldots \lor Y_{i,j,c_{|\Sigma|-1}^`}))</tex>.

4) <tex>C</tex> отвечает за то, что в каждой ячейке находится ровно один символ. Для каждой ячейки <tex>q_{i,j}</tex> проверяется, что только одна переменная <tex>Y_{i,j,c}</tex> принимает значение ''истина''. <tex>C = \land_{i=0..t,j=0..t} ((Y_{i,j,c_1} \land \lnot Y_{i,j,c_2} \land \ldots \land \lnot Y_{i,j,c_{|\Sigma|-1}}) \lor \ldots \lor (Y_{i,j,c_{|\Sigma|-1}} \land \lnot Y_{i,j,c_1} \land \ldots \land \lnot Y_{i,j,c_{|\Sigma|-2}}))</tex>.

Мы построили функцию сведения <tex>f: <m, x, 1^t> \mapsto \phi = S \land T \land N \land C</tex>. Она является полиномиальной, так как длина формулы <tex>\phi</tex> полиномиально зависит от <tex>|1^t| = t</tex>, а именно: <tex>|\phi| = O(t^3)</tex>.

1) Пусть <tex><m, x, 1^t> \in BH_{1N}</tex>, тогда существует допускающая цепочка переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex>, где (в МО <tex>q_t</tex> присутствует допускающее состояние <tex>\#_y\,\!</tex>), следовательно можем построить таблицунайти такое присваивание 0 и 1 переменным <tex>Y_{i, аналогичную приведенной вышеj, а значит можем построить выполнимую формулу c}</tex>, что <tex>\phi</tex>примет значение ''истина''.

2) Пусть в результате работы функции <tex>f</tex> получили выполнимую формулу <tex>\phi</tex>, следовательно существует такой набор переменных <tex>Y_{i,j,c}</tex>, что <tex>\phi</tex> на нем принимает значение <tex>1</tex>''истина''. Тогда можем по данному набору построить непротиворечивую таблицу, аналогичную приведенной выше, по которой можно восстановить допускающую цепочку переходов <tex>q_0 \vdash q_1 \vdash ... \vdash q_t</tex>. Совершив эти переходы машина <tex>m</tex> перейдет в допускающее состояние за время <tex>t</tex>, следовательно <tex><m, x, 1^t> \in BH_{1N}</tex>.