		Search-engine friendly clone of the ACL2 documentation.

Svex-alist

Svex-alist-vals

Like alist-vals but with proper fty-discipline for svex-alists.

Signature
(svex-alist-vals x) → vals
Arguments: x — Guard (svex-alist-p x).
Returns: vals — Type (svexlist-p vals).

Definitions and Theorems

Function: svex-alist-vals

(defun
 svex-alist-vals (x)
 (declare (xargs :guard (svex-alist-p x)))
 (let
   ((__function__ 'svex-alist-vals))
   (declare (ignorable __function__))
   (mbe :logic (if (atom x)
                   nil
                   (if (mbt (and (consp (car x)) (svar-p (caar x))))
                       (cons (mbe :logic (svex-fix (cdar x))
                                  :exec (cdar x))
                             (svex-alist-vals (cdr x)))
                       (svex-alist-vals (cdr x))))
        :exec (strip-cdrs x))))

Theorem: svexlist-p-of-svex-alist-vals

(defthm svexlist-p-of-svex-alist-vals
        (b* ((vals (svex-alist-vals x)))
            (svexlist-p vals))
        :rule-classes :rewrite)

Theorem: svex-alist-vals-of-svex-alist-fix-x

(defthm svex-alist-vals-of-svex-alist-fix-x
        (equal (svex-alist-vals (svex-alist-fix x))
               (svex-alist-vals x)))

Theorem: svex-alist-vals-svex-alist-equiv-congruence-on-x

(defthm svex-alist-vals-svex-alist-equiv-congruence-on-x
        (implies (svex-alist-equiv x x-equiv)
                 (equal (svex-alist-vals x)
                        (svex-alist-vals x-equiv)))
        :rule-classes :congruence)

Theorem: member-svex-alist-vals-when-svex-lookup

(defthm member-svex-alist-vals-when-svex-lookup
        (implies (svex-lookup k x)
                 (member (svex-lookup k x)
                         (svex-alist-vals x))))

Theorem: svex-alist-vals-of-svex-acons

(defthm svex-alist-vals-of-svex-acons
        (equal (svex-alist-vals (svex-acons k v x))
               (cons (svex-fix v)
                     (svex-alist-vals x))))

Theorem: len-of-svex-alist-vals

(defthm len-of-svex-alist-vals
        (equal (len (svex-alist-vals x))
               (len (svex-alist-keys x))))

Theorem: svex-alist-vals-of-pairlis$

(defthm svex-alist-vals-of-pairlis$
        (implies (and (equal (len x) (len y))
                      (svarlist-p x))
                 (equal (svex-alist-vals (pairlis$ x y))
                        (svexlist-fix y))))