Recognizer for bit-size.
(bit-size-p x) → yes/no
Function:
(defun bit-size-p (x) (declare (xargs :guard t)) (and (integerp x) (integerp (/ x 8)) (<= 8 x) (<= x 256)))
Theorem:
(defthm booleanp-of-bit-size-p (b* ((yes/no (bit-size-p x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm bit-size-p-alt-def (iff (bit-size-p x) (member x (list 8 16 24 32 40 48 56 64 72 80 88 96 104 112 120 128 136 144 152 160 168 176 184 192 200 208 216 224 232 240 248 256))))