		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Uint-not

Bitwise negation of unsigned integer values.

Signature
(uint-not operand) → result
Arguments: operand — Guard (uintp operand).
Returns: result — Type (uintp result).

Definitions and Theorems

Function: uint-not

(defun uint-not (operand)
  (declare (xargs :guard (uintp operand)))
  (b* ((size (uint->size operand))
       (x (uint->value operand)))
    (make-uint :size (uint->size operand)
               :value (loghead size (lognot x)))))

Theorem: uintp-of-uint-not

(defthm uintp-of-uint-not
  (b* ((result (uint-not operand)))
    (uintp result))
  :rule-classes :rewrite)

Theorem: uint-not-of-uint-fix-operand

(defthm uint-not-of-uint-fix-operand
  (equal (uint-not (uint-fix operand))
         (uint-not operand)))

Theorem: uint-not-uint-equiv-congruence-on-operand

(defthm uint-not-uint-equiv-congruence-on-operand
  (implies (uint-equiv operand operand-equiv)
           (equal (uint-not operand)
                  (uint-not operand-equiv)))
  :rule-classes :congruence)