Изменения

Хотелось бы воспользоваться протоколом из [[#SAT|доказательства принадлежности #SAT к классу IP]], лишь проверяя <tex>A_i(1)+\cdot A_i(0)=A_{i-1}(r_{i})</tex> в случае, когда по <tex>X_i</tex> произведение. К сожалению, сразу этот протокол применить нельзя, потому что произведение может увеличить степень полинома в два раза. Поэтому потребуем, чтобы между появлением переменной и первым ее использованием было не более одного квантора <tex>\forall</tex>. Для этого заменим все суффиксы вида <tex>\forall x_{i+1} \tau(x_1, x_2, \ldots, x_i, x_{i+1})</tex> на <tex>\forall x_{i+1} \exists x_1',\ldots,x_i'(x_1=x_1')\land(x_2=x_2')\land \ldots \land(x_i=x_i')\tau(x_1', x_2', \ldots, x_i', x_{i+1})</tex>. От такого преобразования количество переменных увеличится лишь в полином от их первоначального количества раз, сама формула тоже увеличится не более, чем полиномиально. Теперь после арифметизации по протоколу из [[#SAT]] будут передаваться полиномы не выше второй степени.