		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-bitnot

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

Definitions and Theorems

Function: sparseint$-bitnot

(defun sparseint$-bitnot (x)
 (declare (xargs :guard (sparseint$-p x)))
 (let ((__function__ 'sparseint$-bitnot))
  (declare (ignorable __function__))
  (sparseint$-case
      x
      :leaf (sparseint$-leaf (lognot x.val))
      :concat
      (change-sparseint$-concat x
                                :lsbs (sparseint$-bitnot x.lsbs)
                                :msbs (sparseint$-bitnot x.msbs)))))

Theorem: sparseint$-p-of-sparseint$-bitnot

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

Theorem: sparseint$-height-of-sparseint$-bitnot

(defthm sparseint$-height-of-sparseint$-bitnot
  (b* ((?bitnot (sparseint$-bitnot x)))
    (equal (sparseint$-height bitnot)
           (sparseint$-height x))))

Theorem: sparseint$-height-correct-of-sparseint$-bitnot

(defthm sparseint$-height-correct-of-sparseint$-bitnot
  (b* ((?bitnot (sparseint$-bitnot x)))
    (implies (sparseint$-height-correctp x)
             (sparseint$-height-correctp bitnot))))

Theorem: sparseint$-val-of-sparseint$-bitnot

(defthm sparseint$-val-of-sparseint$-bitnot
  (b* ((?bitnot (sparseint$-bitnot x)))
    (equal (sparseint$-val bitnot)
           (lognot (sparseint$-val x)))))

Theorem: sparseint$-bitnot-of-sparseint$-fix-x

(defthm sparseint$-bitnot-of-sparseint$-fix-x
  (equal (sparseint$-bitnot (sparseint$-fix x))
         (sparseint$-bitnot x)))

Theorem: sparseint$-bitnot-sparseint$-equiv-congruence-on-x

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