(svdecomp-normalize-svexlist-eval x env rec-limit) → (mv newx newenv)
Function:
(defun svdecomp-normalize-svexlist-eval (x env rec-limit) (declare (xargs :guard (and (svexlist-p x) (svdecomp-symenv-p env) (natp rec-limit)))) (let ((__function__ 'svdecomp-normalize-svexlist-eval)) (declare (ignorable __function__)) (b* (((when (zp rec-limit)) (mv (svexlist-fix x) env)) (vars (mergesort (cwtime (svexlist-collect-vars x)))) ((mv err svalist env1) (cwtime (svex-decomp-process-env-term env vars))) ((when err) (cw "Svdecomp error: ~@0~%" err) (mv (svexlist-fix x) env)) ((when (atom svalist)) (mv (svexlist-fix x) env1)) (newx (with-fast-alist svalist (cwtime (svexlist-compose x svalist))))) (clear-memoize-table 'svex-compose) (svdecomp-normalize-svexlist-eval newx env1 (1- rec-limit)))))
Theorem:
(defthm svexlist-p-of-svdecomp-normalize-svexlist-eval.newx (b* (((mv ?newx ?newenv) (svdecomp-normalize-svexlist-eval x env rec-limit))) (svexlist-p newx)) :rule-classes :rewrite)
Theorem:
(defthm svdecomp-symenv-p-of-svdecomp-normalize-svexlist-eval.newenv (implies (svdecomp-symenv-p env) (b* (((mv ?newx ?newenv) (svdecomp-normalize-svexlist-eval x env rec-limit))) (svdecomp-symenv-p newenv))) :rule-classes :rewrite)
Theorem:
(defthm svdecomp-normalize-svex-eval-correct (b* (((mv newx newenv) (svdecomp-normalize-svexlist-eval x env rec-limit))) (equal (svexlist-eval newx (svdecomp-ev-symenv newenv a)) (svexlist-eval x (svdecomp-ev-symenv env a)))))
Theorem:
(defthm svdecomp-normalize-svex-eval-correct-single (b* (((mv newx newenv) (svdecomp-normalize-svexlist-eval (list x) env rec-limit))) (equal (svex-eval (car newx) (svdecomp-ev-symenv newenv a)) (svex-eval x (svdecomp-ev-symenv env a)))))
Theorem:
(defthm len-of-svdecomp-normalize-svexlist-eval-newx (equal (len (mv-nth 0 (svdecomp-normalize-svexlist-eval x env rec-limit))) (len x)))
Theorem:
(defthm consp-of-svdecomp-normalize-svexlist-eval-newx (equal (consp (mv-nth 0 (svdecomp-normalize-svexlist-eval x env rec-limit))) (consp x)))
Theorem:
(defthm svdecomp-normalize-svexlist-eval-of-svexlist-fix-x (equal (svdecomp-normalize-svexlist-eval (svexlist-fix x) env rec-limit) (svdecomp-normalize-svexlist-eval x env rec-limit)))
Theorem:
(defthm svdecomp-normalize-svexlist-eval-svexlist-equiv-congruence-on-x (implies (svexlist-equiv x x-equiv) (equal (svdecomp-normalize-svexlist-eval x env rec-limit) (svdecomp-normalize-svexlist-eval x-equiv env rec-limit))) :rule-classes :congruence)
Theorem:
(defthm svdecomp-normalize-svexlist-eval-of-nfix-rec-limit (equal (svdecomp-normalize-svexlist-eval x env (nfix rec-limit)) (svdecomp-normalize-svexlist-eval x env rec-limit)))
Theorem:
(defthm svdecomp-normalize-svexlist-eval-nat-equiv-congruence-on-rec-limit (implies (nat-equiv rec-limit rec-limit-equiv) (equal (svdecomp-normalize-svexlist-eval x env rec-limit) (svdecomp-normalize-svexlist-eval x env rec-limit-equiv))) :rule-classes :congruence)