(sparseint$-height-correct-exec x) → height-if-correct
Function:
(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:
(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:
(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:
(defthm sparseint$-height-correct-exec-of-sparseint$-fix-x (equal (sparseint$-height-correct-exec (sparseint$-fix x)) (sparseint$-height-correct-exec x)))
Theorem:
(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)