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.