Изменения

|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> , то и семейство требуемых схем.