		Search-engine friendly clone of the ACL2 documentation.

Loghead

Loghead-basics

Definitions and Theorems

Theorem: unsigned-byte-p-loghead

(defthm unsigned-byte-p-loghead
  (implies (and (>= size1 size)
                (integerp size)
                (>= size 0)
                (integerp size1))
           (unsigned-byte-p size1 (loghead size i))))

Theorem: loghead-upper-bound

(defthm loghead-upper-bound
  (< (loghead size i) (expt 2 size))
  :rule-classes (:linear :rewrite))