		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-leaves-mergeable-p

Signature
(sparseint$-leaves-mergeable-p width lsbs msbs) → mergep
Arguments: width — Guard (posp width).; lsbs — Guard (integerp lsbs).; msbs — Guard (integerp msbs).

Definitions and Theorems

Function: sparseint$-leaves-mergeable-p

(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: sparseint$-leaves-mergeable-p-of-pos-fix-width

(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: sparseint$-leaves-mergeable-p-pos-equiv-congruence-on-width

(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: sparseint$-leaves-mergeable-p-of-ifix-lsbs

(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: sparseint$-leaves-mergeable-p-int-equiv-congruence-on-lsbs

(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: sparseint$-leaves-mergeable-p-of-ifix-msbs

(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: sparseint$-leaves-mergeable-p-int-equiv-congruence-on-msbs

(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)