		Search-engine friendly clone of the ACL2 documentation.

Logops-bit-functions

B-not

Negation for bitps.

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

Definitions and Theorems

Function: b-not$inline

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

Theorem: bitp-of-b-not

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