Изменения

|proof=Чтобы доказать это, просто приведём программу <tex>solve</tex>, решающую булеву формулу с кванторами на <tex>O(n)</tex> дополнительной памяти и работающую за конечное время.

<tex>solve(Q_k x_k \ldots Q_n x_n \phi(x_1, x_2, \ldots, x_n))</tex>

'''return''' <tex>\phi(x_1, x_2, \ldots, x_n)</tex>

'''if''' <tex>Q_k = \forall</tex>