		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-==

Bitwise equality of 4vecs.

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

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 and Z values as unknowns, i.e., whether or not an X/Z bit is equal to anything else, including another X/Z bit, is always unknown.

Definitions and Theorems

Function: 4vec-==

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

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

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

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

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

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

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

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

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

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

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