		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Svdecomp-normalize-svexlist-eval

Signature
(svdecomp-normalize-svexlist-eval x env rec-limit) → (mv newx newenv)
Arguments: x — Guard (svexlist-p x).; env — Guard (svdecomp-symenv-p env).; rec-limit — Guard (natp rec-limit).
Returns: newx — Type (svexlist-p newx).; newenv — Type (svdecomp-symenv-p newenv), given (svdecomp-symenv-p env).

Definitions and Theorems

Function: svdecomp-normalize-svexlist-eval

(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: svexlist-p-of-svdecomp-normalize-svexlist-eval.newx

(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: svdecomp-symenv-p-of-svdecomp-normalize-svexlist-eval.newenv

(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: svdecomp-normalize-svex-eval-correct

(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: svdecomp-normalize-svex-eval-correct-single

(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: len-of-svdecomp-normalize-svexlist-eval-newx

(defthm len-of-svdecomp-normalize-svexlist-eval-newx
 (equal
   (len (mv-nth 0
                (svdecomp-normalize-svexlist-eval x env rec-limit)))
   (len x)))

Theorem: consp-of-svdecomp-normalize-svexlist-eval-newx

(defthm consp-of-svdecomp-normalize-svexlist-eval-newx
 (equal
   (consp
        (mv-nth 0
                (svdecomp-normalize-svexlist-eval x env rec-limit)))
   (consp x)))

Theorem: svdecomp-normalize-svexlist-eval-of-svexlist-fix-x

(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: svdecomp-normalize-svexlist-eval-svexlist-equiv-congruence-on-x

(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: svdecomp-normalize-svexlist-eval-of-nfix-rec-limit

(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: svdecomp-normalize-svexlist-eval-nat-equiv-congruence-on-rec-limit

(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)