		Search-engine friendly clone of the ACL2 documentation.

4vmask

4veclist-mask

Reduce a list of constant 4vecs using individual 4vmasks; any irrelevant bits become Xes.

Signature
(4veclist-mask masks values) → masked-values
Arguments: masks — List of 4vmasks to use.
Guard (4vmasklist-p masks).; values — List of 4vecs to simplify.
Guard (4veclist-p values).
Returns: masked-values — Updated 4vecs with irrelevant bits replaced by Xes.
Type (4veclist-p masked-values).

Definitions and Theorems

Function: 4veclist-mask

(defun 4veclist-mask (masks values)
  (declare (xargs :guard (and (4vmasklist-p masks)
                              (4veclist-p values))))
  (let ((__function__ '4veclist-mask))
    (declare (ignorable __function__))
    (cond ((atom values) nil)
          ((atom masks) (4veclist-fix values))
          (t (cons (4vec-mask (car masks) (car values))
                   (4veclist-mask (cdr masks)
                                  (cdr values)))))))

Theorem: 4veclist-p-of-4veclist-mask

(defthm 4veclist-p-of-4veclist-mask
  (b* ((masked-values (4veclist-mask masks values)))
    (4veclist-p masked-values))
  :rule-classes :rewrite)

Theorem: 4veclist-mask-of-4vmasklist-fix-masks

(defthm 4veclist-mask-of-4vmasklist-fix-masks
  (equal (4veclist-mask (4vmasklist-fix masks)
                        values)
         (4veclist-mask masks values)))

Theorem: 4veclist-mask-4vmasklist-equiv-congruence-on-masks

(defthm 4veclist-mask-4vmasklist-equiv-congruence-on-masks
  (implies (4vmasklist-equiv masks masks-equiv)
           (equal (4veclist-mask masks values)
                  (4veclist-mask masks-equiv values)))
  :rule-classes :congruence)

Theorem: 4veclist-mask-of-4veclist-fix-values

(defthm 4veclist-mask-of-4veclist-fix-values
  (equal (4veclist-mask masks (4veclist-fix values))
         (4veclist-mask masks values)))

Theorem: 4veclist-mask-4veclist-equiv-congruence-on-values

(defthm 4veclist-mask-4veclist-equiv-congruence-on-values
  (implies (4veclist-equiv values values-equiv)
           (equal (4veclist-mask masks values)
                  (4veclist-mask masks values-equiv)))
  :rule-classes :congruence)

Theorem: len-of-4veclist-mask

(defthm len-of-4veclist-mask
  (equal (len (4veclist-mask masks values))
         (len values)))

Theorem: 4veclist-mask-of-nil

(defthm 4veclist-mask-of-nil
  (equal (4veclist-mask nil x)
         (4veclist-fix x)))

Theorem: equal-of-4veclist-mask-cons

(defthm equal-of-4veclist-mask-cons
  (equal (equal (4veclist-mask (cons m1 m) x)
                (4veclist-mask (cons m1 m) y))
         (and (equal (consp x) (consp y))
              (equal (4vec-mask m1 (car x))
                     (4vec-mask m1 (car y)))
              (equal (4veclist-mask m (cdr x))
                     (4veclist-mask m (cdr y))))))