11
правок
Изменения
→Доказательство: часть 2
Каждый элемент таблицы <tex>q_{i, j}\in \Sigma \cup Q</tex>. И для каждого такого элемента заведём <tex>|\Sigma| + |Q|\,\!</tex> переменных <tex>Y_{i, j, c} = [q_{i, j} = c]\ \forall c \in \Sigma \cup Q\,\!</tex>
Общий вид формулы : <tex>\phi = S \land T \land N \land C</tex>. <tex>S</tex> отвечает за правильный старт, то есть символ <tex>q_{0,0}</tex> должен быть начальным состоянием <tex>q_0\,\!</tex> машины <tex>m\,\!</tex>, символы с <tex>q_{0,1}\,\!</tex> по <tex>q_{0,|x|}\,\!</tex> — образовывать цепочку <tex>x\,\!</tex>, а оставшиеся <tex>q_{0,i}\,\!</tex> — быть пробелами <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>. <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>. <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>. <tex>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>.
