		Search-engine friendly clone of the ACL2 documentation.

Logops-bit-functions

B-and

Conjunction for bitps.

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

Definitions and Theorems

Function: b-and$inline

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

Theorem: bitp-of-b-and

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