limit application of permutative rewrite rules  See rule-classes
for a discussion of the syntax of the :loop-stopper field of
: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
commutativity-of-+,  (implies (and (acl2-numberp x)
(acl2-numberp y))          (equal (+ x y) (+ y x))), creates a
rewrite rule with a loop-stopper of ((x y binary-+)). This
means, very roughly, that the term corresponding to y must be
``smaller'' than the term corresponding to x in order for this
rule to apply. However, the presence 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 th