		Search-engine friendly clone of the ACL2 documentation.

Logops-bit-functions

B-eqv

Equivalence (a.k.a. if and only if, xnor) for bitps.

Signature
(b-eqv i j) → bit
Arguments: i — Guard (bitp i).; j — Guard (bitp j).
Returns: bit — Type (bitp bit).

Definitions and Theorems

Function: b-eqv$inline

(defun b-eqv$inline (i j)
  (declare (xargs :guard (and (bitp i) (bitp j))))
  (let ((__function__ 'b-eqv))
    (declare (ignorable __function__))
    (mbe :logic
         (if (zbp i)
             (if (zbp j) 1 0)
           (if (zbp j) 0 1))
         :exec (the (unsigned-byte 1)
                    (logxor (the (unsigned-byte 1)
                                 (logxor (the (unsigned-byte 1) i)
                                         (the (unsigned-byte 1) j)))
                            1)))))

Theorem: bitp-of-b-eqv

(defthm bitp-of-b-eqv
  (b* ((bit (b-eqv$inline i j)))
    (bitp bit))
  :rule-classes :type-prescription)