		Search-engine friendly clone of the ACL2 documentation.

In-of-sbitset-members

Sbitset-find

Helper definition; shouldn't be needed by users.

Signature
(sbitset-find offset x) → *
Arguments: offset — Guard (natp offset).; x — Guard (sbitsetp x).

Definitions and Theorems

Function: sbitset-find

(defun sbitset-find (offset x)
  (declare (xargs :guard (and (natp offset) (sbitsetp x))))
  (let ((__function__ 'sbitset-find))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((equal (sbitset-pair-offset (car x))
                  offset)
           (car x))
          (t (sbitset-find offset (cdr x))))))

Theorem: sbitset-find-when-atom

(defthm sbitset-find-when-atom
  (implies (atom x)
           (equal (sbitset-find offset x) nil)))

Theorem: sbitset-find-of-cons

(defthm sbitset-find-of-cons
  (equal (sbitset-find offset (cons a x))
         (if (equal (sbitset-pair-offset a) offset)
             a
           (sbitset-find offset x))))

Theorem: member-equal-of-sbitset-find

(defthm member-equal-of-sbitset-find
  (implies (sbitset-find offset x)
           (member-equal (sbitset-find offset x)
                         x)))

Theorem: sbitset-pairp-of-sbitset-find

(defthm sbitset-pairp-of-sbitset-find
  (implies (force (sbitsetp x))
           (equal (sbitset-pairp (sbitset-find offset x))
                  (if (sbitset-find offset x) t nil))))

Theorem: sbitset-pair-offset-of-sbitset-find

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

Theorem: natp-when-sbitset-find

(defthm natp-when-sbitset-find
  (implies (and (sbitset-find offset x)
                (sbitsetp x))
           (natp offset))
  :rule-classes (:forward-chaining))