		Search-engine friendly clone of the ACL2 documentation.

4vmask

4vec-mask?

Signature
(4vec-mask? mask care dontcare) → res
Arguments: mask — Guard (4vmask-p mask).; care — Guard (4vec-p care).; dontcare — Guard (4vec-p dontcare).
Returns: res — Type (4vec-p res).

Definitions and Theorems

Function: 4vec-mask?

(defun 4vec-mask? (mask care dontcare)
  (declare (xargs :guard (and (4vmask-p mask)
                              (4vec-p care)
                              (4vec-p dontcare))))
  (let ((__function__ '4vec-mask?))
    (declare (ignorable __function__))
    (b* (((4vec care))
         ((4vec dontcare))
         (mask (sparseint-val (4vmask-fix mask))))
      (4vec (logite mask care.upper dontcare.upper)
            (logite mask care.lower dontcare.lower)))))

Theorem: 4vec-p-of-4vec-mask?

(defthm 4vec-p-of-4vec-mask?
  (b* ((res (4vec-mask? mask care dontcare)))
    (4vec-p res))
  :rule-classes :rewrite)

Theorem: 4vec-mask?-same

(defthm 4vec-mask?-same
  (equal (4vec-mask? mask x x)
         (4vec-fix x)))

Theorem: 4vec-mask?-of-4vec-mask?

(defthm 4vec-mask?-of-4vec-mask?
  (equal (4vec-mask? mask x (4vec-mask? mask y z))
         (4vec-mask? mask x z)))

Theorem: 4vec-mask?-of-4vec-mask

(defthm 4vec-mask?-of-4vec-mask
  (equal (4vec-mask? mask b (4vec-mask mask b))
         (4vec-mask mask b)))

Theorem: 4vec-mask-of-4vec-mask?

(defthm 4vec-mask-of-4vec-mask?
  (equal (4vec-mask mask (4vec-mask? mask a b))
         (4vec-mask mask a)))

Theorem: equal-of-4vec-mask?-when-equal-under-mask

(defthm equal-of-4vec-mask?-when-equal-under-mask
  (equal (equal x (4vec-mask? mask y x))
         (and (4vec-p x)
              (equal (4vec-mask mask x)
                     (4vec-mask mask y)))))

Theorem: 4vec-mask?-constants

(defthm 4vec-mask?-constants
  (and (equal (4vec-mask? -1 care dontcare)
              (4vec-fix care))
       (equal (4vec-mask? 0 care dontcare)
              (4vec-fix dontcare))))