		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-unary-minus

Signature
(sparseint$-unary-minus x) → minus
Arguments: x — Guard (sparseint$-p x).
Returns: minus — Type (sparseint$-p minus).

Definitions and Theorems

Function: sparseint$-unary-minus

(defun sparseint$-unary-minus (x)
  (declare (xargs :guard (sparseint$-p x)))
  (declare (xargs :guard (sparseint$-height-correctp x)))
  (let ((__function__ 'sparseint$-unary-minus))
    (declare (ignorable __function__))
    (b* ((height (sparseint$-height x))
         (neg (sparseint$-bitnot x))
         ((mv minus ?height)
          (sparseint$-plus-int 0 neg height 0 1)))
      minus)))

Theorem: sparseint$-p-of-sparseint$-unary-minus

(defthm sparseint$-p-of-sparseint$-unary-minus
  (b* ((minus (sparseint$-unary-minus x)))
    (sparseint$-p minus))
  :rule-classes :rewrite)

Theorem: sparseint$-height-correctp-of-sparseint$-unary-minus

(defthm sparseint$-height-correctp-of-sparseint$-unary-minus
  (b* ((?minus (sparseint$-unary-minus x)))
    (implies (sparseint$-height-correctp x)
             (sparseint$-height-correctp minus))))

Theorem: sparseint$-val-of-sparseint$-unary-minus

(defthm sparseint$-val-of-sparseint$-unary-minus
  (b* ((?minus (sparseint$-unary-minus x)))
    (equal (sparseint$-val minus)
           (- (sparseint$-val x)))))

Theorem: sparseint$-unary-minus-of-sparseint$-fix-x

(defthm sparseint$-unary-minus-of-sparseint$-fix-x
  (equal (sparseint$-unary-minus (sparseint$-fix x))
         (sparseint$-unary-minus x)))

Theorem: sparseint$-unary-minus-sparseint$-equiv-congruence-on-x

(defthm sparseint$-unary-minus-sparseint$-equiv-congruence-on-x
  (implies (sparseint$-equiv x x-equiv)
           (equal (sparseint$-unary-minus x)
                  (sparseint$-unary-minus x-equiv)))
  :rule-classes :congruence)