Limit application of permutative rewrite rules

See rule-classes for a discussion of the syntax of the
`rewrite` rule-classes. Here we
describe how that field is used, and also how that field is created when the
user does not explicitly supply it.

For example, the built-in `rewrite` rule

(implies (and (acl2-numberp x) (acl2-numberp y)) (equal (+ x y) (+ y x))),

creates a rewrite rule with a loop-stopper of `binary-+` in the list means that certain
functions that are ``invisible'' with respect to `binary-+` (by default,
`unary--` is the only such function) are more or less ignored when
making this ``smaller'' test. We are much more precise below.

Our explanation of loop-stopping is in four parts. First we discuss ACL2's
notion of ``term order.'' Next, we bring in the notion of ``invisibility'',
and use it together with term order to define orderings on terms that are used
in the loop-stopping algorithm. Third, we describe that algorithm. These
topics all assume that we have in hand the

ACL2 must sometimes decide which of two terms is syntactically simpler. It
uses a total ordering on terms, called the ``term order.'' Under this
ordering constants such as

When the loop-stopping algorithm is controlling the use of permutative
`rewrite` rules it allows **not** the above explained term order but a
more complicated ordering described below. The use of a total ordering stops
rules like commutativity from looping indefinitely because it allows `binary-+` tree denoted by the term

Suppose the loop-stopping algorithm used term order, as noted above, and
consider the `binary-+` tree denoted by `+` function
above.

Briefly, a unary function symbol `invisible-fns-table`; also see set-invisible-fns-table, which
explains its format and how it can be set by the user. Roughly speaking,
``invisible'' function symbols are ignored for the purposes of the term-order
test.

Consider the example above, `invisible-fns-table` makes `unary--` invisible with respect to `binary-+`. The commutativity rule for `binary-+` will attempt to swap
`binary-+` expression, `unary--` is invisible.
Thus, instead of comparing

Here is a more precise specification of the total order used for
loop-stopping with respect to a list,

Now we may describe the loop-stopping algorithm. Consider a rewrite rule
with conclusion `pr` with the name of the rule; see pr.)
We describe when rewriting is permitted. The simplest case is when the
loop-stopper list is

It remains only to describe how the loop-stopper field is calculated for a
rewrite rule when this field is not supplied by the user. (On the other hand,
to see how the user may specify the

- Invisible-fns-table
- Functions that are invisible to the loop-stopper algorithm
- Set-invisible-fns-table
- Set the invisible functions table
- Add-invisible-fns
- Make some unary functions invisible to the loop-stopper algorithm
- Remove-invisible-fns
- Make some unary functions no longer invisible