sbitsets

(in-package "BITSETS")

(include-book "bits-between")

(local (include-book "centaur/bitops/equal-by-logbitp" :dir :system))

(local (include-book "centaur/bitops/ihs-extensions" :dir :system))

(local (include-book "centaur/misc/equal-sets" :dir :system))

(local (include-book "std/lists/revappend" :dir :system))

(local (include-book "std/lists/rev" :dir :system))

(local (include-book "std/lists/append" :dir :system))

(local (include-book "ihs/quotient-remainder-lemmas" :dir :system))

(local (in-theory (enable* definitions
      expensive-rules
      ash-1-removal)))

(defxdoc sbitsets
  :parents (std/bitsets)
  :short "Sparse bitsets library: an alternative to @(see bitsets) for
representing finite sets of natural numbers."
  :long "<h3>Introduction</h3>

<p>In the ordinary @(see bitsets) library, sets of natural numbers are encoded
as bignums.  This is perfectly fine when the set elements are relatively small,
but it is not an efficient way to deal with sets of large numbers.  For
instance, trying to insert a number like 2^30 into an ordinary bitset will
probably kill your Lisp.</p>

<p>Sparse bitsets are a more forgiving alternative.  They can handle very large
set elements, but still achieve bitset-like efficiencies in many cases.</p>

<p>Sparse bitsets are represented as ordered lists of @('(offset . block)')
pairs.  Loosely speaking, each such pair in the set @('X') means that:</p>

@({
  offset*blocksize + 0             \in X  iff  (logbitp 0 block)
  offset*blocksize + 1             \in X  iff  (logbitp 1 block)
    ...
  offset*blocksize + (blocksize-1) \in X  iff  (logbitp (blocksize-1) block)
})

<p>The @('blocksize') is a some constant determined by @(see
*sbitset-block-size*).  We'll assume it is 60 (which makes each @('block') a
fixnum on 64-bit CCL).</p>

<h4>Efficiency Considerations</h4>

<p>Sparse bitsets are essentially a hybrid of ordered sets and bitsets, and
their efficiency characteristics are very data dependent.</p>

<p>Sparse bitsets perform best on sets that have "clusters" of nearby
members, perhaps separated by wide gaps.  Here, sparse bitsets give you some of
the same benefits of bitsets, viz. word-at-a-time operations like union and the
space efficiency of using bit masks to represent the set members.</p>

<p>For completely dense sets, e.g., all integers in @('[0, 1000]'), sparse
bitsets are:</p>

<ul>

<li>Better than ordered sets, because they get to compress nearby elements into
 bitmasks and use word-at-a-time operations.</li>

<li>Somewhat worse than ordinary bitsets.  They are less space efficient due to
 the conses and offset numbers.  They are also more expensive for membership
 testing: regular bitsets can basically use O(1) array indexing via @(see
 logbitp), while sparse bitsets must use an O(n) search for the right
 pair.</li>

</ul>

<p>For "cluster-free" sets where the elements are so far apart that they
never fall into the same block, sparse bitsets are:</p>

<ul>

<li>Better than bitsets, which perform badly here since they can have large
segments of 0 bits that waste space and take time to process during set
operations.</li>

<li>Somewhat worse than ordered sets.  For instance, a set like {0, 60, 120}
would be encoded as @('((0 . 1) (1 . 1) (2 . 1))'), which is similar to its
ordered set representation except for the additional overhead of using @('(1
. 1)') to represent 60, etc.</li>

</ul>


<h3>Sparse Bitset Operations</h3>

<p>Convention:</p>

<ul>
<li>@('a, b, ...') denote set elements</li>
<li>@('X, Y, ...') denote sets.</li>
</ul>

<p>Valid sparse bitsets are recognized by @(see sbitsetp), and there is a
standard fixing function, @(see sbitset-fix).</p>

<p>We intend to eventually implement sparse analogues for all of the functions
in the @(see bitsets) library, and analogues for the bitset @(see reasoning)
techniques.  For now we have only finished a few of these operations:</p>

<h5>Sparse Bitset Construtors</h5>

<dl>

<dt>@('(sbitset-singleton a)')</dt>
<dd>Constructs the set @('{a}')</dd>

<dt>@('(sbitset-union X Y ...)')</dt>
<dd>Constructs the set @('X U Y U ...')</dd>

<dt>@('(sbitset-intersect X Y ...)')</dt>
<dd>Constructs the set @('X \intersect Y \intersect ...')</dd>

<dt>@('(sbitset-difference X Y)')</dt>
<dd>Constructs the set @('X - Y')</dd>

</dl>

<h5>Inspecting Sparse Bitsets</h5>

<dl>
<dt>Todo</dt>
</dl>

<h5>Enumerating Sparse Bitset Members</h5>

<dl>
<dt>@('(sbitset-members X)')</dt>
<dd>Constructs an ordinary ordered set with the elements of X.</dd>
<dd>Important in @(see reasoning) about sparse bitsets.</dd>
</dl>")

(defsection *sbitset-block-size*
  :parents (sbitset-pairp)
  :short "Size of each block in an sparse bitset."
  :long "<p>The block size can be any positive number, but for good performance
you probably want to use the maximal number such that:</p>

@({
 (fixnump (1- (expt 2 *sbitset-block-size*))) = T
})

<p>On CCL and SBCL, 60 is the right number.  For other Lisps, 60 is logically
fine, but other numbers may give you better performance.</p>

<p>Note: if you change this, you may wish to also write a corresponding,
optimized version of @(see sbitset-pair-members).</p>"
  (defconst *sbitset-block-size* 60))

(local (defthm floor-is-nonnegative-integer-quotient
    (implies (and (natp a) (posp b))
      (equal (floor a b)
        (nonnegative-integer-quotient a
          b)))))

(local (in-theory (disable truncate)))

(local (defthm truncate-is-nonnegative-integer-quotient
    (implies (and (natp a) (posp b))
      (equal (truncate a b)
        (nonnegative-integer-quotient a
          b)))))

