There are several points which should be noted about the addition
and reordering of pattern CEs: 1) The entire LHS of a rule is
considered to be within an implicit and CE; 2) The conversion
of the forall and exists CEs to equivalent not
and and CEs is performed before patterns are added to the
LHS of a rule; 3) In general, it is not very useful to have a
test CE as the first CE within an and CE; and 4)
The output of commands such as the matches
command display information for the CEs that are actually added
to the LHS of a rule and, because of reordering and implicit additions,
may not reflect the rule exactly as defined by the user.