		Search-engine friendly clone of the ACL2 documentation.

4vmask

4vmasklist-subsumes

(4vmasklist-subsumes x y) checks whether the masks in the list x all subsume the corresponding masks in y, in the sense of 4vmask-subsumes.

Signature
(4vmasklist-subsumes x y) → *
Arguments: x — Guard (4vmasklist-p x).; y — Guard (4vmasklist-p y).

Definitions and Theorems

Function: 4vmasklist-subsumes

(defun 4vmasklist-subsumes (x y)
  (declare (xargs :guard (and (4vmasklist-p x)
                              (4vmasklist-p y))))
  (let ((__function__ '4vmasklist-subsumes))
    (declare (ignorable __function__))
    (if (and (atom x) (atom y))
        t
      (and (4vmask-subsumes (if (consp x) (car x) -1)
                            (if (consp y) (car y) -1))
           (4vmasklist-subsumes (cdr x)
                                (cdr y))))))

Theorem: 4vmasklist-subsumes-of-4vmasklist-fix-x

(defthm 4vmasklist-subsumes-of-4vmasklist-fix-x
  (equal (4vmasklist-subsumes (4vmasklist-fix x)
                              y)
         (4vmasklist-subsumes x y)))

Theorem: 4vmasklist-subsumes-4vmasklist-equiv-congruence-on-x

(defthm 4vmasklist-subsumes-4vmasklist-equiv-congruence-on-x
  (implies (4vmasklist-equiv x x-equiv)
           (equal (4vmasklist-subsumes x y)
                  (4vmasklist-subsumes x-equiv y)))
  :rule-classes :congruence)

Theorem: 4vmasklist-subsumes-of-4vmasklist-fix-y

(defthm 4vmasklist-subsumes-of-4vmasklist-fix-y
  (equal (4vmasklist-subsumes x (4vmasklist-fix y))
         (4vmasklist-subsumes x y)))

Theorem: 4vmasklist-subsumes-4vmasklist-equiv-congruence-on-y

(defthm 4vmasklist-subsumes-4vmasklist-equiv-congruence-on-y
  (implies (4vmasklist-equiv y y-equiv)
           (equal (4vmasklist-subsumes x y)
                  (4vmasklist-subsumes x y-equiv)))
  :rule-classes :congruence)

Theorem: 4vmasklist-subsumes-implies-masks-equal

(defthm 4vmasklist-subsumes-implies-masks-equal
  (implies (and (4vmasklist-subsumes m1 m2)
                (equal (4veclist-mask m1 x)
                       (4veclist-mask m1 y)))
           (equal (equal (4veclist-mask m2 x)
                         (4veclist-mask m2 y))
                  t)))

Theorem: 4vmasklist-subsumes-self

(defthm 4vmasklist-subsumes-self
  (4vmasklist-subsumes x x))