(sparseint$-unary-bittest op x) → test
Function:
(defun sparseint$-unary-bittest (op x) (declare (type (unsigned-byte 2) op)) (declare (xargs :guard (and (integerp op) (sparseint$-p x)))) (let ((__function__ 'sparseint$-unary-bittest)) (declare (ignorable __function__)) (sparseint$-unary-bittest-offset op 0 x)))
Theorem:
(defthm booleanp-of-sparseint$-unary-bittest (b* ((test (sparseint$-unary-bittest op x))) (booleanp test)) :rule-classes :type-prescription)
Theorem:
(defthm sparseint$-unary-bittest-correct (b* ((?test (sparseint$-unary-bittest op x))) (equal test (not (equal (unary-bitop op (sparseint$-val x)) 0)))))
Theorem:
(defthm sparseint$-unary-bittest-of-ifix-op (equal (sparseint$-unary-bittest (ifix op) x) (sparseint$-unary-bittest op x)))
Theorem:
(defthm sparseint$-unary-bittest-int-equiv-congruence-on-op (implies (int-equiv op op-equiv) (equal (sparseint$-unary-bittest op x) (sparseint$-unary-bittest op-equiv x))) :rule-classes :congruence)
Theorem:
(defthm sparseint$-unary-bittest-of-sparseint$-fix-x (equal (sparseint$-unary-bittest op (sparseint$-fix x)) (sparseint$-unary-bittest op x)))
Theorem:
(defthm sparseint$-unary-bittest-sparseint$-equiv-congruence-on-x (implies (sparseint$-equiv x x-equiv) (equal (sparseint$-unary-bittest op x) (sparseint$-unary-bittest op x-equiv))) :rule-classes :congruence)