68
правок
Изменения
Нет описания правки
Под выражением <tex>\exists I</tex> будем понимать <tex> \exists x_{I,1,c_1} \, \exists x_{I,1,c_2} \ldots \exists x_{I,1,c_\Omega} \, \exists x_{I,2,c_1} \ldots</tex> Аналогично выражение <tex> \forall I</tex> обозначает <tex> \forall x_{I,1,c_1} \, \forall x_{I,1,c_2} \ldots \forall x_{I,1,c_\Omega} \, \forall x_{I,2,c_1} \ldots</tex>
Рассмотрим функцию <tex>\phi(A, B, t)</tex>, проверяющую следующее условие: конфигурация <tex>B</tex> достижима из конфигурации <tex>A</tex> не более, чем за <tex>2^t</tex> шагов.
<tex>\phi(A, B, 0) = (A = B) \lor (A \vdash B)</tex>.
<tex>\phi(A, B, t) = \exists R \,\forall U \,\forall V \, \{\phi(U, V, \lceil t/2\rceil) \nrightarrow \neg[(U = A \land V = R) \lor (U = R \land V = B)]\}</tex>.
Получившаяся формула верна только когда верно <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>\phi(A, B, t)</tex> полиномиален относительно <tex>n</tex>.
