		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svex-mask-alist-extract-vars

Signature
(svex-mask-alist-extract-vars x) → new-x
Arguments: x — Guard (svex-mask-alist-p x).
Returns: new-x — Type (svex-mask-alist-p new-x).

Definitions and Theorems

Function: svex-mask-alist-extract-vars

(defun svex-mask-alist-extract-vars (x)
  (declare (xargs :guard (svex-mask-alist-p x)))
  (let ((__function__ 'svex-mask-alist-extract-vars))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (if (and (mbt (svex-p (caar x)))
               (eq (svex-kind (caar x)) :var))
          (hons-acons (caar x)
                      (4vmask-fix (cdar x))
                      (svex-mask-alist-extract-vars (cdr x)))
        (svex-mask-alist-extract-vars (cdr x))))))

Theorem: svex-mask-alist-p-of-svex-mask-alist-extract-vars

(defthm svex-mask-alist-p-of-svex-mask-alist-extract-vars
  (b* ((new-x (svex-mask-alist-extract-vars x)))
    (svex-mask-alist-p new-x))
  :rule-classes :rewrite)

Theorem: lookup-in-svex-mask-alist-extract-vars

(defthm lookup-in-svex-mask-alist-extract-vars
  (b* ((?new-x (svex-mask-alist-extract-vars x)))
    (equal (hons-assoc-equal s new-x)
           (and (svex-p s)
                (equal (svex-kind s) :var)
                (hons-assoc-equal s (svex-mask-alist-fix x))))))

Theorem: svex-mask-lookup-in-svex-mask-alist-extract-vars

(defthm svex-mask-lookup-in-svex-mask-alist-extract-vars
  (b* ((?new-x (svex-mask-alist-extract-vars x)))
    (equal (svex-mask-lookup s new-x)
           (if (equal (svex-kind s) :var)
               (svex-mask-lookup s x)
             0))))

Theorem: svex-maskbits-ok-of-svex-mask-alist-extract-vars

(defthm svex-maskbits-ok-of-svex-mask-alist-extract-vars
  (b* ((?new-x (svex-mask-alist-extract-vars x)))
    (iff (svex-maskbits-ok vars new-x)
         (svex-maskbits-ok vars x))))

Theorem: svex-maskbits-for-vars-of-svex-mask-alist-extract-vars

(defthm svex-maskbits-for-vars-of-svex-mask-alist-extract-vars
  (b* ((?new-x (svex-mask-alist-extract-vars x)))
    (equal (svex-maskbits-for-vars vars new-x boolmasks)
           (svex-maskbits-for-vars vars x boolmasks))))

Theorem: svex-mask-alist-extract-vars-of-svex-mask-alist-fix-x

(defthm svex-mask-alist-extract-vars-of-svex-mask-alist-fix-x
  (equal (svex-mask-alist-extract-vars (svex-mask-alist-fix x))
         (svex-mask-alist-extract-vars x)))

Theorem: svex-mask-alist-extract-vars-svex-mask-alist-equiv-congruence-on-x

(defthm
 svex-mask-alist-extract-vars-svex-mask-alist-equiv-congruence-on-x
 (implies (svex-mask-alist-equiv x x-equiv)
          (equal (svex-mask-alist-extract-vars x)
                 (svex-mask-alist-extract-vars x-equiv)))
 :rule-classes :congruence)