		Search-engine friendly clone of the ACL2 documentation.

3vec-operations

3vec-==

Bitwise equality of 3vecs.

Signature
(3vec-== x y) → equal
Arguments: x — Guard (4vec-p x).; y — Guard (4vec-p y).
Returns: equal — Type (4vec-p equal).

Assuming that the inputs have no Z bits, we return, following the boolean-convention:

True (all 1s) when the inputs are purely Boolean and are equal, or
False (all 0s) if any bit is 0 in one input and is 1 in another, or
All Xes otherwise

This properly treats X as an unknown, i.e., whether or not an X bit is equal to anything else, including another X bit, is always unknown.

Definitions and Theorems

Function: 3vec-==

(defun 3vec-== (x y)
  (declare (xargs :guard (and (4vec-p x) (4vec-p y))))
  (let ((__function__ '3vec-==))
    (declare (ignorable __function__))
    (3vec-reduction-and (3vec-bitnot (3vec-bitxor x y)))))

Theorem: 4vec-p-of-3vec-==

(defthm 4vec-p-of-3vec-==
  (b* ((equal (3vec-== x y)))
    (4vec-p equal))
  :rule-classes :rewrite)

Theorem: 3vec-==-of-4vec-fix-x

(defthm 3vec-==-of-4vec-fix-x
  (equal (3vec-== (4vec-fix x) y)
         (3vec-== x y)))

Theorem: 3vec-==-4vec-equiv-congruence-on-x

(defthm 3vec-==-4vec-equiv-congruence-on-x
  (implies (4vec-equiv x x-equiv)
           (equal (3vec-== x y)
                  (3vec-== x-equiv y)))
  :rule-classes :congruence)

Theorem: 3vec-==-of-4vec-fix-y

(defthm 3vec-==-of-4vec-fix-y
  (equal (3vec-== x (4vec-fix y))
         (3vec-== x y)))

Theorem: 3vec-==-4vec-equiv-congruence-on-y

(defthm 3vec-==-4vec-equiv-congruence-on-y
  (implies (4vec-equiv y y-equiv)
           (equal (3vec-== x y)
                  (3vec-== x y-equiv)))
  :rule-classes :congruence)