(svdecomp-svex-alist-eval-metafun x) → newx
Function:
(defun svdecomp-svex-alist-eval-metafun (x) (declare (xargs :guard (pseudo-termp x))) (let ((__function__ 'svdecomp-svex-alist-eval-metafun)) (declare (ignorable __function__)) (b* (((acl2::unless-match x (svex-alist-eval '(:? svexal) (:? env))) (cw "svdecomp-svexlist-eval-meta failed, probably running on non-concrete svex~%") x) ((unless (svex-alist-p svexal)) (cw "svdecomp-svexlist-eval-meta failed because the svexlist was not svexlist-p~%") x) ((mv err symenv) (map-alist-term-keys-to-val-terms env)) ((when err) (cw "svdecomp-svex-eval-meta failed to process the environment term: ~@0~%" err) x) ((mv newsvexes newenv) (svdecomp-normalize-svexlist-eval (svex-alist-vals svexal) symenv 10))) (cons 'svex-alist-eval (cons (cons 'quote (cons (pairlis$ (svex-alist-keys svexal) newsvexes) 'nil)) (cons (svdecomp-symenv->term newenv) 'nil))))))
Theorem:
(defthm pseudo-termp-of-svdecomp-svex-alist-eval-metafun (implies (and (pseudo-termp x)) (b* ((newx (svdecomp-svex-alist-eval-metafun x))) (pseudo-termp newx))) :rule-classes :rewrite)
Theorem:
(defthm svdecomp-svex-alist-eval-meta (equal (svdecomp-ev x a) (svdecomp-ev (svdecomp-svex-alist-eval-metafun x) a)) :rule-classes ((:meta :trigger-fns (svex-eval))))