		Search-engine friendly clone of the ACL2 documentation.

Bitsets

Bitset-memberp

(bitset-memberp a x) tests whether a is a member of the set X.

Signature
(bitset-memberp a x) → bool
Arguments: a — Guard (natp a).; x — Guard (natp x).
Returns: bool — Type (booleanp bool).

This is reasonably efficient: it executes as logbitp and does not need to use bitset-members.

We prefer to reason about (set::in a (bitset-members X)). We could have used this as the :logic definition, but the logbitp-based definition should be better for symbolic simulation with ACL2::gl.

Definitions and Theorems

Function: bitset-memberp$inline

(defun acl2::bitset-memberp$inline (a x)
  (declare (type unsigned-byte a)
           (type unsigned-byte x))
  (declare (xargs :guard (and (natp a) (natp x))))
  (declare (xargs :split-types t))
  (let ((__function__ 'bitset-memberp))
    (declare (ignorable __function__))
    (logbitp a (the unsigned-byte (lnfix x)))))

Theorem: booleanp-of-bitset-memberp

(defthm acl2::booleanp-of-bitset-memberp
  (b* ((bool (acl2::bitset-memberp$inline a x)))
    (booleanp bool))
  :rule-classes :type-prescription)

Theorem: bitset-memberp-removal

(defthm bitset-memberp-removal
  (equal (bitset-memberp a x)
         (in (nfix a) (bitset-members x))))