		Search-engine friendly clone of the ACL2 documentation.

Logbitp-bounds

Lemmas about inferring logbitp information from bounds expressed using expt and vice versa

(logbitp n x) => (<= (expt 2 n) x)
(logbitp n (expt 2 n)) = t
(<= (expt 2 n) x) and (< x (expt 2 (1+ n))) => (logbitp n x) and (not (logbitp (1+ n) x))

Definitions and Theorems

Theorem: logbitp-to-lower-bound

(defthm logbitp-to-lower-bound
        (implies (and (logbitp n x) (natp n) (natp x))
                 (<= (expt 2 n) x))
        :rule-classes (:linear :rewrite))

Theorem: expt-2-n-to-logbitp

(defthm expt-2-n-to-logbitp
        (implies (natp n)
                 (logbitp n (expt 2 n))))

Theorem: bounds-to-logbitp-lemma

(defthm bounds-to-logbitp-lemma
        (implies (and (< (expt 2 n) x)
                      (< x (expt 2 (+ 1 n)))
                      (natp n)
                      (natp x))
                 (logbitp n x)))

Theorem: bounds-to-logbitp

(defthm bounds-to-logbitp
        (implies (and (<= (expt 2 n) x)
                      (< x (expt 2 (+ 1 n)))
                      (natp n)
                      (natp x))
                 (and (logbitp n x)
                      (not (logbitp (+ 1 n) x)))))