Изменения

|statement= Пусть <tex>SAT \in P /poly </tex>, тогда существует семейство схем полиномиального размера <tex>D_n</tex>, таких, что для любой формулы <tex>\phi \in SAT</tex> можно за полиномиальное время вывести , <tex>D_{|\phi|}(\phi)</tex> выводит набор значений, удовлетворяющий удовлетворяющих формуле.

Иначе, выберем любую переменную <tex>x</tex> из формулы <tex>\phi</tex>, и выполним подстановку <tex>x = 0</tex>. Получим формулу <tex>\phi_0</tex>. Если <tex>\phi_0 \in SAT</tex> (так как по условию теоремы<tex>SAT \in P/poly</tex>, такую проверку можно выполнить сделать за полиномиальное время, вычислив соответствующую схему), то мы свели задачу к аналогичной с меньшим числом переменных. В противном случае, сведение выполняется подстановкой <tex>x = 1</tex>. Мы получили программу, работающую за полиномиальное время, а так как <tex>P \in P/poly</tex> то и семейство требуемых схем.