		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svexlist-mask-alist

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

Definitions and Theorems

Function: svexlist-mask-alist

(defun svexlist-mask-alist (x)
  (declare (xargs :guard (svexlist-p x)))
  (let ((__function__ 'svexlist-mask-alist))
    (declare (ignorable __function__))
    (b* (((mv mask-al ?toposort)
          (svexlist-mask-alist/toposort x)))
      mask-al)))

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

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

Theorem: svexlist-mask-alist-of-svexlist-fix-x

(defthm svexlist-mask-alist-of-svexlist-fix-x
  (equal (svexlist-mask-alist (svexlist-fix x))
         (svexlist-mask-alist x)))

Theorem: svexlist-mask-alist-svexlist-equiv-congruence-on-x

(defthm svexlist-mask-alist-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-mask-alist x)
                  (svexlist-mask-alist x-equiv)))
  :rule-classes :congruence)

Theorem: svexlist-mask-alist-complete

(defthm svexlist-mask-alist-complete
  (svex-mask-alist-complete (svexlist-mask-alist x)))

Theorem: svexlist-mask-alist-lookup

(defthm svexlist-mask-alist-lookup
  (implies (member-equal (svex-fix y)
                         (svexlist-fix x))
           (equal (svex-mask-lookup y (svexlist-mask-alist x))
                  -1)))

Theorem: svex-argmasks-lookup-of-svexlist-mask-alist

(defthm svex-argmasks-lookup-of-svexlist-mask-alist
  (implies (subsetp-equal (svexlist-fix y)
                          (svexlist-fix x))
           (equal (svex-argmasks-lookup y (svexlist-mask-alist x))
                  (replicate (len y) -1))))

Theorem: svexlist-mask-alist/toposort-to-mask-alist

(defthm svexlist-mask-alist/toposort-to-mask-alist
  (equal (svexlist-mask-alist/toposort x)
         (mv (svexlist-mask-alist x)
             (mv-nth 0 (svexlist-toposort x nil nil)))))