(svdecomp-equal-svex-evals-metafun x mfc state) → newx
Function:
(defun svdecomp-equal-svex-evals-metafun (x mfc state) (declare (xargs :stobjs (state))) (declare (xargs :guard (pseudo-termp x))) (declare (ignorable mfc)) (let ((__function__ 'svdecomp-equal-svex-evals-metafun)) (declare (ignorable __function__)) (b* (((acl2::when-match x (equal (svex-eval '(:? svex1) (:? env1)) (svex-eval '(:? svex2) (:? env2)))) (cwtime (b* (((mv env1 env2) (mbe :logic (mv env1 env2) :exec (let ((pair (hons env1 env2))) (mv (car pair) (cdr pair))))) ((unless (and (svex-p svex1) (svex-p svex2))) (cw "svdecomp-svex-eval-meta failed because the svex was not svex-p~%") x) ((mv err symenv1) (map-alist-term-keys-to-val-terms env1)) ((when err) (fmt-to-comment-window "svdecomp-svex-eval-meta failed to process the environment term: ~@0~%" (cons (cons '#\0 err) 'nil) 0 '(nil 8 10 nil) nil) x) ((mv err symenv2) (map-alist-term-keys-to-val-terms env2)) ((when err) (cw "svdecomp-svex-eval-meta failed to process the environment term: ~@0~%" err) x) ((mv newsvexlist1 newenv1) (cwtime (svdecomp-normalize-svexlist-eval (list svex1) symenv1 10) :mintime 1)) ((mv newsvexlist2 newenv2) (cwtime (svdecomp-normalize-svexlist-eval (list svex2) symenv2 10) :mintime 1)) (limit (svdecomp-get-rewrite-limit state)) ((mv newsvexlist1 newsvexlist2) (cwtime (svexlists-rewrite-until-same newsvexlist1 newsvexlist2 limit) :mintime 1)) (newsvex1 (nth 0 newsvexlist1)) (newsvex2 (nth 0 newsvexlist2))) (if (hons-equal newenv1 newenv2) (cw "Environments are equal.~%") (cw "Environments differ~%")) (if (hons-equal newsvex1 newsvex2) (cw "Svexes are equal.~%") (cw "Svexes differ.~%")) (svdecomp-svex?-eval-compare-term newsvex1 newsvex2 newenv1 newenv2 'svex-eval)) :name svdecomp-equal-svex-evals-metafun))) x)))
Theorem:
(defthm pseudo-termp-of-svdecomp-equal-svex-evals-metafun (implies (and (state-p state) (pseudo-termp x)) (b* ((newx (svdecomp-equal-svex-evals-metafun x mfc state))) (pseudo-termp newx))) :rule-classes :rewrite)
Theorem:
(defthm svdecomp-equal-svex-evals-meta (equal (svdecomp-ev x a) (svdecomp-ev (svdecomp-equal-svex-evals-metafun x mfc state) a)) :rule-classes ((:meta :trigger-fns (equal))))