		Search-engine friendly clone of the ACL2 documentation.

Logops-bit-functions

B-orc1

Inclusive or of bitps, complementing the first.

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

Definitions and Theorems

Function: b-orc1$inline

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

Theorem: bitp-of-b-orc1

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