Function:
(defun sparseint$-leaves-mergeable-p (width lsbs msbs) (declare (xargs :guard (and (posp width) (integerp lsbs) (integerp msbs)))) (let ((__function__ 'sparseint$-leaves-mergeable-p)) (declare (ignorable __function__)) (b* ((msbs (lifix msbs)) (lsbs (lifix lsbs)) (width (lposfix width)) ((when (eql 0 width)) t) ((when (or (eql msbs 0) (eql msbs -1))) (b* (((when (eql (logbitp (1- width) lsbs) (logbitp 0 msbs))) t) ((when (< width (sparseint$-leaf-bitlimit))) t)) nil)) ((when (< (+ width (integer-length msbs)) (sparseint$-leaf-bitlimit))) t)) nil)))
Theorem:
(defthm sparseint$-leaves-mergeable-p-of-pos-fix-width (equal (sparseint$-leaves-mergeable-p (pos-fix width) lsbs msbs) (sparseint$-leaves-mergeable-p width lsbs msbs)))
Theorem:
(defthm sparseint$-leaves-mergeable-p-pos-equiv-congruence-on-width (implies (pos-equiv width width-equiv) (equal (sparseint$-leaves-mergeable-p width lsbs msbs) (sparseint$-leaves-mergeable-p width-equiv lsbs msbs))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-leaves-mergeable-p-of-ifix-lsbs (equal (sparseint$-leaves-mergeable-p width (ifix lsbs) msbs) (sparseint$-leaves-mergeable-p width lsbs msbs)))
Theorem:
(defthm sparseint$-leaves-mergeable-p-int-equiv-congruence-on-lsbs (implies (int-equiv lsbs lsbs-equiv) (equal (sparseint$-leaves-mergeable-p width lsbs msbs) (sparseint$-leaves-mergeable-p width lsbs-equiv msbs))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-leaves-mergeable-p-of-ifix-msbs (equal (sparseint$-leaves-mergeable-p width lsbs (ifix msbs)) (sparseint$-leaves-mergeable-p width lsbs msbs)))
Theorem:
(defthm sparseint$-leaves-mergeable-p-int-equiv-congruence-on-msbs (implies (int-equiv msbs msbs-equiv) (equal (sparseint$-leaves-mergeable-p width lsbs msbs) (sparseint$-leaves-mergeable-p width lsbs msbs-equiv))) :rule-classes :congruence)