		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Uint-minus

Arithmetic negation of unsigned integer values.

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

Definitions and Theorems

Function: uint-minus

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

Theorem: uintp-of-uint-minus

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

Theorem: uint-minus-of-uint-fix-operand

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

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

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