		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-===

Unsafe, Verilog-style ``case 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).

Warning: this is a bad operator that breaks the 4vec-<<= lattice monotonicity property. It is similar to 4vec-== but, instead of treating X or Z bits as unknown, allows them to be directly compared with one another.

We return, following the boolean-convention,

True (all 1s) when the inputs are identical, or
False (all 0s) otherwise.

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__))
    (2vec (bool->vec (4vec-equiv x 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-4vec-fix-x

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

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

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

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

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

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

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