		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-mergeable-leaves-p

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

Definitions and Theorems

Function: sparseint$-mergeable-leaves-p

(defun sparseint$-mergeable-leaves-p (width lsbs msbs)
 (declare (xargs :guard (and (posp width)
                             (sparseint$-p lsbs)
                             (sparseint$-p msbs))))
 (let ((__function__ 'sparseint$-mergeable-leaves-p))
  (declare (ignorable __function__))
  (and
    (sparseint$-case lsbs :leaf)
    (sparseint$-case msbs :leaf)
    (sparseint$-leaves-mergeable-p width (sparseint$-leaf->val lsbs)
                                   (sparseint$-leaf->val msbs)))))

Theorem: not-mergeable-leaves-when-lsbs-concat

(defthm not-mergeable-leaves-when-lsbs-concat
  (b* ((?mergep (sparseint$-mergeable-leaves-p width lsbs msbs)))
    (implies (sparseint$-case lsbs :concat)
             (not mergep))))

Theorem: not-mergeable-leaves-when-msbs-concat

(defthm not-mergeable-leaves-when-msbs-concat
  (b* ((?mergep (sparseint$-mergeable-leaves-p width lsbs msbs)))
    (implies (sparseint$-case msbs :concat)
             (not mergep))))

Theorem: sparseint$-mergeable-leaves-p-of-pos-fix-width

(defthm sparseint$-mergeable-leaves-p-of-pos-fix-width
  (equal (sparseint$-mergeable-leaves-p (pos-fix width)
                                        lsbs msbs)
         (sparseint$-mergeable-leaves-p width lsbs msbs)))

Theorem: sparseint$-mergeable-leaves-p-pos-equiv-congruence-on-width

(defthm sparseint$-mergeable-leaves-p-pos-equiv-congruence-on-width
 (implies
      (pos-equiv width width-equiv)
      (equal (sparseint$-mergeable-leaves-p width lsbs msbs)
             (sparseint$-mergeable-leaves-p width-equiv lsbs msbs)))
 :rule-classes :congruence)

Theorem: sparseint$-mergeable-leaves-p-of-sparseint$-fix-lsbs

(defthm sparseint$-mergeable-leaves-p-of-sparseint$-fix-lsbs
  (equal (sparseint$-mergeable-leaves-p width (sparseint$-fix lsbs)
                                        msbs)
         (sparseint$-mergeable-leaves-p width lsbs msbs)))

Theorem: sparseint$-mergeable-leaves-p-sparseint$-equiv-congruence-on-lsbs

(defthm
  sparseint$-mergeable-leaves-p-sparseint$-equiv-congruence-on-lsbs
 (implies
      (sparseint$-equiv lsbs lsbs-equiv)
      (equal (sparseint$-mergeable-leaves-p width lsbs msbs)
             (sparseint$-mergeable-leaves-p width lsbs-equiv msbs)))
 :rule-classes :congruence)

Theorem: sparseint$-mergeable-leaves-p-of-sparseint$-fix-msbs

(defthm sparseint$-mergeable-leaves-p-of-sparseint$-fix-msbs
 (equal
    (sparseint$-mergeable-leaves-p width lsbs (sparseint$-fix msbs))
    (sparseint$-mergeable-leaves-p width lsbs msbs)))

Theorem: sparseint$-mergeable-leaves-p-sparseint$-equiv-congruence-on-msbs

(defthm
  sparseint$-mergeable-leaves-p-sparseint$-equiv-congruence-on-msbs
 (implies
      (sparseint$-equiv msbs msbs-equiv)
      (equal (sparseint$-mergeable-leaves-p width lsbs msbs)
             (sparseint$-mergeable-leaves-p width lsbs msbs-equiv)))
 :rule-classes :congruence)