• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
      • Bitsets
      • Sbitsets
        • Sbitset-members
        • Sbitset-pairp
        • Sbitsetp
        • Sbitset-difference
        • Sbitset-intersect
        • Sbitset-union
        • Sbitset-singleton
        • Sbitset-fix
      • Reasoning
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Sbitsets

Sbitset-difference

(sbitset-difference X Y) constructs the set X - Y.

Signature

(sbitset-difference x y) → sbitset

Arguments

x — Guard (sbitsetp x).

y — Guard (sbitsetp y).

Definitions and Theorems

Function: sbitset-difference-exec

(defun
 sbitset-difference-exec (x y)
 (declare (xargs :guard (and (sbitsetp x) (sbitsetp y))))
 (let
  ((__function__ 'sbitset-difference-exec))
  (declare (ignorable __function__))
  (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))))))

Function: sbitset-difference$inline

(defun acl2::sbitset-difference$inline (x y)
       (declare (xargs :guard (and (sbitsetp x) (sbitsetp y))))
       (let ((__function__ 'sbitset-difference))
            (declare (ignorable __function__))
            (mbe :logic (sbitset-difference-exec (sbitset-fix x)
                                                 (sbitset-fix y))
                 :exec (sbitset-difference-exec x y))))

Theorem: sbitsetp-of-sbitset-difference-exec

(defthm sbitsetp-of-sbitset-difference-exec
        (implies (and (sbitsetp x) (sbitsetp y))
                 (sbitsetp (sbitset-difference-exec x y))))

Theorem: sbitset-of-sbitset-difference

(defthm sbitset-of-sbitset-difference
        (sbitsetp (sbitset-difference x y)))

Theorem: sbitset-members-of-sbitset-difference

(defthm sbitset-members-of-sbitset-difference
        (equal (sbitset-members (sbitset-difference x y))
               (difference (sbitset-members x)
                           (sbitset-members y))))