• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
      • Bitsets
        • Bitset-members
        • Bitset-insert
        • Bitset-delete
        • Bitset-intersectp
        • Bitset-intersect
          • Bitset-binary-intersect
        • Bitset-difference
        • Bitset-subsetp
        • Bitset-union
        • Bitset-memberp
        • Bitset-singleton
        • Bitset-list
        • Bitset-cardinality
        • Bitset-list*
        • Utilities
      • Sbitsets
      • Reasoning
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Bitsets

Bitset-intersect

(bitset-intersect X Y ...) constructs the set X \intersect Y \intersect ....

Note: if you only want to know whether or not two sets intersect, bitset-intersectp is probably more efficient.

Definitions and Theorems

Function: bitset-binary-intersect$inline

(defun bitset-binary-intersect$inline (x y)
  (declare (type unsigned-byte x)
           (type unsigned-byte y))
  (declare (xargs :guard (and (natp x) (natp y))))
  (declare (xargs :split-types t))
  (let ((__function__ 'bitset-binary-intersect))
    (declare (ignorable __function__))
    (the unsigned-byte
         (logand (the unsigned-byte (lnfix x))
                 (the unsigned-byte (lnfix y))))))

Theorem: natp-of-bitset-binary-intersect

(defthm natp-of-bitset-binary-intersect
  (b* ((bitset (bitset-binary-intersect$inline x y)))
    (natp bitset))
  :rule-classes :type-prescription)

Theorem: bitset-intersect-when-not-natp-left

(defthm bitset-intersect-when-not-natp-left
  (implies (not (natp x))
           (equal (bitset-intersect x y) 0)))

Theorem: bitset-intersect-when-not-natp-right

(defthm bitset-intersect-when-not-natp-right
  (implies (not (natp y))
           (equal (bitset-intersect x y) 0)))

Theorem: bitset-intersect-of-nfix-left

(defthm bitset-intersect-of-nfix-left
  (equal (bitset-intersect (nfix x) y)
         (bitset-intersect x y)))

Theorem: bitset-intersect-of-nfix-right

(defthm bitset-intersect-of-nfix-right
  (equal (bitset-intersect x (nfix y))
         (bitset-intersect x y)))

Theorem: bitset-members-of-bitset-intersect

(defthm bitset-members-of-bitset-intersect
  (equal (bitset-members (bitset-intersect x y))
         (intersect (bitset-members x)
                    (bitset-members y))))

Subtopics

Bitset-binary-intersect