		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-height

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

Definitions and Theorems

Function: sparseint$-height

(defun sparseint$-height (x)
 (declare (xargs :guard (sparseint$-p x)))
 (declare (xargs :guard (sparseint$-height-correctp x)))
 (let ((__function__ 'sparseint$-height))
  (declare (ignorable __function__))
  (sparseint$-case
   x
   :leaf 0
   :concat
   (mbe :logic (+ 1
                  (max (sparseint$-height x.lsbs)
                       (sparseint$-height x.msbs)))
        :exec (cond (x.lsbs-taller (+ 2 (sparseint$-height x.msbs)))
                    (x.msbs-taller (+ 2 (sparseint$-height x.lsbs)))
                    (t (+ 1 (sparseint$-height x.lsbs))))))))

Theorem: natp-of-sparseint$-height

(defthm natp-of-sparseint$-height
  (b* ((height (sparseint$-height x)))
    (natp height))
  :rule-classes :type-prescription)

Theorem: sparseint$-real-height-equals-sparseint$-height

(defthm sparseint$-real-height-equals-sparseint$-height
  (b* ((?height (sparseint$-height x)))
    (equal (sparseint$-real-height x)
           height)))

Theorem: sparseint$-height-equal-0

(defthm sparseint$-height-equal-0
  (b* ((?height (sparseint$-height x)))
    (equal (equal height 0)
           (sparseint$-case x :leaf))))

Theorem: sparseint$-height-when-concat

(defthm sparseint$-height-when-concat
  (implies (sparseint$-case x :concat)
           (equal (sparseint$-height x)
                  (b* (((sparseint$-concat x)))
                    (+ 1
                       (max (sparseint$-height x.lsbs)
                            (sparseint$-height x.msbs)))))))

Theorem: sparseint$-height-of-concat

(defthm sparseint$-height-of-concat
  (equal (sparseint$-height
              (make-sparseint$-concat :width width
                                      :lsbs lsbs
                                      :msbs msbs
                                      :lsbs-taller lsbs-taller
                                      :msbs-taller msbs-taller))
         (+ 1
            (max (sparseint$-height lsbs)
                 (sparseint$-height msbs)))))

Theorem: sparseint$-height-when-leaf

(defthm sparseint$-height-when-leaf
  (implies (sparseint$-case x :leaf)
           (equal (sparseint$-height x) 0))
  :rule-classes (:rewrite :forward-chaining))

Theorem: sparseint$-height-posp-when-concat

(defthm sparseint$-height-posp-when-concat
  (b* ((?height (sparseint$-height x)))
    (iff (posp height)
         (equal (sparseint$-kind x) :concat)))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((sparseint$-height x))
        :corollary (implies (posp (sparseint$-height x))
                            (equal (sparseint$-kind x) :concat)))
   (:forward-chaining
        :trigger-terms ((equal (sparseint$-kind x) :concat))
        :corollary (implies (equal (sparseint$-kind x) :concat)
                            (posp (sparseint$-height x))))))

Theorem: sparseint$-height-gt-0-implies-concat

(defthm sparseint$-height-gt-0-implies-concat
  (b* ((?height (sparseint$-height x)))
    (implies (< 0 height)
             (equal (sparseint$-kind x) :concat)))
  :rule-classes
  ((:forward-chaining :trigger-terms ((sparseint$-height x)))))

Theorem: sparseint$-height-of-lsbs-upper-bound

(defthm sparseint$-height-of-lsbs-upper-bound
  (implies (sparseint$-case x :concat)
           (<= (sparseint$-height (sparseint$-concat->lsbs x))
               (+ -1 (sparseint$-height x))))
  :rule-classes :linear)

Theorem: sparseint$-height-of-msbs-upper-bound

(defthm sparseint$-height-of-msbs-upper-bound
  (implies (sparseint$-case x :concat)
           (<= (sparseint$-height (sparseint$-concat->msbs x))
               (+ -1 (sparseint$-height x))))
  :rule-classes :linear)

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

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

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

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