SIMPLE

Major Section:  MISCELLANEOUS

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 :do-not hint; see hints.

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.