Изменения

'''Предваренная нормальная форма''' {{---}} форма, при которой в начале выражения записаны все кванторы, а затем глобальное условие.

}}

После того, как выражение приведено в предваренную нормальную форму, в глобальном условии оказалось множество переменных. Для каждой переменной определен диапазон, из которого она берет значения, поэтому можно построить соответсвующее декартово произведение. Другими словами, берем все переменные и строим потенциально огромное декартово произведение. Теперь его необходимо отфильтровать по глобальному условию из предваренной нормальной формы. Для каждого кортежа из декартово произведения зафиксированы все значения, поэтому для каждого из них можно проверить, истинно оно или нет. Проверили, то есть сделали фильтр по условию, теперь необходимо применить кванторы.