		Search-engine friendly clone of the ACL2 documentation.

Sbitset-members

In-of-sbitset-members

Low-level lemma to rewrite (in a (sbitset-members x)) into a more structural form.

This theorem is disabled by default and most users shouldn't enable it. It's only needed to prove properties about the basic sbitset constructors.

This is a little more complicated than in the basic bitset library, because we have to go to the proper pair.

Definitions and Theorems

Theorem: in-of-sbitset-members

(defthm in-of-sbitset-members
  (equal
       (in a (sbitset-members x))
       (and (sbitsetp x)
            (let ((pair (sbitset-find (floor a *sbitset-block-size*)
                                      x)))
              (and pair
                   (in a (sbitset-pair-members pair)))))))

Subtopics

Sbitset-find: Helper definition; shouldn't be needed by users.