We make two simplifying assumptions to keep our discussion from being too intricate. We assume no \(\phi_i\) contains a nested \(\textsf{ where }\) clause. The basic ideas are amply illustrated with this condition imposed, but everything extends to the general case without too much difficulty. It is a general requirement that the variables in \(\bx_i\) are ‘local’ to \(P_i(\bx_i) \simeq \phi_i\), that is, they are considered to be bound in this formula. To this we add another simplifying assumption: the variables in \(\bx_i\) are the only variables that may occur free in \(\phi_i\). Roughly this means that we have no parameters, only local variables. This serves to allow us to discuss things with less clutter. Again, everything extends to the more general case with no fundamental changes.