(sparseint$-truncate-height width x height) → (mv new-x new-height)
Function:
(defun sparseint$-truncate-height (width x height) (declare (xargs :guard (and (posp width) (sparseint$-p x)))) (declare (xargs :guard (and (sparseint$-height-correctp x) (equal height (sparseint$-height x))))) (let ((__function__ 'sparseint$-truncate-height)) (declare (ignorable __function__)) (b* ((height (mbe :logic (sparseint$-height x) :exec height))) (sparseint$-case x :leaf (mv (sparseint$-fix x) height) :concat (if (< x.width (lposfix width)) (mv (sparseint$-fix x) height) (sparseint$-truncate-height width x.lsbs (- height (if x.msbs-taller 2 1))))))))
Theorem:
(defthm return-type-of-sparseint$-truncate-height.new-x (b* (((mv ?new-x ?new-height) (sparseint$-truncate-height width x height))) (equal new-x (sparseint$-truncate width x))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-sparseint$-truncate-height.new-height (b* (((mv ?new-x ?new-height) (sparseint$-truncate-height width x height))) (equal new-height (sparseint$-height (sparseint$-truncate width x)))) :rule-classes :rewrite)
Theorem:
(defthm sparseint$-truncate-height-of-pos-fix-width (equal (sparseint$-truncate-height (pos-fix width) x height) (sparseint$-truncate-height width x height)))
Theorem:
(defthm sparseint$-truncate-height-pos-equiv-congruence-on-width (implies (pos-equiv width width-equiv) (equal (sparseint$-truncate-height width x height) (sparseint$-truncate-height width-equiv x height))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-truncate-height-of-sparseint$-fix-x (equal (sparseint$-truncate-height width (sparseint$-fix x) height) (sparseint$-truncate-height width x height)))
Theorem:
(defthm sparseint$-truncate-height-sparseint$-equiv-congruence-on-x (implies (sparseint$-equiv x x-equiv) (equal (sparseint$-truncate-height width x height) (sparseint$-truncate-height width x-equiv height))) :rule-classes :congruence)