(replace-equal-with-top-level-equal-rec x) → new-x
Function:
(defun replace-equal-with-top-level-equal-rec (x) (declare (xargs :guard (pseudo-termp x))) (let ((__function__ 'replace-equal-with-top-level-equal-rec)) (declare (ignorable __function__)) (pseudo-term-case x :fncall (cond ((eq x.fn 'equal) (pseudo-term-fncall 'top-level-equal x.args)) ((eq x.fn 'implies) (pseudo-term-fncall 'implies (list (first x.args) (replace-equal-with-top-level-equal-rec (second x.args))))) ((eq x.fn 'if) (if (equal (third x.args) ''nil) (pseudo-term-fncall 'if (list (replace-equal-with-top-level-equal-rec (first x.args)) (replace-equal-with-top-level-equal-rec (second x.args)) ''nil)) (pseudo-term-fncall 'if (list (first x.args) (replace-equal-with-top-level-equal-rec (second x.args)) (replace-equal-with-top-level-equal-rec (third x.args)))))) ((eq x.fn 'return-last) (pseudo-term-fncall 'return-last (list (first x.args) (second x.args) (replace-equal-with-top-level-equal-rec (third x.args))))) (t (pseudo-term-fix x))) :lambda (pseudo-term-lambda x.formals (replace-equal-with-top-level-equal-rec x.body) x.args) :otherwise (pseudo-term-fix x))))
Theorem:
(defthm pseudo-termp-of-replace-equal-with-top-level-equal-rec (b* ((new-x (replace-equal-with-top-level-equal-rec x))) (pseudo-termp new-x)) :rule-classes :rewrite)
Theorem:
(defthm replace-equal-with-top-level-equal-rec-correct (equal (repl-equal-ev (replace-equal-with-top-level-equal-rec x) a) (repl-equal-ev x a)))