68
правок
Изменения
Нет описания правки
<tex>\phi(A, B, t) = \exists R \,\forall U \,\forall V \, \{\phi(U, V, t-1) \lor \neg [(U = A \land V = R) \lor (U = R \land V = B)]\}</tex>.
Получившаяся в фигурых скобках формула верна только когда верно <tex>\phi(U, V, t-1)</tex> или <tex>\neg[(U = A \land V = R) \lor (U = R \land V = B)]</tex>. Это равносильно тому, что существует такое промежуточное состояние промежуточная конфигурация <tex>R</tex>, что для любых конфигураций <tex>RU</tex> достижима из и <tex>AV</tex> не более, чем за либо верна формула <tex>2^{\phi(U, V, t-1})</tex> шагов, и либо те конигурации для которых вызывается наша формула нас не интересуют. Если описания <tex>BU</tex> достижима из и <tex>RV</tex> за нам подходят, то чтобы вся формула была верна необходимо чтобы <tex>2^{\phi(U, V, t-1})</tex> шаговвыполялось. А если верно и тозначит, и другое, то конфигурация <tex>B</tex> достижима из конфигурации <tex>A</tex> не более, чем за <tex>2^t</tex> шагов.
За один шаг рекурсии длина максимального пути между конфигурациями уменьшается в два раза. Поэтому общую длину получившейся формулы можно представить как <tex>L(t) = L(t-1)+const</tex>, где <tex>const = \|\exists R \,\forall U \,\forall V \, \{\| + \|\land [(U = A \land V = R) \lor (U = R \land V = B)]\}\|</tex>.
