Clause processor that replaces the final call of
(replace-equal-with-top-level-equal clause) → *
Function:
(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:
(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)