As we noted above, we have not described in detail how applications of theorems as rewrite rules are carried out. Recall that all theorems proved by Watson are equations (implicitly universally quantified over their free variables) and so are suitable for use as rewrite rules.

As we stated above, the user views the right side of the equational
theorem under construction. In fact, the user views not only the
right side, but also a selected subterm of the right side. When the
user applies a theorem as a rewrite rule, it is to this selected
subterm that he applies it. The user does *not* rewrite proper
subterms of the selected subterm to which the rewrite rule is
applicable (as he would in most rewriting systems); the
appropriate side of the rewrite rule is matched only to the selected
subterm itself (and applied if applicable).

The user has further commands at his disposal which control which subterm of the right side of the equation is selected to view. These are referred to collectively as ``term navigation commands''. These include commands to move to the right or left subterm of the current selected subterm, to the parent subterm of the current selected subterm, or to the top term (the entire right side of the equation). There are some more sophisticated navigation commands as well.

Certain terms present technical challenges under this picture. An
abstraction term has only one immediate subterm: moving to the left or
to the right takes one to that same subterm. A case expression `?p || ?x, ?y` doesn't really have an immediate right subterm; the
prover allows one to move to this virtual subterm on the way to
modifying its real left and right subterms, but it does not allow the
application of rewrite rules to the virtual subterm. Moving to the
left in a prefix term will reveal the hidden left subterm if there is
one and produce a subterm error otherwise.

The selected subterm is enclosed in braces `{}` in the display of
the entire right subterm, unless it happens to be the virtual subterm of
a case expression.