Helper definition; shouldn't be needed by users.
Function:
(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:
(defthm sbitset-find-when-atom (implies (atom x) (equal (sbitset-find offset x) nil)))
Theorem:
(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:
(defthm member-equal-of-sbitset-find (implies (sbitset-find offset x) (member-equal (sbitset-find offset x) x)))
Theorem:
(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:
(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:
(defthm natp-when-sbitset-find (implies (and (sbitset-find offset x) (sbitsetp x)) (natp offset)) :rule-classes (:forward-chaining))