		Search-engine friendly clone of the ACL2 documentation.

S4vecs

S4vec-resand

Signature
(s4vec-resand x y) → resand
Arguments: x — Guard (s4vec-p x).; y — Guard (s4vec-p y).
Returns: resand — Type (s4vec-p resand).

Definitions and Theorems

Function: s4vec-resand

(defun s4vec-resand (x y)
 (declare (xargs :guard (and (s4vec-p x) (s4vec-p y))))
 (let ((__function__ 's4vec-resand))
  (declare (ignorable __function__))
  (b* (((s4vec x)) ((s4vec y)))
   (s4vec (sparseint-bitand
               (sparseint-bitor x.upper x.lower)
               (sparseint-bitand (sparseint-bitor y.upper y.lower)
                                 (sparseint-bitor x.upper y.upper)))
          (sparseint-bitand x.lower y.lower)))))

Theorem: s4vec-p-of-s4vec-resand

(defthm s4vec-p-of-s4vec-resand
  (b* ((resand (s4vec-resand x y)))
    (s4vec-p resand))
  :rule-classes :rewrite)

Theorem: s4vec-resand-correct

(defthm s4vec-resand-correct
  (b* ((?resand (s4vec-resand x y)))
    (equal (s4vec->4vec resand)
           (4vec-resand (s4vec->4vec x)
                        (s4vec->4vec y)))))

Theorem: s4vec-resand-of-s4vec-fix-x

(defthm s4vec-resand-of-s4vec-fix-x
  (equal (s4vec-resand (s4vec-fix x) y)
         (s4vec-resand x y)))

Theorem: s4vec-resand-s4vec-equiv-congruence-on-x

(defthm s4vec-resand-s4vec-equiv-congruence-on-x
  (implies (s4vec-equiv x x-equiv)
           (equal (s4vec-resand x y)
                  (s4vec-resand x-equiv y)))
  :rule-classes :congruence)

Theorem: s4vec-resand-of-s4vec-fix-y

(defthm s4vec-resand-of-s4vec-fix-y
  (equal (s4vec-resand x (s4vec-fix y))
         (s4vec-resand x y)))

Theorem: s4vec-resand-s4vec-equiv-congruence-on-y

(defthm s4vec-resand-s4vec-equiv-congruence-on-y
  (implies (s4vec-equiv y y-equiv)
           (equal (s4vec-resand x y)
                  (s4vec-resand x y-equiv)))
  :rule-classes :congruence)