Изменения

<tex>\mathrm{TAUT} = \{\phi</tex> {{---}} булева формула <tex>\bigm{| } \forall x = (x_1, x_2, \ldots , x_m) \, \phi(x)=1\}</tex>.

|proof=<tex>\overline {\mathrm{TAUT}} = \{\phi \bigm{| } \exists x : \phi(x) \ne 1\} = \{\phi \bigm{| } \overline {\phi} \in \mathrm{SAT}\}</tex>, то есть <tex>\mathrm{SAT} \le \overline {\mathrm{TAUT}} \, (f(\phi) = \overline {\phi})</tex>. Кроме того, <tex>\overline {\mathrm{TAUT}} \in \mathrm{NP}</tex> <tex>(</tex>в качестве сертификата используется <tex>x</tex>, на котором <tex>\phi(x) \ne 1)</tex>. Значит <tex>\overline{\mathrm{TAUT}} \in \mathrm{NPC}</tex>. Тогда по лемме (1) <tex>\mathrm{TAUT} \in \mathrm{coNPC}</tex>.

<tex>\mathrm{SPARSE} = \{L \bigm{| } \exists</tex> полином <tex>p: \forall n \, |L \cap \Sigma^n| \le p(n)\}</tex>.

'''if''' <tex>\phi=0</tex>

'''if''' <tex>\phi=1</tex>

'''if''' <tex>memo[\phi] \ne -1</tex>

<tex>memo[\phi] \leftarrow check(\phi|_{x_i=0}, i+1) \wedge check(\phi|_{x_i=1}, i+1)</tex>

'''returnexit''' 0

<tex>memo[f(\phi)] \leftarrow check(\phi|_{x_i=0}, i+1) \wedge check(\phi|_{x_i=1}, i+1)</tex> //(2)

Рассмотрим произвольный элемент <tex>memo[ij]</tex>. ЗаметимНайдем, сколько раз условие <tex>(1)</tex> в ходе выполнения программы является ложным при обращении к элементу <tex>memo[j]</tex>. Найдем в дереве такой узел, в котором есть обращение к <tex>memo[j]</tex>, а в его поддереве обращений к этому элементу нет, причем <tex>memo[j] = -1</tex>. До этого момента количество обращений к <tex>memo[j]</tex> не превышает глубины найденного узла, что не превосходит высоты дерева, что не превосходит некоторого полинома <tex>p'(n)</tex>. После этого момента условие <tex>(1)</tex> будет принимать истинное значение при обращении к <tex>memo[j]</tex>. Значит, в ходе выполнения программы условие <tex>(1)</tex> является ложным при обращении к элементу <tex>memo[ij]</tex> не более одного раза<tex>p'(n)</tex> раз.  Так как всего в <tex>memo</tex> не более <tex>r(n)</tex> элементов, то суммарно за все время выполнения программы условие <tex>(1)</tex> принимает ложное значение не более <tex>p''(n) = r(n) \cdot p'(n)</tex> раз, то есть <tex>p''</tex> {{---}} полином. Отсюда следует, что присваивание <tex>(2)</tex> выполняется не более <tex>rp''(n)</tex> раз, а значит в дереве не более <tex>rp''(n)</tex> внутренних вершин. Значит всего в дереве не более <tex>2 \cdot rp''(n) + 1</tex> вершин, то есть данная программа работает за полиномиальное время.

*[[Недетерминированные вычисления. Классы NP и Σ₁]]