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