		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Svdecomp-ev-envmap

Signature
(svdecomp-ev-envmap x env) → res
Arguments: x — Guard (envmap-p x).
Returns: res — Type (svex-env-p res).

Definitions and Theorems

Function: svdecomp-ev-envmap

(defun svdecomp-ev-envmap (x env)
 (declare (xargs :guard (envmap-p x)))
 (let ((__function__ 'svdecomp-ev-envmap))
  (declare (ignorable __function__))
  (if (atom x)
      nil
    (if
      (mbt (consp (car x)))
      (append (ec-call (svex-alist-eval (cdar x)
                                        (svdecomp-ev (caar x) env)))
              (svdecomp-ev-envmap (cdr x) env))
      (svdecomp-ev-envmap (cdr x) env)))))

Theorem: svex-env-p-of-svdecomp-ev-envmap

(defthm svex-env-p-of-svdecomp-ev-envmap
  (b* ((res (svdecomp-ev-envmap x env)))
    (svex-env-p res))
  :rule-classes :rewrite)

Theorem: svdecomp-ev-envmap-of-svex-alist-alist-fix-x

(defthm svdecomp-ev-envmap-of-svex-alist-alist-fix-x
  (equal (svdecomp-ev-envmap (svex-alist-alist-fix x)
                             env)
         (svdecomp-ev-envmap x env)))

Theorem: svdecomp-ev-envmap-svex-alist-alist-equiv-congruence-on-x

(defthm svdecomp-ev-envmap-svex-alist-alist-equiv-congruence-on-x
  (implies (svex-alist-alist-equiv x x-equiv)
           (equal (svdecomp-ev-envmap x env)
                  (svdecomp-ev-envmap x-equiv env)))
  :rule-classes :congruence)