• 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

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