		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Envmap-to-term-alist

Signature
(envmap-to-term-alist x) → xal
Arguments: x — Guard (envmap-p x).
Returns: xal — Type (and (implies (envmap-p x) (svdecomp-symenv-p xal)) (svar-alist-p xal)) .

Definitions and Theorems

Function: envmap-to-term-alist

(defun envmap-to-term-alist (x)
  (declare (xargs :guard (envmap-p x)))
  (let ((__function__ 'envmap-to-term-alist))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (if (mbt (consp (car x)))
          (append (envmap-entry-to-term-alist (cdar x)
                                              (caar x))
                  (envmap-to-term-alist (cdr x)))
        (envmap-to-term-alist (cdr x))))))

Theorem: return-type-of-envmap-to-term-alist

(defthm return-type-of-envmap-to-term-alist
  (b* ((xal (envmap-to-term-alist x)))
    (and (implies (envmap-p x)
                  (svdecomp-symenv-p xal))
         (svar-alist-p xal)))
  :rule-classes :rewrite)

Theorem: eval-of-envmap-to-term-alist

(defthm eval-of-envmap-to-term-alist
  (equal (svdecomp-ev-symenv (envmap-to-term-alist x)
                             a)
         (svdecomp-ev-envmap x a)))

Theorem: envmap-to-term-alist-of-append

(defthm envmap-to-term-alist-of-append
  (equal (envmap-to-term-alist (append a b))
         (append (envmap-to-term-alist a)
                 (envmap-to-term-alist b))))

Theorem: envmap-to-term-alist-of-svex-alist-alist-fix-x

(defthm envmap-to-term-alist-of-svex-alist-alist-fix-x
  (equal (envmap-to-term-alist (svex-alist-alist-fix x))
         (envmap-to-term-alist x)))

Theorem: envmap-to-term-alist-svex-alist-alist-equiv-congruence-on-x

(defthm envmap-to-term-alist-svex-alist-alist-equiv-congruence-on-x
  (implies (svex-alist-alist-equiv x x-equiv)
           (equal (envmap-to-term-alist x)
                  (envmap-to-term-alist x-equiv)))
  :rule-classes :congruence)