		Search-engine friendly clone of the ACL2 documentation.

Bit-size

Bit-size-p

Recognizer for bit-size.

Signature
(bit-size-p x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: bit-size-p

(defun bit-size-p (x)
  (declare (xargs :guard t))
  (and (integerp x)
       (integerp (/ x 8))
       (<= 8 x)
       (<= x 256)))

Theorem: booleanp-of-bit-size-p

(defthm booleanp-of-bit-size-p
  (b* ((yes/no (bit-size-p x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: bit-size-p-alt-def

(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))))