`(bits-between n m x)` returns a proper, ordered set of all

This is a key function in the definition of bitset-members.

**Function: **

(defun bits-between (n m x) (declare (xargs :guard (and (natp n) (natp m) (integerp x)))) (declare (xargs :guard (<= n m))) (let ((__function__ 'bits-between)) (declare (ignorable __function__)) (let* ((n (lnfix n)) (m (lnfix m))) (cond ((mbe :logic (zp (- m n)) :exec (= m n)) nil) ((logbitp n x) (cons n (bits-between (+ n 1) m x))) (t (bits-between (+ n 1) m x))))))

**Theorem: **

(defthm true-listp-of-bits-between (true-listp (bits-between n m x)) :rule-classes :type-prescription)

**Theorem: **

(defthm integer-listp-of-bits-between (integer-listp (bits-between n m x)))

**Theorem: **

(defthm nat-listp-of-bits-between (nat-listp (bits-between n m x)))

**Theorem: **

(defthm bits-between-when-not-integer (implies (not (integerp x)) (equal (bits-between n m x) nil)))

**Theorem: **

(defthm member-equal-of-bits-between (iff (member-equal a (bits-between n m x)) (and (natp a) (<= (nfix n) a) (< a (nfix m)) (logbitp a x))))

**Theorem: **

(defthm no-duplicatesp-equal-of-bits-between (no-duplicatesp-equal (bits-between n m x)))

**Theorem: **

(defthm bits-between-of-increment-right-index (implies (and (force (natp n)) (force (natp m)) (force (<= n m))) (equal (bits-between n (+ 1 m) x) (if (logbitp m x) (append (bits-between n m x) (list m)) (bits-between n m x)))))

**Theorem: **

(defthm merge-appended-bits-between (implies (and (natp n) (natp m) (natp k) (<= n m) (<= m k)) (equal (append (bits-between n m x) (bits-between m k x)) (bits-between n k x))))

**Theorem: **

(defthm bits-between-of-right-shift (implies (and (natp n) (natp m) (<= n m) (integerp k) (< k 0)) (equal (bits-between n m (ash x k)) (add-to-each k (bits-between (- n k) (- m k) x)))))

**Theorem: **

(defthm bits-between-of-mod-2^n (implies (and (integerp x) (natp k) (<= m k)) (equal (bits-between n m (mod x (expt 2 k))) (bits-between n m x))))

**Theorem: **

(defthm bits-between-of-mod-2^32 (implies (and (integerp x) (<= m 32)) (equal (bits-between n m (mod x 4294967296)) (bits-between n m x))))

**Theorem: **

(defthm bits-between-upper (implies (and (syntaxp (not (equal m (cons 'integer-length (cons x 'nil))))) (natp n) (natp m) (natp x) (<= (integer-length x) m)) (equal (bits-between n m x) (bits-between n (integer-length x) x))))

**Theorem: **

(defthm setp-of-bits-between (setp (bits-between n m x)))

**Theorem: **

(defthm in-of-bits-between (equal (in a (bits-between n m x)) (and (natp a) (<= (nfix n) a) (< a (nfix m)) (logbitp a x))))