In Section 2.3.1 we begin with expressions of the form:
where each 
is a variable appearing in term P and each 
is
a sort restriction on the corresponding 
. We then define a
condition for each variable which conforms to the sort
restriction on the variable and may relate it to other variables, thus
producing the refined expression:
where each 
is a condition on 
conforming to the sort
restriction 
and involving predicates which we define in subsequent
design. A similar pattern was followed in Section 2.3.2.