		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Uint-ne

Non-equality comparison of unsigned integer values.

Signature
(uint-ne left right) → result
Arguments: left — Guard (uintp left).; right — Guard (uintp right).
Returns: result — Type (boolp result).

Definitions and Theorems

Function: uint-ne

(defun uint-ne (left right)
  (declare (xargs :guard (and (uintp left) (uintp right))))
  (declare (xargs :guard (= (uint->size left)
                            (uint->size right))))
  (b* ((x (uint->value left))
       (y (uint->value right)))
    (bool (not (equal x y)))))

Theorem: boolp-of-uint-ne

(defthm boolp-of-uint-ne
  (b* ((result (uint-ne left right)))
    (boolp result))
  :rule-classes :rewrite)

Theorem: uint-ne-of-uint-fix-left

(defthm uint-ne-of-uint-fix-left
  (equal (uint-ne (uint-fix left) right)
         (uint-ne left right)))

Theorem: uint-ne-uint-equiv-congruence-on-left

(defthm uint-ne-uint-equiv-congruence-on-left
  (implies (uint-equiv left left-equiv)
           (equal (uint-ne left right)
                  (uint-ne left-equiv right)))
  :rule-classes :congruence)

Theorem: uint-ne-of-uint-fix-right

(defthm uint-ne-of-uint-fix-right
  (equal (uint-ne left (uint-fix right))
         (uint-ne left right)))

Theorem: uint-ne-uint-equiv-congruence-on-right

(defthm uint-ne-uint-equiv-congruence-on-right
  (implies (uint-equiv right right-equiv)
           (equal (uint-ne left right)
                  (uint-ne left right-equiv)))
  :rule-classes :congruence)