		Search-engine friendly clone of the ACL2 documentation.

Sbitset-pairp

Sbitset-blockp

(sbitset-blockp x) recognizes numbers that are valid as the block component of an sbitset-pairp.

Signature
(sbitset-blockp x) → bool
Returns: bool — Type (booleanp bool).

To ensure that sparse bitsets are canonical, we don't allow 0 as a valid block. The idea is that any block whose value is 0 should just be omitted from the set.

Definitions and Theorems

Function: sbitset-blockp$inline

(defun sbitset-blockp$inline (x)
  (declare (xargs :guard t))
  (let ((__function__ 'sbitset-blockp))
    (declare (ignorable __function__))
    (mbe :logic (and (posp x)
                     (< x (expt 2 *sbitset-block-size*)))
         :exec (and (integerp x)
                    (<= 1 x)
                    (<= x 1152921504606846975)))))

Theorem: booleanp-of-sbitset-blockp

(defthm booleanp-of-sbitset-blockp
  (b* ((bool (sbitset-blockp$inline x)))
    (booleanp bool))
  :rule-classes :type-prescription)

Theorem: sbitset-block-type

(defthm sbitset-block-type
  (implies (sbitset-blockp x) (posp x))
  :rule-classes :compound-recognizer)

Theorem: sbitset-block-upper-bound

(defthm sbitset-block-upper-bound
  (implies (sbitset-blockp x)
           (< x (expt 2 *sbitset-block-size*))))