		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-height-correctp

Signature
(sparseint$-height-correctp x) → correctp
Arguments: x — Guard (sparseint$-p x).

Definitions and Theorems

Function: sparseint$-height-correctp

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

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

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

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

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