		Search-engine friendly clone of the ACL2 documentation.

Top-level-equal

Replace-equal-with-top-level-equal

Clause processor that replaces the final call of equal in a theorem conclusion with top-level-equal.

Signature
(replace-equal-with-top-level-equal clause) → *
Arguments: clause — Guard (pseudo-term-listp clause).

Definitions and Theorems

Function: replace-equal-with-top-level-equal

(defun replace-equal-with-top-level-equal (clause)
  (declare (xargs :guard (pseudo-term-listp clause)))
  (let ((__function__ 'replace-equal-with-top-level-equal))
    (declare (ignorable __function__))
    (list (append (butlast clause 1)
                  (list (replace-equal-with-top-level-equal-rec
                             (car (last clause))))))))

Theorem: replace-equal-with-top-level-equal-correct

(defthm replace-equal-with-top-level-equal-correct
 (implies
  (and
   (pseudo-term-listp clause)
   (alistp a)
   (repl-equal-ev
       (conjoin-clauses (replace-equal-with-top-level-equal clause))
       a))
  (repl-equal-ev (disjoin clause) a))
 :rule-classes :clause-processor)