(local (encapsulate nil
    (local (defun niq-ind
        (a b c)
        (declare (xargs :measure (nonnegative-integer-quotient c
              a)))
        (if (or (= (nfix a) 0)
            (< (ifix c) a))
          b
          (niq-ind a
            (- b 1)
            (- c a)))))
    (defthm niq-lemma
      (implies (and (posp a)
          (natp b)
          (natp c))
        (equal (equal (nonnegative-integer-quotient c
              a)
            b)
          (and (<= (* a b) c)
            (< c (+ a (* a b))))))
      :hints (("goal" :induct (niq-ind a b c)) (and stable-under-simplificationp '(:nonlinearp t))))
    (local (include-book "arithmetic-3/bind-free/top" :dir :system))
    (local (in-theory (disable cancel-mod-+-basic)))
    (local (defthm l0
        (implies (and (integerp a)
            (natp size)
            (<= (* size offset) a)
            (< a
              (+ size (* size offset)))
            (natp offset))
          (equal (+ a (* (- size) offset))
            (mod a size)))
        :hints (("Goal" :in-theory (enable mod) :do-not-induct t))))
    (make-event `(defthm mod-blocksize-nonsense
        (implies (and (integerp a)
            (<= (* ,BITSETS::*SBITSET-BLOCK-SIZE* offset)
              a)
            (< a
              (+ ,BITSETS::*SBITSET-BLOCK-SIZE*
                (* ,BITSETS::*SBITSET-BLOCK-SIZE* offset)))
            (natp offset))
          (equal (+ a
              (* ,(- BITSETS::*SBITSET-BLOCK-SIZE*) offset))
            (mod a ,BITSETS::*SBITSET-BLOCK-SIZE*)))))))

(local (in-theory (disable logbitp-when-too-small
      expt-2-monotonic
      associativity-of-append)))

(local (defthm integer-listp-of-append
    (implies (and (integer-listp x)
        (integer-listp y))
      (integer-listp (append x y)))))

(local (defthm rassoc-append
    (equal (append x (append y z))
      (append (append x y) z))))

(local (defun dec-induct
    (n)
    (if (zp n)
      n
      (dec-induct (1- n)))))

(local (defthm integerp-of-car-when-integer-listp
    (implies (integer-listp x)
      (equal (integerp (car x)) (consp x)))))

(local (defthmd member-equal-is-in
    (implies (setp x)
      (iff (member-equal a x)
        (in a x)))
    :hints (("Goal" :in-theory (enable in-to-member)))))

(local (make-event `(defthm expt-2-monotonic-specialized-for-block-size
      (implies (and (< a ,BITSETS::*SBITSET-BLOCK-SIZE*)
          (natp a))
        (< (expt 2 a)
          ,(EXPT 2 BITSETS::*SBITSET-BLOCK-SIZE*)))
      :hints (("Goal" :use ((:instance expt-2-monotonic
            (a a)
            (b ,BITSETS::*SBITSET-BLOCK-SIZE*))))))))

(local (defsection add-to-each
    (defthm consp-of-add-to-each
      (equal (consp (add-to-each offset x))
        (consp x))
      :hints (("Goal" :in-theory (enable add-to-each))))
    (defthm integer-listp-of-add-to-each
      (implies (and (integerp offset)
          (integer-listp x))
        (integer-listp (add-to-each offset x)))
      :hints (("Goal" :in-theory (enable add-to-each))))
    (local (defthm l0
        (implies (and (member-equal a
              (add-to-each offset x))
            (integerp offset)
            (integer-listp x))
          (integerp a))))
    (defthm member-equal-add-to-each
      (implies (and (force (integerp offset))
          (force (integer-listp x)))
        (iff (member-equal a
            (add-to-each offset x))
          (and (integerp a)
            (member-equal (- a offset)
              x)))))
    (defthm no-duplicatesp-equal-of-add-to-each
      (implies (and (no-duplicatesp-equal x)
          (force (integer-listp x))
          (force (integerp offset)))
        (no-duplicatesp-equal (add-to-each offset x))))
    (local (defthm l1
        (implies (and (integerp a) (integerp b))
          (equal (<< a b)
            (< a b)))
        :hints (("Goal" :in-theory (enable <<
             lexorder
             alphorder)))))
    (defthm setp-of-add-to-each
      (implies (and (integerp offset)
          (integer-listp x)
          (setp x))
        (setp (add-to-each offset x)))
      :hints (("Goal" :in-theory (enable* (:ruleset primitive-rules)
           add-to-each))))))

(local (defsection no-duplicatesp-equal-when-setp
    (local (defthm l0
        (implies (and (member-equal a x)
            (<< a (car x)))
          (not (setp x)))
        :hints (("Goal" :induct (len x)
           :in-theory (enable* (:ruleset primitive-rules)
             (:ruleset order-rules))))))
    (defthm no-duplicatesp-equal-when-setp
      (implies (setp x)
        (no-duplicatesp-equal x))
      :hints (("Goal" :in-theory (enable* (:ruleset primitive-rules)))))))

(local (defsection append-is-union
    (defun max-int
      (x)
      (cond ((atom x) nil)
        ((atom (cdr x)) (car x))
        (t (max (car x) (max-int (cdr x))))))
    (defun min-int
      (x)
      (cond ((atom x) nil)
        ((atom (cdr x)) (car x))
        (t (min (car x) (min-int (cdr x))))))
    (local (defthm l1
        (implies (and (case-split (integerp a))
            (case-split (integerp b)))
          (equal (<< a b)
            (< a b)))
        :hints (("Goal" :in-theory (enable <<
             lexorder
             alphorder)))))
    (local (defthm l2
        (implies (and (integer-listp x)
            (setp x))
          (equal (min-int x)
            (if (consp x)
              (car x)
              nil)))
        :hints (("Goal" :in-theory (enable* (:ruleset primitive-rules))))))
    (defthmd setp-of-append
      (implies (and (force (or (< (max-int x)
                (min-int y))
              (atom x)
              (atom y)))
          (force (integer-listp x))
          (force (integer-listp y))
          (force (setp x))
          (force (setp y)))
        (setp (append x y)))
      :hints (("Goal" :in-theory (enable* (:ruleset primitive-rules)))))
    (local (in-theory (enable setp-of-append)))
    (local (defthm in-of-append
        (implies (and (force (or (< (max-int x)
                  (min-int y))
                (atom x)
                (atom y)))
            (force (integer-listp x))
            (force (integer-listp y))
            (force (setp x))
            (force (setp y)))
          (equal (in a (append x y))
            (or (in a x)
              (in a y))))
        :hints (("goal" :use ((:instance member-equal-is-in
              (x (append x y))) (:instance member-equal-is-in
               (x x))
             (:instance member-equal-is-in
               (x y)))))))
    (defthmd append-is-union
      (implies (and (force (or (< (max-int x)
                (min-int y))
              (atom x)
              (atom y)))
          (force (integer-listp x))
          (force (integer-listp y))
          (force (setp x))
          (force (setp y)))
        (equal (append x y)
          (union x y))))))

(local (defsection consp-of-bits-between
    (local (defthm l1
        (implies (posp x)
          (logbitp (logbitp-mismatch x 0)
            x))
        :hints (("Goal" :in-theory (disable logbitp-mismatch-correct)
           :use ((:instance logbitp-mismatch-correct
              (a x)
              (b 0)))))))
    (local (defthm l2
        (implies (posp x)
          (< (logbitp-mismatch x 0)
            (integer-length x)))
        :rule-classes ((:rewrite) (:linear))))
    (local (defthm l3
        (implies (and (< x (expt 2 n))
            (posp x)
            (natp n))
          (<= (logbitp-mismatch x 0) n))
        :rule-classes ((:rewrite) (:linear))
        :hints (("Goal" :in-theory (disable integer-length-bounded-by-expt)
           :use ((:instance integer-length-bounded-by-expt
              (a x)))))))
    (local (defthm l4
        (implies (posp x)
          (natp (logbitp-mismatch x 0)))
        :hints (("Goal" :in-theory (enable natp)))
        :rule-classes ((:rewrite) (:type-prescription))))
    (defthm consp-of-bits-between
      (implies (and (< block (expt 2 n))
          (posp block)
          (natp n))
        (consp (bits-between 0 n block)))
      :hints (("Goal" :in-theory (disable member-equal-of-bits-between)
         :use ((:instance member-equal-of-bits-between
            (a (logbitp-mismatch block 0))
            (n 0)
            (x block)
            (m n))))))))

(defmacro the-sbitset-block
  (x)
  `(the (unsigned-byte ,BITSETS::*SBITSET-BLOCK-SIZE*)
    ,BITSETS::X))

(make-event `(define sbitset-blockp
    (x)
    :returns (bool booleanp
      :rule-classes :type-prescription)
    :parents (sbitset-pairp)
    :short "@(call sbitset-blockp) recognizes numbers that are valid as the
<i>block</i> component of an @(see sbitset-pairp)."
    :long "<p>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.</p>"
    :inline t
    (mbe :logic (and (posp x)
        (< x (expt 2 *sbitset-block-size*)))
      :exec (and (integerp x)
        (<= 1 x)
        (<= x ,(1- (EXPT 2 BITSETS::*SBITSET-BLOCK-SIZE*)))))
    ///
    (defthm sbitset-block-type
      (implies (sbitset-blockp x)
        (posp x))
      :rule-classes :compound-recognizer)
    (defthm sbitset-block-upper-bound
      (implies (sbitset-blockp x)
        (< x (expt 2 *sbitset-block-size*))))))

(define sbitset-pairp
  (x)
  :parents (sbitsets)
  :returns (pairp booleanp
    :rule-classes :type-prescription)
  :short "@(call sbitset-pairp) recognizes a valid @('(offset . block)') pair
for sparse bitsets."
  :inline t
  (and (consp x)
    (natp (car x))
    (sbitset-blockp (cdr x)))
  ///
  (defthm consp-when-sbitset-pairp
    (implies (sbitset-pairp x)
      (consp x))
    :rule-classes :compound-recognizer))

(define sbitset-pair
  ((offset natp :type unsigned-byte) (block sbitset-blockp))
  :returns pair
  :parents (sbitset-pairp)
  :short "@(call sbitset-pair) constructs a @('(offset . block)') pair."
  :inline t
  (cons offset block))

(define sbitset-pair-offset
  ((x sbitset-pairp))
  :parents (sbitset-pairp)
  :returns offset
  :short "@(call sbitset-pair-offset) gets the @('offset') from an @('(offset
  . block)') pair."
  :inline t
  (car x))

(define sbitset-pair-block
  ((x sbitset-pairp))
  :parents (sbitset-pairp)
  :returns block
  :short "@(call sbitset-pair-block) gets the @('block') from an @('(offset
  . block)') pair."
  :inline t
  (cdr x))

(defsection sbitset-pairp-basics
  :extension sbitset-pairp
  (local (in-theory (enable sbitset-pairp
        sbitset-pair
        sbitset-pair-offset
        sbitset-pair-block)))
  (defthm sbitset-pair-offset-of-sbitset-pair
    (equal (sbitset-pair-offset (sbitset-pair offset block))
      offset))
  (defthm sbitset-pair-block-of-sbitset-pair
    (equal (sbitset-pair-block (sbitset-pair offset block))
      block))
  (defthm sbitset-pair-offset-type
    (implies (force (sbitset-pairp x))
      (natp (sbitset-pair-offset x)))
    :rule-classes :type-prescription)
  (defthm sbitset-pair-block-type
    (implies (force (sbitset-pairp x))
      (and (integerp (sbitset-pair-block x))
        (< 0 (sbitset-pair-block x))))
    :rule-classes :type-prescription)
  (defthm sbitset-pair-block-upper-bound
    (implies (force (sbitset-pairp x))
      (< (sbitset-pair-block x)
        (expt 2 *sbitset-block-size*)))
    :rule-classes ((:rewrite) (:linear))
    :hints (("Goal" :use ((:instance sbitset-block-upper-bound
          (x (cdr x)))))))
  (defthm sbitset-pairp-of-sbitset-pair
    (implies (and (force (natp offset))
        (force (sbitset-blockp block)))
      (sbitset-pairp (sbitset-pair offset block))))
  (defthm sbitset-blockp-of-sbitset-pair-block
    (implies (force (sbitset-pairp x))
      (sbitset-blockp (sbitset-pair-block x)))))

(define sbitset-pair-members
  ((x sbitset-pairp))
  :returns set
  :parents (sbitset-members sbitset-pairp)
  :short "@(call sbitset-pair-members) extracts the members of a single @(see
sbitset-pairp)."
  :long "<p>For instance, if the pair is @('(0 . 7)'), we produce the set
@('{0, 1, 2}'); if the set is @('(1 . 7)'), we produce @('{60, 61, 62}').</p>

<p>This serves as the logical definition we use to reason about member
extraction.</p>

<p>Normally this function isn't executed.  When the block size is 32 or 60, we
can instead use the optimized @(see bits-0-31) or @(see 60bits-0-59) routines
instead.  But, if you change the block size to something else, this function
<b>will</b> be executed and its performance will probably be bad.  In this
case, you might want to write a custom @('bits-0-32') style routine for your
block size.</p>"
  (add-to-each (* (sbitset-pair-offset x)
      *sbitset-block-size*)
    (bits-between 0
      *sbitset-block-size*
      (sbitset-pair-block x)))
  ///
  (defthm sbitset-pair-members-of-nil
    (equal (sbitset-pair-members nil) nil))
  (defthm true-listp-of-sbitset-pair-members
    (true-listp (sbitset-pair-members x))
    :rule-classes :type-prescription)
  (defthm integer-listp-of-sbitset-pair-members
    (implies (force (sbitset-pairp x))
      (integer-listp (sbitset-pair-members x))))
  (local (include-book "arithmetic-3/bind-free/top" :dir :system))
  (defthm member-equal-sbitset-pair-members
    (implies (force (sbitset-pairp x))
      (iff (member-equal a
          (sbitset-pair-members x))
        (and (natp a)
          (equal (floor a *sbitset-block-size*)
            (sbitset-pair-offset x))
          (logbitp (mod a *sbitset-block-size*)
            (sbitset-pair-block x))))))
  (defthm no-duplicatesp-equal-of-sbitset-pair-members
    (implies (force (sbitset-pairp x))
      (no-duplicatesp-equal (sbitset-pair-members x))))
  (defthm offsets-must-agree-when-sbitset-pair-members-intersect
    (implies (and (force (sbitset-pairp x))
        (force (sbitset-pairp y))
        (intersectp-equal (sbitset-pair-members x)
          (sbitset-pair-members y))
        (syntaxp (term-order y x)))
      (equal (sbitset-pair-offset x)
        (sbitset-pair-offset y)))
    :hints ((set-reasoning)))
  (defthm consp-of-sbitset-pair-members
    (implies (force (sbitset-pairp x))
      (and (true-listp (sbitset-pair-members x))
        (consp (sbitset-pair-members x))))
    :rule-classes :type-prescription)
  (defthm setp-of-sbitset-pair-members
    (implies (force (sbitset-pairp a))
      (setp (sbitset-pair-members a))))
  (defthm in-of-sbitset-pair-members
    (implies (force (sbitset-pairp x))
      (equal (in a
          (sbitset-pair-members x))
        (and (natp a)
          (equal (floor a *sbitset-block-size*)
            (sbitset-pair-offset x))
          (logbitp (mod a *sbitset-block-size*)
            (sbitset-pair-block x)))))
    :hints (("Goal" :use ((:instance member-equal-is-in
          (x (sbitset-pair-members x)))))))
  (defthm emptyp-of-sbitset-pair-members
    (implies (force (sbitset-pairp x))
      (not (emptyp (sbitset-pair-members x))))
    :hints (("Goal" :in-theory (e/d* ((:ruleset primitive-rules))
         (sbitset-pair-members))))))

(local (defsection sbitset-pair-members-bounds
    (local (in-theory (enable sbitset-pair-members)))
    (local (defthm max-int-of-add-to-each
        (implies (and (force (integerp offset))
            (force (integer-listp x)))
          (equal (max-int (add-to-each offset x))
            (if (consp x)
              (+ offset (max-int x))
              nil)))
        :hints (("Goal" :induct (add-to-each offset x)
           :in-theory (enable add-to-each max-int)))))
    (local (defthm min-int-of-add-to-each
        (implies (and (force (integerp offset))
            (force (integer-listp x)))
          (equal (min-int (add-to-each offset x))
            (if (consp x)
              (+ offset (min-int x))
              nil)))
        :hints (("Goal" :induct (add-to-each offset x)
           :in-theory (enable add-to-each min-int)))))
    (local (defthm max-int-of-bits-between
        (implies (and (consp (bits-between n m x))
            (force (natp n))
            (force (natp m))
            (force (<= n m)))
          (< (max-int (bits-between n m x))
            m))
        :rule-classes ((:rewrite) (:linear))
        :hints (("Goal" :induct (bits-between n m x)
           :in-theory (enable bits-between)))))
    (local (defthm min-int-of-bits-between
        (implies (and (consp (bits-between n m x))
            (force (natp n))
            (force (natp m))
            (force (<= n m)))
          (<= n
            (min-int (bits-between n m x))))
        :rule-classes ((:rewrite) (:linear))
        :hints (("Goal" :induct (bits-between n m x)
           :in-theory (enable bits-between)))))
    (defthm sbitset-pair-members-upper-bound
      (implies (force (sbitset-pairp x))
        (< (max-int (sbitset-pair-members x))
          (* *sbitset-block-size*
            (+ (sbitset-pair-offset x) 1))))
      :rule-classes ((:rewrite) (:linear)))
    (defthm sbitset-pair-members-lower-bound
      (implies (force (sbitset-pairp x))
        (<= (* *sbitset-block-size*
            (sbitset-pair-offset x))
          (min-int (sbitset-pair-members x))))
      :rule-classes ((:rewrite) (:linear)))))

(define sbitsetp
  (x)
  :returns bool
  :parents (sbitsets)
  :short "@(call sbitsetp) determines whether @('X') is a well-formed sparse
bitset."
  (if (atom x)
    (not x)
    (and (sbitset-pairp (first x))
      (if (atom (cdr x))
        (not (cdr x))
        (and (sbitset-pairp (second x))
          (< (sbitset-pair-offset (first x))
            (sbitset-pair-offset (second x)))))
      (sbitsetp (cdr x))))
  ///
  (defthm true-listp-when-sbitsetp
    (implies (sbitsetp x)
      (true-listp x))
    :rule-classes :compound-recognizer)
  (defthm sbitsetp-when-atom
    (implies (atom x)
      (equal (sbitsetp x) (not x))))
  (defthm sbitsetp-of-cons
    (equal (sbitsetp (cons a x))
      (and (sbitset-pairp a)
        (sbitsetp x)
        (or (atom x)
          (< (sbitset-pair-offset a)
            (sbitset-pair-offset (first x)))))))
  (defthm sbitset-pairp-of-car
    (implies (sbitsetp x)
      (equal (sbitset-pairp (car x))
        (consp x))))
  (defthm sbitsetp-of-cdr
    (implies (sbitsetp x)
      (sbitsetp (cdr x))))
  (defthm sbitset-pairp-when-member-equal-of-sbitsetp
    (implies (and (member-equal a x)
        (sbitsetp x))
      (sbitset-pairp a))
    :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (sbitsetp x)
            (member-equal a x))
          (sbitset-pairp a))))))

