		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-height-correct-exec

Signature
(sparseint$-height-correct-exec x) → height-if-correct
Arguments: x — Guard (sparseint$-p x).
Returns: height-if-correct — Type (acl2::maybe-natp height-if-correct).

Definitions and Theorems

Function: sparseint$-height-correct-exec

(defun sparseint$-height-correct-exec (x)
 (declare (xargs :guard (sparseint$-p x)))
 (let ((__function__ 'sparseint$-height-correct-exec))
  (declare (ignorable __function__))
  (sparseint$-case
   x :leaf 0 :concat
   (b* ((lsb-height (sparseint$-height-correct-exec x.lsbs))
        ((unless lsb-height) nil)
        (msb-height (sparseint$-height-correct-exec x.msbs)))
    (and msb-height
         (cond (x.lsbs-taller (and (not x.msbs-taller)
                                   (eql lsb-height (+ 1 msb-height))
                                   (+ 1 lsb-height)))
               (x.msbs-taller (and (eql msb-height (+ 1 lsb-height))
                                   (+ 1 msb-height)))
               (t (and (eql msb-height lsb-height)
                       (+ 1 lsb-height)))))))))

Theorem: maybe-natp-of-sparseint$-height-correct-exec

(defthm maybe-natp-of-sparseint$-height-correct-exec
  (b* ((height-if-correct (sparseint$-height-correct-exec x)))
    (acl2::maybe-natp height-if-correct))
  :rule-classes :type-prescription)

Theorem: height-if-correct-of-sparseint$-height-correct-exec

(defthm height-if-correct-of-sparseint$-height-correct-exec
  (b* ((?height-if-correct (sparseint$-height-correct-exec x)))
    (implies height-if-correct
             (equal height-if-correct
                    (sparseint$-real-height x)))))

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

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

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

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