Function:
(defun sparseint$-binary-bittest-int-width (op width offset x y) (declare (type (unsigned-byte 4) op)) (declare (xargs :guard (and (integerp op) (posp width) (natp offset) (sparseint$-p x) (integerp y)))) (let ((__function__ 'sparseint$-binary-bittest-int-width)) (declare (ignorable __function__)) (b* ((width (lposfix width)) (offset (lnfix offset)) (y (lifix y)) ((when (or (eql y 0) (eql y -1))) (b* ((cofactor (binary-bitop-cofactor2 op (- y)))) (sparseint$-unary-bittest-width cofactor width offset x)))) (sparseint$-case x :leaf (binary-bittest op (bignum-logext width (logtail offset x.val)) (bignum-logext width y)) :concat (b* (((when (<= x.width offset)) (sparseint$-binary-bittest-int-width op width (- offset x.width) x.msbs y)) (width1 (- x.width offset)) ((when (<= width width1)) (sparseint$-binary-bittest-int-width op width offset x.lsbs y))) (or (sparseint$-binary-bittest-int-width op width1 offset x.lsbs (bignum-logext width1 y)) (sparseint$-binary-bittest-int-width op (- width width1) 0 x.msbs (logtail width1 y))))))))
Theorem:
(defthm booleanp-of-sparseint$-binary-bittest-int-width (b* ((test (sparseint$-binary-bittest-int-width op width offset x y))) (booleanp test)) :rule-classes :type-prescription)
Theorem:
(defthm sparseint$-val-of-sparseint$-binary-bittest-int-width (b* ((?test (sparseint$-binary-bittest-int-width op width offset x y))) (equal test (binary-bittest op (logext width (logtail offset (sparseint$-val x))) (logext width y)))))
Theorem:
(defthm sparseint$-binary-bittest-int-width-of-ifix-op (equal (sparseint$-binary-bittest-int-width (ifix op) width offset x y) (sparseint$-binary-bittest-int-width op width offset x y)))
Theorem:
(defthm sparseint$-binary-bittest-int-width-int-equiv-congruence-on-op (implies (int-equiv op op-equiv) (equal (sparseint$-binary-bittest-int-width op width offset x y) (sparseint$-binary-bittest-int-width op-equiv width offset x y))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-binary-bittest-int-width-of-pos-fix-width (equal (sparseint$-binary-bittest-int-width op (pos-fix width) offset x y) (sparseint$-binary-bittest-int-width op width offset x y)))
Theorem:
(defthm sparseint$-binary-bittest-int-width-pos-equiv-congruence-on-width (implies (pos-equiv width width-equiv) (equal (sparseint$-binary-bittest-int-width op width offset x y) (sparseint$-binary-bittest-int-width op width-equiv offset x y))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-binary-bittest-int-width-of-nfix-offset (equal (sparseint$-binary-bittest-int-width op width (nfix offset) x y) (sparseint$-binary-bittest-int-width op width offset x y)))
Theorem:
(defthm sparseint$-binary-bittest-int-width-nat-equiv-congruence-on-offset (implies (nat-equiv offset offset-equiv) (equal (sparseint$-binary-bittest-int-width op width offset x y) (sparseint$-binary-bittest-int-width op width offset-equiv x y))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-binary-bittest-int-width-of-sparseint$-fix-x (equal (sparseint$-binary-bittest-int-width op width offset (sparseint$-fix x) y) (sparseint$-binary-bittest-int-width op width offset x y)))
Theorem:
(defthm sparseint$-binary-bittest-int-width-sparseint$-equiv-congruence-on-x (implies (sparseint$-equiv x x-equiv) (equal (sparseint$-binary-bittest-int-width op width offset x y) (sparseint$-binary-bittest-int-width op width offset x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-binary-bittest-int-width-of-ifix-y (equal (sparseint$-binary-bittest-int-width op width offset x (ifix y)) (sparseint$-binary-bittest-int-width op width offset x y)))
Theorem:
(defthm sparseint$-binary-bittest-int-width-int-equiv-congruence-on-y (implies (int-equiv y y-equiv) (equal (sparseint$-binary-bittest-int-width op width offset x y) (sparseint$-binary-bittest-int-width op width offset x y-equiv))) :rule-classes :congruence)