(sparseint$-mergeable-leaves-p width lsbs msbs) → mergep
Function:
(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:
(defthm not-mergeable-leaves-when-lsbs-concat (b* ((?mergep (sparseint$-mergeable-leaves-p width lsbs msbs))) (implies (sparseint$-case lsbs :concat) (not mergep))))
Theorem:
(defthm not-mergeable-leaves-when-msbs-concat (b* ((?mergep (sparseint$-mergeable-leaves-p width lsbs msbs))) (implies (sparseint$-case msbs :concat) (not mergep))))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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)