(svdecomp-svex?-eval-compare-term x y env1 env2 eval-fn) → eq
Function:
(defun svdecomp-svex?-eval-compare-term (x y env1 env2 eval-fn) (declare (xargs :guard (and (svdecomp-symenv-p env1) (svdecomp-symenv-p env2)))) (let ((__function__ 'svdecomp-svex?-eval-compare-term)) (declare (ignorable __function__)) (if (and (hons-equal x y) (hons-equal env1 env2)) (prog2$ (cw "Resulting svexes are equal~%") ''t) (prog2$ (cw "Resulting svexes aren't equal~%") (cons 'svdecomp-equal (cons (cons eval-fn (cons (cons 'quote (cons x 'nil)) (cons (svdecomp-symenv->term env1) 'nil))) (cons (cons eval-fn (cons (cons 'quote (cons y 'nil)) (cons (svdecomp-symenv->term env2) 'nil))) 'nil)))))))
Theorem:
(defthm pseudo-termp-of-svdecomp-svex?-eval-compare-term (implies (and (svdecomp-symenv-p env1) (svdecomp-symenv-p env2) (symbolp eval-fn) (not (eq eval-fn 'quote))) (b* ((eq (svdecomp-svex?-eval-compare-term x y env1 env2 eval-fn))) (pseudo-termp eq))) :rule-classes :rewrite)
Theorem:
(defthm svdecomp-svex?-eval-compare-term-correct (equal (svdecomp-ev (svdecomp-svex?-eval-compare-term x y env1 env2 eval-fn) a) (equal (svdecomp-ev (cons eval-fn (cons (cons 'quote (cons x 'nil)) (cons (svdecomp-symenv->term env1) 'nil))) a) (svdecomp-ev (cons eval-fn (cons (cons 'quote (cons y 'nil)) (cons (svdecomp-symenv->term env2) 'nil))) a))))