		Search-engine friendly clone of the ACL2 documentation.

Decomp.lisp

Envmap->svex-alist

Signature
(envmap->svex-alist envmap) → svalist
Arguments: envmap — Guard (envmap-p envmap).
Returns: svalist — Type (svex-alist-p svalist).

Definitions and Theorems

Function: envmap->svex-alist

(defun envmap->svex-alist (envmap)
  (declare (xargs :guard (envmap-p envmap)))
  (let ((__function__ 'envmap->svex-alist))
    (declare (ignorable __function__))
    (if (atom envmap)
        nil
      (if (mbt (consp (car envmap)))
          (append (svex-alist-fix (cdar envmap))
                  (envmap->svex-alist (cdr envmap)))
        (envmap->svex-alist (cdr envmap))))))

Theorem: svex-alist-p-of-envmap->svex-alist

(defthm svex-alist-p-of-envmap->svex-alist
  (b* ((svalist (envmap->svex-alist envmap)))
    (svex-alist-p svalist))
  :rule-classes :rewrite)

Theorem: envmap->svex-alist-of-append

(defthm envmap->svex-alist-of-append
  (equal (envmap->svex-alist (append a b))
         (append (envmap->svex-alist a)
                 (envmap->svex-alist b))))

Theorem: envmap->svex-alist-of-atom

(defthm envmap->svex-alist-of-atom
  (implies (not (consp envmap))
           (equal (envmap->svex-alist envmap) nil))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: svar-lookup-of-envmap-to-term-alist-under-iff

(defthm svar-lookup-of-envmap-to-term-alist-under-iff
  (iff (svar-lookup k (envmap-to-term-alist x))
       (svar-lookup k (envmap->svex-alist x))))

Theorem: envmap->svex-alist-of-svex-alist-alist-fix-envmap

(defthm envmap->svex-alist-of-svex-alist-alist-fix-envmap
  (equal (envmap->svex-alist (svex-alist-alist-fix envmap))
         (envmap->svex-alist envmap)))

Theorem: envmap->svex-alist-svex-alist-alist-equiv-congruence-on-envmap

(defthm
     envmap->svex-alist-svex-alist-alist-equiv-congruence-on-envmap
  (implies (svex-alist-alist-equiv envmap envmap-equiv)
           (equal (envmap->svex-alist envmap)
                  (envmap->svex-alist envmap-equiv)))
  :rule-classes :congruence)