(sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height) → (mv concat height)
Function:
(defun sparseint$-finalize-concat (width lsbs lsbs.height msbs msbs.height) (declare (xargs :guard (and (posp width) (sparseint$-p lsbs) (sparseint$-p msbs)))) (declare (xargs :guard (and (sparseint$-height-correctp lsbs) (equal lsbs.height (sparseint$-height lsbs)) (sparseint$-height-correctp msbs) (equal msbs.height (sparseint$-height msbs)) (within-1 lsbs.height msbs.height)))) (let ((__function__ 'sparseint$-finalize-concat)) (declare (ignorable __function__)) (b* ((lsbs.height (mbe :logic (sparseint$-height lsbs) :exec lsbs.height)) (msbs.height (mbe :logic (sparseint$-height msbs) :exec msbs.height)) ((unless (and (eql lsbs.height 0) (eql msbs.height 0))) (mv (make-sparseint$-concat :width width :lsbs lsbs :msbs msbs :lsbs-taller (> lsbs.height msbs.height) :msbs-taller (> msbs.height lsbs.height)) (+ 1 (max lsbs.height msbs.height)))) ((sparseint$-leaf lsbs)) ((sparseint$-leaf msbs)) (width (lposfix width)) ((when (eql 0 width)) (mv (sparseint$-fix msbs) 0)) ((when (or (eql msbs.val 0) (eql msbs.val -1))) (b* (((when (eql (logbitp (1- width) lsbs.val) (logbitp 0 msbs.val))) (if (< (integer-length lsbs.val) width) (mv (sparseint$-fix lsbs) 0) (mv (make-sparseint$-leaf :val (bignum-logext width lsbs.val)) 0))) ((when (< width (sparseint$-leaf-bitlimit))) (mv (make-sparseint$-leaf :val (logapp width lsbs.val msbs.val)) 0))) (mv (make-sparseint$-concat :width width :lsbs lsbs :msbs msbs) 1))) ((when (< (+ width (integer-length msbs.val)) (sparseint$-leaf-bitlimit))) (mv (make-sparseint$-leaf :val (logapp width lsbs.val msbs.val)) 0))) (mv (make-sparseint$-concat :width width :lsbs lsbs :msbs msbs) 1))))
Theorem:
(defthm sparseint$-p-of-sparseint$-finalize-concat.concat (b* (((mv ?concat ?height) (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height))) (sparseint$-p concat)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-sparseint$-finalize-concat.height (b* (((mv ?concat ?height) (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height))) (equal height (sparseint$-height concat))) :rule-classes :rewrite)
Theorem:
(defthm sparseint$-finalize-concat-height-correctp (b* (((mv ?concat ?height) (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height))) (implies (and (sparseint$-height-correctp lsbs) (sparseint$-height-correctp msbs) (within-1 (sparseint$-height lsbs) (sparseint$-height msbs))) (sparseint$-height-correctp concat))))
Theorem:
(defthm sparseint$-finalize-concat-correct (b* (((mv ?concat ?height) (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height))) (equal (sparseint$-val concat) (logapp (pos-fix width) (sparseint$-val lsbs) (sparseint$-val msbs)))))
Theorem:
(defthm sparseint$-finalize-concat-height-possibilities (b* (((mv ?concat ?height) (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height))) (equal (sparseint$-height concat) (+ (if (sparseint$-mergeable-leaves-p width lsbs msbs) 0 1) (max (sparseint$-height lsbs) (sparseint$-height msbs))))))
Theorem:
(defthm sparseint$-finalize-concat-not-leaf-unless-merged (b* (((mv ?concat ?height) (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height))) (implies (not (sparseint$-mergeable-leaves-p width lsbs msbs)) (equal (sparseint$-kind concat) :concat))))
Theorem:
(defthm sparseint$-finalize-concat-leaf-when-merged (b* (((mv ?concat ?height) (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height))) (implies (sparseint$-mergeable-leaves-p width lsbs msbs) (equal (sparseint$-kind concat) :leaf))))
Theorem:
(defthm sparseint$-finalize-concat-of-pos-fix-width (equal (sparseint$-finalize-concat (pos-fix width) lsbs lsbs.height msbs msbs.height) (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height)))
Theorem:
(defthm sparseint$-finalize-concat-pos-equiv-congruence-on-width (implies (pos-equiv width width-equiv) (equal (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height) (sparseint$-finalize-concat width-equiv lsbs lsbs.height msbs msbs.height))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-finalize-concat-of-sparseint$-fix-lsbs (equal (sparseint$-finalize-concat width (sparseint$-fix lsbs) lsbs.height msbs msbs.height) (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height)))
Theorem:
(defthm sparseint$-finalize-concat-sparseint$-equiv-congruence-on-lsbs (implies (sparseint$-equiv lsbs lsbs-equiv) (equal (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height) (sparseint$-finalize-concat width lsbs-equiv lsbs.height msbs msbs.height))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-finalize-concat-of-sparseint$-fix-msbs (equal (sparseint$-finalize-concat width lsbs lsbs.height (sparseint$-fix msbs) msbs.height) (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height)))
Theorem:
(defthm sparseint$-finalize-concat-sparseint$-equiv-congruence-on-msbs (implies (sparseint$-equiv msbs msbs-equiv) (equal (sparseint$-finalize-concat width lsbs lsbs.height msbs msbs.height) (sparseint$-finalize-concat width lsbs lsbs.height msbs-equiv msbs.height))) :rule-classes :congruence)