(sparseint$-unary-bittest-width op width offset x) → test
Function:
(defun sparseint$-unary-bittest-width (op width offset x) (declare (type (unsigned-byte 2) op)) (declare (xargs :guard (and (integerp op) (posp width) (natp offset) (sparseint$-p x)))) (let ((__function__ 'sparseint$-unary-bittest-width)) (declare (ignorable __function__)) (b* ((op (mbe :logic (loghead 2 op) :exec op))) (case op (0 nil) (1 (not (sparseint$-equal-int-width width offset x -1))) (2 (not (sparseint$-equal-int-width width offset x 0))) (t t)))))
Theorem:
(defthm booleanp-of-sparseint$-unary-bittest-width (b* ((test (sparseint$-unary-bittest-width op width offset x))) (booleanp test)) :rule-classes :type-prescription)
Theorem:
(defthm sparseint$-unary-bittest-width-correct (b* ((?test (sparseint$-unary-bittest-width op width offset x))) (equal test (not (equal (unary-bitop op (logext width (logtail offset (sparseint$-val x)))) 0)))))
Theorem:
(defthm sparseint$-unary-bittest-width-of-ifix-op (equal (sparseint$-unary-bittest-width (ifix op) width offset x) (sparseint$-unary-bittest-width op width offset x)))
Theorem:
(defthm sparseint$-unary-bittest-width-int-equiv-congruence-on-op (implies (int-equiv op op-equiv) (equal (sparseint$-unary-bittest-width op width offset x) (sparseint$-unary-bittest-width op-equiv width offset x))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-unary-bittest-width-of-pos-fix-width (equal (sparseint$-unary-bittest-width op (pos-fix width) offset x) (sparseint$-unary-bittest-width op width offset x)))
Theorem:
(defthm sparseint$-unary-bittest-width-pos-equiv-congruence-on-width (implies (pos-equiv width width-equiv) (equal (sparseint$-unary-bittest-width op width offset x) (sparseint$-unary-bittest-width op width-equiv offset x))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-unary-bittest-width-of-nfix-offset (equal (sparseint$-unary-bittest-width op width (nfix offset) x) (sparseint$-unary-bittest-width op width offset x)))
Theorem:
(defthm sparseint$-unary-bittest-width-nat-equiv-congruence-on-offset (implies (nat-equiv offset offset-equiv) (equal (sparseint$-unary-bittest-width op width offset x) (sparseint$-unary-bittest-width op width offset-equiv x))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-unary-bittest-width-of-sparseint$-fix-x (equal (sparseint$-unary-bittest-width op width offset (sparseint$-fix x)) (sparseint$-unary-bittest-width op width offset x)))
Theorem:
(defthm sparseint$-unary-bittest-width-sparseint$-equiv-congruence-on-x (implies (sparseint$-equiv x x-equiv) (equal (sparseint$-unary-bittest-width op width offset x) (sparseint$-unary-bittest-width op width offset x-equiv))) :rule-classes :congruence)