(define sbitset-fix
  ((x sbitsetp))
  :parents (sbitsets)
  :short "@(call sbitset-fix) is a basic fixing function for sparse bitsets."
  :inline t
  (mbe :logic (if (sbitsetp x)
      x
      nil)
    :exec x)
  ///
  (defthm true-listp-of-sbitset-fix
    (true-listp (sbitset-fix x))
    :rule-classes :type-prescription)
  (defthm sbitsetp-of-sbitset-fix
    (sbitsetp (sbitset-fix x)))
  (defthm sbitset-fix-when-sbitsetp
    (implies (sbitsetp x)
      (equal (sbitset-fix x) x))))

(defsection sbitset-members
  :parents (sbitsets)
  :short "@(call sbitset-members) converts a bitset into an ordinary, ordered
set."
  :long "<p>In the logic, we just call @(see sbitset-pair-members) on each
block to get the members.</p>

<p>However, this function should typically be left disabled and you should not
reason about the underlying representation of sparse bitsets.</p>

<p>For faster execution, when the block size is 32 or 60 we use a partially
unrolled inner loop for extracting the bits from each block.  This optimization
is not performed for other block sizes.</p>"
  (make-event (b* ((fn (case *sbitset-block-size*
           (60 '60bits-0-59)
           (32 'bits-0-31)
           (otherwise nil))) (exec-def (if fn
            `(defun sbitset-members-exec
              (x acc)
              (declare (xargs :guard (sbitsetp x)))
              (if (atom x)
                acc
                (let* ((pair1 (car x)) (offset1 (sbitset-pair-offset pair1))
                    (block1 (sbitset-pair-block pair1)))
                  (,BITSETS::FN (* offset1 ,BITSETS::*SBITSET-BLOCK-SIZE*)
                    block1
                    (sbitset-members-exec (cdr x)
                      acc)))))
            `(value-triple :invisible)))
        (logic-body `(if (not (sbitsetp x))
            nil
            (if (atom x)
              nil
              (append (sbitset-pair-members (car x))
                (sbitset-members-aux (cdr x))))))
        (real-body (if fn
            `(mbe :logic ,BITSETS::LOGIC-BODY
              :exec (sbitset-members-exec x nil))
            logic-body))
        (remove-thm (if fn
            `(defthm sbitset-members-exec-removal
              (implies (force (sbitsetp x))
                (equal (sbitset-members-exec x acc)
                  (append (sbitset-members-aux x)
                    acc)))
              :hints (("Goal" :in-theory (enable sbitset-pair-members))))
            `(value-triple :invisible))))
      `(encapsulate nil
        ,BITSETS::EXEC-DEF
        (defund-inline sbitset-members-aux
          (x)
          (declare (xargs :guard (sbitsetp x)
              :verify-guards nil))
          ,BITSETS::REAL-BODY)
        (local (in-theory (enable sbitset-members-aux)))
        ,BITSETS::REMOVE-THM
        (verify-guards sbitset-members-aux$inline))))
  (define sbitset-members
    ((x sbitsetp))
    :inline t
    :verify-guards nil
    (mbe :logic (if (or (not (sbitsetp x)) (atom x))
        nil
        (union (sbitset-pair-members (car x))
          (sbitset-members (cdr x))))
      :exec (sbitset-members-exec x nil)))
  (local (in-theory (enable sbitset-members
        sbitset-members-aux)))
  (defsection guard-verification
    (local (defthm l0
        (integer-listp (sbitset-members-aux x))))
    (local (defthm l1
        (equal (consp (sbitset-members-aux x))
          (and (sbitsetp x) (consp x)))))
    (local (defthm l2
        (implies (setp (append x y))
          (and (setp (list-fix x))
            (setp y)))
        :hints (("Goal" :in-theory (enable* (:ruleset primitive-rules))))))
    (local (defthm l3
        (equal (min-int (append x y))
          (if (consp x)
            (if (consp y)
              (min (min-int x)
                (min-int y))
              (min-int x))
            (if (consp y)
              (min-int y)
              nil)))
        :hints (("Goal" :in-theory (enable min-int append)))))
    (local (defthm l4
        (setp (sbitset-members-aux x))
        :hints (("Goal" :in-theory (enable setp-of-append)))))
    (local (defthm l5
        (equal (sbitset-members-aux x)
          (if (or (atom x) (not (sbitsetp x)))
            nil
            (union (sbitset-pair-members (car x))
              (sbitset-members-aux (cdr x)))))
        :rule-classes :definition :hints (("Goal" :in-theory (e/d (append-is-union)
             (double-containment))))))
    (defthm sbitset-members-aux-removal
      (equal (sbitset-members-aux x)
        (sbitset-members x)))
    (verify-guards+ sbitset-members))
  (defthm sbitset-members-default
    (implies (not (sbitsetp a))
      (equal (sbitset-members a) nil)))
  (defthm sbitset-members-when-atom
    (implies (atom x)
      (equal (sbitset-members x) nil)))
  (local (defthm l0
      (implies (atom x)
        (equal (setp x) (not x)))
      :hints (("Goal" :in-theory (enable setp)))))
  (local (defthm union-under-iff
      (iff (union x y)
        (or (not (emptyp x))
          (not (emptyp y))))
      :hints (("Goal" :in-theory (enable* (:ruleset primitive-rules))))))
  (defthm sbitset-members-of-cons
    (implies (force (sbitsetp (cons a x)))
      (equal (sbitset-members (cons a x))
        (union (sbitset-pair-members a)
          (sbitset-members x)))))
  (defthm sbitset-members-of-sbitset-fix
    (equal (sbitset-members (sbitset-fix b))
      (sbitset-members b))
    :hints (("Goal" :in-theory (enable sbitset-fix))))
  (defthm true-listp-of-sbitset-members
    (true-listp (sbitset-members x))
    :rule-classes :type-prescription)
  (defthm setp-of-sbitset-members
    (setp (sbitset-members x)))
  (defthm no-duplicatesp-equal-of-sbitset-members
    (no-duplicatesp-equal (sbitset-members x))))

(define sbitset-find
  ((offset natp) (x sbitsetp))
  :parents (in-of-sbitset-members)
  :short "Helper definition; shouldn't be needed by users."
  (cond ((atom x) nil)
    ((equal (sbitset-pair-offset (car x))
       offset) (car x))
    (t (sbitset-find offset (cdr x))))
  ///
  (defthm sbitset-find-when-atom
    (implies (atom x)
      (equal (sbitset-find offset x)
        nil)))
  (defthm sbitset-find-of-cons
    (equal (sbitset-find offset
        (cons a x))
      (if (equal (sbitset-pair-offset a)
          offset)
        a
        (sbitset-find offset x))))
  (defthm member-equal-of-sbitset-find
    (implies (sbitset-find offset x)
      (member-equal (sbitset-find offset x)
        x)))
  (defthm sbitset-pairp-of-sbitset-find
    (implies (force (sbitsetp x))
      (equal (sbitset-pairp (sbitset-find offset x))
        (if (sbitset-find offset x)
          t
          nil))))
  (defthm sbitset-pair-offset-of-sbitset-find
    (implies (sbitsetp x)
      (equal (sbitset-pair-offset (sbitset-find offset x))
        (if (sbitset-find offset x)
          offset
          nil))))
  (defthm natp-when-sbitset-find
    (implies (and (sbitset-find offset x)
        (sbitsetp x))
      (natp offset))
    :rule-classes (:forward-chaining)))

(defsection in-of-sbitset-members
  :parents (sbitset-members)
  :short "Low-level lemma to rewrite @('(in a (sbitset-members x))') into a
more structural form."
  :long "<p>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.</p>

<p>This is a little more complicated than in the basic bitset library, because
we have to go to the proper pair.</p>"
  (local (defthm l0
      (implies (and (sbitsetp x)
          (in a (sbitset-members x)))
        (sbitset-find (floor a *sbitset-block-size*)
          x))
      :hints (("Goal" :in-theory (disable mod-blocksize-nonsense)
         :induct (len x)
         :expand ((sbitset-members x))))))
  (local (defthm l1
      (implies (and (sbitsetp x)
          (< offset
            (sbitset-pair-offset (car x))))
        (not (sbitset-find offset x)))
      :hints (("Goal" :in-theory (enable sbitset-find)))))
  (local (defthm l2
      (implies (and (sbitset-pairp x)
          (in a
            (sbitset-pair-members x)))
        (equal (sbitset-pair-offset x)
          (floor a *sbitset-block-size*)))))
  (local (defthm l3
      (implies (sbitsetp x)
        (equal (in a (sbitset-members x))
          (let ((pair (sbitset-find (floor a *sbitset-block-size*)
                 x)))
            (and pair
              (in a
                (sbitset-pair-members pair))))))
      :hints (("Goal" :induct (len x)
         :expand ((sbitset-members x) (:free (n)
             (sbitset-find n x)))
         :in-theory (disable in-of-sbitset-pair-members)
         :do-not '(generalize fertilize)))))
  (defthmd 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))))))
    :hints (("Goal" :use ((:instance l3))))))

(local (in-theory (enable in-of-sbitset-members)))

(make-event `(define sbitset-singleton-pair
    ((a natp :type unsigned-byte))
    :returns (pair sbitset-pairp)
    :parents (sbitset-singleton)
    :short "@(call sbitset-singleton-pair) creates a @(see sbitset-pairp) whose
only member is @('a')."
    :guard-hints (("Goal" :in-theory (enable sbitset-blockp)))
    :split-types t
    :prepwork ((local (in-theory (enable sbitset-blockp))) (local (include-book "arithmetic-3/bind-free/top" :dir :system)))
    :inline t
    (mbe :logic (let ((a (nfix a)))
        (sbitset-pair (floor a *sbitset-block-size*)
          (expt 2 (mod a *sbitset-block-size*))))
      :exec (sbitset-pair (truncate a ,BITSETS::*SBITSET-BLOCK-SIZE*)
        (ash 1 (rem a ,BITSETS::*SBITSET-BLOCK-SIZE*))))
    ///
    (defthm sbitset-pair-offset-of-sbitset-singleton-pair
      (equal (sbitset-pair-offset (sbitset-singleton-pair a))
        (floor (nfix a)
          *sbitset-block-size*)))
    (defthm sbiset-pair-block-of-sbitset-singleton-pair
      (equal (sbitset-pair-block (sbitset-singleton-pair a))
        (expt 2
          (mod (nfix a)
            *sbitset-block-size*))))))

(define sbitset-singleton
  ((a natp :type unsigned-byte))
  :parents (sbitsets)
  :short "@(call sbitset-singleton) constructs the singleton set @('{a}')."
  :split-types t
  :inline t
  :returns (sbitset sbitsetp)
  (list (sbitset-singleton-pair a))
  ///
  (local (include-book "arithmetic-3/bind-free/top" :dir :system))
  (local (defthm l0
      (equal (in a
          (sbitset-members (sbitset-singleton b)))
        (equal a (nfix b)))
      :hints (("goal" :use ((:instance niq-lemma
            (c (nfix b))
            (a 60)
            (b a)))
         :in-theory (e/d (mod)
           (niq-lemma mod-blocksize-nonsense))))))
  (defthm sbitset-members-of-sbitset-singleton
    (equal (sbitset-members (sbitset-singleton a))
      (insert (nfix a) nil))
    :hints (("Goal" :in-theory (disable sbitset-singleton)))))

(local (defthm sbitset-blockp-of-logior
    (implies (and (force (sbitset-blockp x))
        (force (sbitset-blockp y)))
      (sbitset-blockp (logior x y)))
    :hints (("Goal" :in-theory (e/d (sbitset-blockp)
         (upper-bound-of-logior-for-naturals))
       :use ((:instance upper-bound-of-logior-for-naturals
          (x x)
          (y y)
          (n *sbitset-block-size*)))))))

(local (defthm equal-of-sbitset-pair
    (implies (force (sbitset-pairp x))
      (equal (equal (sbitset-pair offset block)
          x)
        (and (equal offset
            (sbitset-pair-offset x))
          (equal block (sbitset-pair-block x)))))
    :hints (("Goal" :in-theory (enable sbitset-pair
         sbitset-pairp
         sbitset-pair-offset
         sbitset-pair-block)))))

(local (defthm lower-bound-of-first-offset-of-sbitset-find
    (implies (and (sbitset-find b x)
        (<= b a)
        (sbitsetp x))
      (<= (sbitset-pair-offset (car x))
        a))
    :rule-classes ((:rewrite) (:linear))
    :hints (("goal" :in-theory (enable sbitset-find)
       :do-not '(generalize fertilize)))))

(defsection sbitset-union
  :parents (sbitsets)
  :short "@('(sbitset-union X Y ...)') constructs the set @('X U Y U ...')."
  :long "@(def sbitset-union)"
  (define sbitset-union-exec
    ((x sbitsetp) (y sbitsetp))
    :measure (+ (len x) (len y))
    (b* (((when (atom x)) y) ((when (atom y)) x)
        (x1 (car x))
        (y1 (car y))
        ((the unsigned-byte x1.offset) (sbitset-pair-offset x1))
        ((the unsigned-byte y1.offset) (sbitset-pair-offset y1))
        ((when (< x1.offset y1.offset)) (cons x1
            (sbitset-union-exec (cdr x) y)))
        ((unless (eql x1.offset y1.offset)) (cons y1
            (sbitset-union-exec x (cdr y))))
        (x1.block (sbitset-pair-block x1))
        (y1.block (sbitset-pair-block y1))
        (new-block (the-sbitset-block (logior (the-sbitset-block x1.block)
              (the-sbitset-block y1.block))))
        (new-pair (sbitset-pair x1.offset
            new-block)))
      (cons new-pair
        (sbitset-union-exec (cdr x)
          (cdr y)))))
  (define sbitset-binary-union
    ((x sbitsetp) (y sbitsetp))
    :inline t
    (mbe :logic (sbitset-union-exec (sbitset-fix x)
        (sbitset-fix y))
      :exec (sbitset-union-exec x y)))
  (defmacro sbitset-union
    (&rest args)
    (cond ((atom args) nil)
      ((atom (cdr args)) (car args))
      (t (xxxjoin 'sbitset-binary-union
          args))))
  (add-macro-alias sbitset-union
    sbitset-binary-union$inline)
  (add-macro-fn sbitset-union
    sbitset-binary-union$inline
    t)
  (local (in-theory (enable sbitset-union-exec
        sbitset-union)))
  (local (defthm c0
      (implies (and (< a (sbitset-pair-offset x1))
          (< a
            (sbitset-pair-offset (car y2)))
          (sbitset-pairp x1)
          (sbitsetp y2))
        (< a
          (sbitset-pair-offset (car (sbitset-union-exec (cons x1 x2)
                y2)))))
      :rule-classes ((:rewrite) (:linear))))
  (local (defthm c1
      (implies (and (< a (sbitset-pair-offset y1))
          (< a
            (sbitset-pair-offset (car x2)))
          (sbitsetp x2)
          (sbitset-pairp y1))
        (< a
          (sbitset-pair-offset (car (sbitset-union-exec x2
                (cons y1 y2))))))
      :rule-classes ((:rewrite) (:linear))))
  (local (defthm c2
      (implies (and (< a
            (sbitset-pair-offset (car x2)))
          (< a
            (sbitset-pair-offset (car y2)))
          (sbitset-pairp x1)
          (sbitsetp y2))
        (< a
          (sbitset-pair-offset (car (sbitset-union-exec x2 y2)))))
      :rule-classes ((:rewrite) (:linear))))
  (defthm sbitsetp-of-sbitset-union-exec
    (implies (and (sbitsetp x)
        (sbitsetp y))
      (sbitsetp (sbitset-union-exec x y)))
    :hints (("Goal" :induct (sbitset-union-exec x y)
       :do-not '(generalize fertilize))))
  (local (defthm l0
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (iff (sbitset-find offset
            (sbitset-union-exec x y))
          (or (sbitset-find offset x)
            (sbitset-find offset y))))
      :hints (("Goal" :induct (sbitset-union-exec x y)
         :in-theory (enable sbitset-union-exec)))))
  (local (defthm m0
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (equal (sbitset-find offset
            (sbitset-union-exec x y))
          (let* ((|X[OFFSET]| (sbitset-find offset x)) (|Y[OFFSET]| (sbitset-find offset y)))
            (cond ((and |X[OFFSET]| |Y[OFFSET]|) (sbitset-pair offset
                  (logior (sbitset-pair-block |X[OFFSET]|)
                    (sbitset-pair-block |Y[OFFSET]|))))
              (|X[OFFSET]|)
              (|Y[OFFSET]|)
              (t nil)))))
      :hints (("Goal" :induct (sbitset-union-exec x y)
         :in-theory (enable sbitset-union-exec
           sbitset-find)
         :do-not '(generalize fertilize)))))
  (in-theory (disable sbitset-union-exec))
  (local (defthm m1
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (equal (in a
            (sbitset-members (sbitset-union-exec x y)))
          (or (in a (sbitset-members x))
            (in a (sbitset-members y)))))))
  (local (defthm sbitset-members-of-sbitset-union-exec
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (equal (sbitset-members (sbitset-union-exec x y))
          (union (sbitset-members x)
            (sbitset-members y))))))
  (local (in-theory (enable sbitset-union)))
  (defthm sbitset-of-sbitset-union
    (sbitsetp (sbitset-union x y)))
  (defthm sbitset-members-of-sbitset-union
    (equal (sbitset-members (sbitset-union x y))
      (union (sbitset-members x)
        (sbitset-members y)))))

(local (defthm sbitset-blockp-of-logand
    (implies (and (force (sbitset-blockp x))
        (force (sbitset-blockp y)))
      (equal (sbitset-blockp (logand x y))
        (not (zp (logand x y)))))
    :hints (("Goal" :in-theory (e/d (sbitset-blockp)
         (unsigned-byte-p-of-logand-1 unsigned-byte-p-of-logand-2))
       :use ((:instance unsigned-byte-p-of-logand-1
          (x x)
          (y y)
          (n *sbitset-block-size*)))))))

(defsection sbitset-intersect
  :parents (sbitsets)
  :short "@('(sbitset-intersect X Y ...)') constructs the set @('X \intersect Y
\intersect ...')."
  :long "@(def sbitset-intersect)"
  (define sbitset-intersect-exec
    ((x sbitsetp) (y sbitsetp))
    :measure (+ (len x) (len y))
    (b* (((when (atom x)) nil) ((when (atom y)) nil)
        (x1 (car x))
        (y1 (car y))
        ((the unsigned-byte x1.offset) (sbitset-pair-offset x1))
        ((the unsigned-byte y1.offset) (sbitset-pair-offset y1))
        ((when (< x1.offset y1.offset)) (sbitset-intersect-exec (cdr x)
            y))
        ((unless (eql x1.offset y1.offset)) (sbitset-intersect-exec x
            (cdr y)))
        (x1.block (sbitset-pair-block x1))
        (y1.block (sbitset-pair-block y1))
        (new-block (the-sbitset-block (logand (the-sbitset-block x1.block)
              (the-sbitset-block y1.block))))
        ((when (eql 0 (the-sbitset-block new-block))) (sbitset-intersect-exec (cdr x)
            (cdr y)))
        (new-pair (sbitset-pair x1.offset
            new-block)))
      (cons new-pair
        (sbitset-intersect-exec (cdr x)
          (cdr y)))))
  (define sbitset-binary-intersect
    ((x sbitsetp) (y sbitsetp))
    :inline t
    (mbe :logic (sbitset-intersect-exec (sbitset-fix x)
        (sbitset-fix y))
      :exec (sbitset-intersect-exec x y)))
  (defmacro sbitset-intersect
    (&rest args)
    (cond ((atom args) nil)
      ((atom (cdr args)) (car args))
      (t (xxxjoin 'sbitset-binary-intersect
          args))))
  (add-macro-alias sbitset-intersect
    sbitset-binary-intersect$inline)
  (add-macro-fn sbitset-intersect
    sbitset-binary-intersect$inline
    t)
  (local (in-theory (enable sbitset-intersect-exec
        sbitset-intersect)))
  (local (defthm c0
      (implies (and (sbitset-intersect-exec x2 y2)
          (< (sbitset-pair-offset x1)
            (sbitset-pair-offset (car y2)))
          (sbitset-pairp x1)
          (sbitsetp x2)
          (sbitset-pairp y1)
          (sbitsetp y2))
        (< (sbitset-pair-offset x1)
          (sbitset-pair-offset (car (sbitset-intersect-exec x2 y2)))))))
  (defthm sbitsetp-of-sbitset-intersect-exec
    (implies (and (sbitsetp x)
        (sbitsetp y))
      (sbitsetp (sbitset-intersect-exec x y)))
    :hints (("Goal" :induct (sbitset-intersect-exec x y)
       :do-not '(generalize fertilize))))
  (local (defthm l0
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (iff (sbitset-find offset
            (sbitset-intersect-exec x y))
          (let ((a (sbitset-find offset x)) (b (sbitset-find offset y)))
            (and a
              b
              (not (zp (logand (sbitset-pair-block a)
                    (sbitset-pair-block b))))))))
      :hints (("Goal" :induct (sbitset-intersect-exec x y)
         :in-theory (enable sbitset-intersect-exec)))))
  (local (defthm m0
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (equal (sbitset-find offset
            (sbitset-intersect-exec x y))
          (let* ((a (sbitset-find offset x)) (b (sbitset-find offset y))
              (new-block (logand (sbitset-pair-block a)
                  (sbitset-pair-block b))))
            (and a
              b
              (not (zp new-block))
              (sbitset-pair offset new-block)))))
      :hints (("Goal" :induct (sbitset-intersect-exec x y)
         :in-theory (enable sbitset-intersect-exec
           sbitset-find)
         :do-not '(generalize fertilize)))))
  (in-theory (disable sbitset-intersect-exec))
  (local (defthm n0
      (implies (and (logbitp a x)
          (equal (logand x y) 0))
        (not (logbitp a y)))
      :hints (("Goal" :in-theory (disable logbitp-of-logand)
         :use ((:instance logbitp-of-logand
            (a a)
            (x x)
            (y y)))))))
  (local (defthm m1
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (equal (in a
            (sbitset-members (sbitset-intersect-exec x y)))
          (and (in a (sbitset-members x))
            (in a (sbitset-members y)))))))
  (local (defthm sbitset-members-of-sbitset-intersect-exec
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (equal (sbitset-members (sbitset-intersect-exec x y))
          (intersect (sbitset-members x)
            (sbitset-members y))))
      :hints (("Goal" :in-theory (disable (force))))))
  (local (in-theory (enable sbitset-intersect)))
  (defthm sbitset-of-sbitset-intersect
    (sbitsetp (sbitset-intersect x y)))
  (defthm sbitset-members-of-sbitset-intersect
    (equal (sbitset-members (sbitset-intersect x y))
      (intersect (sbitset-members x)
        (sbitset-members y)))))

(local (defthm sbitset-blockp-of-logandc2
    (implies (and (force (sbitset-blockp x))
        (force (sbitset-blockp y)))
      (equal (sbitset-blockp (logand x (lognot y)))
        (not (zp (logand x (lognot y))))))
    :hints (("Goal" :in-theory (e/d (sbitset-blockp)
         (unsigned-byte-p-of-logand-1 unsigned-byte-p-of-logand-2))
       :use ((:instance unsigned-byte-p-of-logand-1
          (x x)
          (y (lognot y))
          (n *sbitset-block-size*)))))))

(define sbitset-difference
  ((x sbitsetp) (y sbitsetp))
  :returns sbitset
  :parents (sbitsets)
  :short "@('(sbitset-difference X Y)') constructs the set @('X - Y')."
  :prepwork ((define sbitset-difference-exec
     ((x sbitsetp) (y sbitsetp))
     :measure (+ (len x) (len y))
     (b* (((when (atom x)) nil) ((when (atom y)) x)
         (x1 (car x))
         (y1 (car y))
         ((the unsigned-byte x1.offset) (sbitset-pair-offset x1))
         ((the unsigned-byte y1.offset) (sbitset-pair-offset y1))
         ((when (< x1.offset y1.offset)) (cons (car x)
             (sbitset-difference-exec (cdr x)
               y)))
         ((unless (eql x1.offset y1.offset)) (sbitset-difference-exec x
             (cdr y)))
         (x1.block (sbitset-pair-block x1))
         (y1.block (sbitset-pair-block y1))
         (new-block (the-sbitset-block (logandc2 (the-sbitset-block x1.block)
               (the-sbitset-block y1.block))))
         ((when (eql 0 (the-sbitset-block new-block))) (sbitset-difference-exec (cdr x)
             (cdr y)))
         (new-pair (sbitset-pair x1.offset
             new-block)))
       (cons new-pair
         (sbitset-difference-exec (cdr x)
           (cdr y))))))
  :inline t
  (mbe :logic (sbitset-difference-exec (sbitset-fix x)
      (sbitset-fix y))
    :exec (sbitset-difference-exec x y))
  ///
  (local (in-theory (enable sbitset-difference-exec)))
  (local (defthm c1
      (implies (and (< a
            (sbitset-pair-offset (car x2)))
          (< a
            (sbitset-pair-offset (car y2)))
          (sbitset-difference-exec x2 y2)
          (sbitsetp x2)
          (sbitsetp y2))
        (< a
          (sbitset-pair-offset (car (sbitset-difference-exec x2 y2)))))))
  (defthm sbitsetp-of-sbitset-difference-exec
    (implies (and (sbitsetp x)
        (sbitsetp y))
      (sbitsetp (sbitset-difference-exec x y)))
    :hints (("Goal" :induct (sbitset-difference-exec x y)
       :do-not '(generalize fertilize))))
  (local (defthm l0
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (iff (sbitset-find offset
            (sbitset-difference-exec x y))
          (let* ((a (sbitset-find offset x)) (b (sbitset-find offset y))
              (new-block (logandc2 (sbitset-pair-block a)
                  (sbitset-pair-block b))))
            (and a
              (or (not b) (not (zp new-block)))))))
      :hints (("Goal" :induct (sbitset-difference-exec x y)
         :in-theory (enable sbitset-difference-exec)))))
  (local (defthm m0
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (equal (sbitset-find offset
            (sbitset-difference-exec x y))
          (let* ((a (sbitset-find offset x)) (b (sbitset-find offset y))
              (new-block (logandc2 (sbitset-pair-block a)
                  (sbitset-pair-block b))))
            (and a
              (if (not b)
                a
                (and (not (zp new-block))
                  (sbitset-pair offset new-block)))))))
      :hints (("Goal" :induct (sbitset-difference-exec x y)
         :in-theory (enable sbitset-difference-exec
           sbitset-find)
         :do-not '(generalize fertilize)))))
  (in-theory (disable sbitset-difference-exec))
  (local (defthm n0
      (implies (and (equal (logand x (lognot y)) 0)
          (logbitp a x))
        (logbitp a y))
      :hints (("Goal" :in-theory (disable logbitp-of-logand)
         :use ((:instance logbitp-of-logand
            (a a)
            (x x)
            (y (lognot y))))))))
  (local (defthm m1
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (equal (in a
            (sbitset-members (sbitset-difference-exec x y)))
          (and (in a (sbitset-members x))
            (not (in a (sbitset-members y))))))))
  (local (defthm sbitset-members-of-sbitset-difference-exec
      (implies (and (sbitsetp x)
          (sbitsetp y))
        (equal (sbitset-members (sbitset-difference-exec x y))
          (difference (sbitset-members x)
            (sbitset-members y))))
      :hints (("Goal" :in-theory (disable (force))))))
  (local (in-theory (enable sbitset-difference)))
  (defthm sbitset-of-sbitset-difference
    (sbitsetp (sbitset-difference x y)))
  (defthm sbitset-members-of-sbitset-difference
    (equal (sbitset-members (sbitset-difference x y))
      (difference (sbitset-members x)
        (sbitset-members y)))))