 In this each \(\bx_i\) is a sequence of variables whose length is the arity of \(P_i\). The \(P_i\) may appear in the formulas \(\phi_0\), …, \(\phi_k\) themselves, and so we have a self-referential set of defining equations, with \(\phi_0\) as ‘output’. Note that with \eqref{whereformula} added to the definition of formula, \(\textsf{ where }\) conditions can appear in some of the \(\phi_i\), and so means of preventing inappropriate interaction between nested conditions is needed. This is done through the familiar machinery of free and bound variables. The symbols \(P_1\), …, \(P_k\) are taken to be relation variables, and are considered to be bound in \eqref{whereformula}. Likewise the occurrences of individual variables in \(\bx_i\) are understood to be bound in \(P_i(\bx_i) \simeq \phi_i\). In effect, these are local variables.