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