211
правок
Изменения
м
Нет описания правки
{{Лемма
|about=1
|statement=<tex>\sum\limits_{x_1 = 0}^1 \ldots \sum\limits_{x_m = 0}^1 A_\phi(x_1, \ldots, x_m)=k \iff Leftrightarrow \langle\phi,k\rangle \in \#SAT</tex>.
|proof=Следует из [[Арифметизация булевых формул с кванторами | леммы (1)]].
}}
Сведём язык <tex>TAUT</tex> к языку <tex>\#SAT</tex> следующим образом: <tex>\phi \mapsto \langle \phi, 2^k \rangle </tex>, где <tex>k</tex> — количество различных переменных в формуле <tex>\phi</tex>.
Очевидно, что <tex>\phi \in TAUT \iff Leftrightarrow \langle \phi, 2^k \rangle \in \#SAT</tex>.
По лемме (2) <tex>\#SAT \in \mathrm{IP}</tex>. Тогда <tex>TAUT \in \mathrm{IP}</tex>. Так как <tex>TAUT \in \mathrm{coNPC}</tex>, то <tex>\mathrm{coNP} \subset \mathrm{IP}</tex>.
