68
правок
Изменения
Нет описания правки
<tex>\phi(A, B, t) = \\ (\exists R) (\forall U) (\forall V) \ \{\phi(U, V, t/2) \lor [\neg(A = U \land R = V) \land \neg(R = U \land B = V)]\}</tex>
:Переменые <tex> U </tex> и <tex>V</tex> важны важно рассмотреть только как пары <tex> (Aв двух случаях: когда первое из них стартовое, R)</tex> и <tex>(Rвторое — промежуточное, B)</tex>или первое — промежуточное, поэтому а второе — финишное. Поэтому для всех остальных вариантов выражение <tex>[\neg(A = U \land R = V) \land \neg(R = U \land B = V)]</tex> будет истинно. Если <tex>A = U \land R = V</tex> то , чтобы <tex>\phi(A, B, t)</tex> было истино истинно, необходимо наличие такого мгновенного описания <tex>R</tex> , чтобы были выполнены два утверждениябыло выполненно утверждение: <tex>A\vdash^{t/2}R</tex> и . Если <tex>R = U \land B = V</tex> то, нас интересует мгновенное описание <tex>R</tex> такое, что <tex>R\vdash^{t/2}B</tex>.
Заметим, что размер функции <tex>\phi(a, B, t)</tex> равен размеру <tex>\phi(A, B, t/2)</tex> с константной добавкой <tex>(\exists R) (\forall U) (\forall V) \ \{\ * \lor [\neg(A = U \land B = R) \land \neg(A = R \land B = V)]\}</tex> .
Теперь мы можем записать функцию <tex>f(M, w)</tex>, которая будет переводить ДМТ <tex>M</tex> и слово на ленте <tex>w</tex> в <tex>TQBF</tex>.
