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

• Sbitsets

Sbitsetp

(sbitsetp x) determines whether X is a well-formed sparse bitset.

Signature

(sbitsetp x) → bool

Definitions and Theorems

Function: sbitsetp

(defun sbitsetp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'sbitsetp))
    (declare (ignorable __function__))
    (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))))))

Theorem: true-listp-when-sbitsetp

(defthm true-listp-when-sbitsetp
  (implies (sbitsetp x) (true-listp x))
  :rule-classes :compound-recognizer)

Theorem: sbitsetp-when-atom

(defthm sbitsetp-when-atom
  (implies (atom x)
           (equal (sbitsetp x) (not x))))

Theorem: sbitsetp-of-cons

(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)))))))

Theorem: sbitset-pairp-of-car

(defthm sbitset-pairp-of-car
  (implies (sbitsetp x)
           (equal (sbitset-pairp (car x))
                  (consp x))))

Theorem: sbitsetp-of-cdr

(defthm sbitsetp-of-cdr
  (implies (sbitsetp x)
           (sbitsetp (cdr x))))

Theorem: sbitset-pairp-when-member-equal-of-sbitsetp

(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)))))