`definition` and `rewrite` rules used in
preprocessing

Example of simple rewrite rule: (equal (car (cons x y)) x) Examples of simple definition: (defun file-clock-p (x) (integerp x)) (defun naturalp (x) (and (integerp x) (>= x 0)))

The theorem prover output sometimes refers to ``simple'' definitions and
rewrite rules. These rules can be used by the preprocessor, which is one of
the theorem prover's ``processes'' understood by the

The preprocessor expands certain definitions and uses certain rewrite rules
that it considers to be ``fast''. There are two ways to qualify as fast. One
is to be an ``abbreviation'', where a rewrite rule with no hypotheses or loop
stopper is an ``abbreviation'' if the right side contains no more variable
occurrences than the left side, and the right side does not call the functions
`if`, `not` or `implies`. Definitions and rewrite rules can
both be abbreviations; the criterion for definitions is similar, except that
the definition must not be recursive. The other way to qualify applies only
to a non-recursive definition, and applies when its body is a disjunction or
conjunction, according to a perhaps subtle criterion that is intended to avoid
case splits.