		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-real-height

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

Definitions and Theorems

Function: sparseint$-real-height

(defun sparseint$-real-height (x)
  (declare (xargs :guard (sparseint$-p x)))
  (let ((__function__ 'sparseint$-real-height))
    (declare (ignorable __function__))
    (sparseint$-case
         x
         :leaf 0
         :concat (+ 1
                    (max (sparseint$-real-height x.lsbs)
                         (sparseint$-real-height x.msbs))))))

Theorem: natp-of-sparseint$-real-height

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

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

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

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

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