		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Svdecomp-ev-symenv

Signature
(svdecomp-ev-symenv x env) → res
Arguments: x — Guard (svdecomp-symenv-p x).
Returns: res — Type (svar-alist-p res).

Definitions and Theorems

Function: svdecomp-ev-symenv

(defun svdecomp-ev-symenv (x env)
  (declare (xargs :guard (svdecomp-symenv-p x)))
  (let ((__function__ 'svdecomp-ev-symenv))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (if (mbt (and (consp (car x)) (svar-p (caar x))))
          (cons (cons (caar x)
                      (svdecomp-ev (cdar x) env))
                (svdecomp-ev-symenv (cdr x) env))
        (svdecomp-ev-symenv (cdr x) env)))))

Theorem: svar-alist-p-of-svdecomp-ev-symenv

(defthm svar-alist-p-of-svdecomp-ev-symenv
  (b* ((res (svdecomp-ev-symenv x env)))
    (svar-alist-p res))
  :rule-classes :rewrite)

Theorem: eval-lookup-of-svdecomp-ev-symenv

(defthm eval-lookup-of-svdecomp-ev-symenv
  (equal (svar-lookup k (svdecomp-ev-symenv x env))
         (and (svar-lookup k x)
              (cons (svar-fix k)
                    (svdecomp-ev (cdr (svar-lookup k x))
                                 env)))))

Theorem: svdecomp-ev-symenv-of-svar-alist-fix-x

(defthm svdecomp-ev-symenv-of-svar-alist-fix-x
  (equal (svdecomp-ev-symenv (svar-alist-fix x)
                             env)
         (svdecomp-ev-symenv x env)))

Theorem: svdecomp-ev-symenv-svar-alist-equiv-congruence-on-x

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