		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svex-maskbits-ok

Signature
(svex-maskbits-ok vars masks) → *
Arguments: vars — Guard (svarlist-p vars).; masks — Guard (svex-mask-alist-p masks).

Definitions and Theorems

Function: svex-maskbits-ok

(defun svex-maskbits-ok (vars masks)
  (declare (xargs :guard (and (svarlist-p vars)
                              (svex-mask-alist-p masks))))
  (let ((__function__ 'svex-maskbits-ok))
    (declare (ignorable __function__))
    (b* (((when (atom vars)) t)
         (mask (svex-mask-lookup (svex-var (car vars))
                                 masks))
         ((when (sparseint-< mask 0)) nil))
      (svex-maskbits-ok (cdr vars) masks))))

Theorem: svex-maskbits-ok-of-svarlist-fix-vars

(defthm svex-maskbits-ok-of-svarlist-fix-vars
  (equal (svex-maskbits-ok (svarlist-fix vars)
                           masks)
         (svex-maskbits-ok vars masks)))

Theorem: svex-maskbits-ok-svarlist-equiv-congruence-on-vars

(defthm svex-maskbits-ok-svarlist-equiv-congruence-on-vars
  (implies (svarlist-equiv vars vars-equiv)
           (equal (svex-maskbits-ok vars masks)
                  (svex-maskbits-ok vars-equiv masks)))
  :rule-classes :congruence)

Theorem: svex-maskbits-ok-of-svex-mask-alist-fix-masks

(defthm svex-maskbits-ok-of-svex-mask-alist-fix-masks
  (equal (svex-maskbits-ok vars (svex-mask-alist-fix masks))
         (svex-maskbits-ok vars masks)))

Theorem: svex-maskbits-ok-svex-mask-alist-equiv-congruence-on-masks

(defthm svex-maskbits-ok-svex-mask-alist-equiv-congruence-on-masks
  (implies (svex-mask-alist-equiv masks masks-equiv)
           (equal (svex-maskbits-ok vars masks)
                  (svex-maskbits-ok vars masks-equiv)))
  :rule-classes :congruence)