		Search-engine friendly clone of the ACL2 documentation.

Ihs/integer-length-lemmas

Lemmas about integer-length from the logops-lemmas book.

Definitions and Theorems

Theorem: equal-integer-length-0

(defthm equal-integer-length-0
  (equal (equal (integer-length i) 0)
         (or (zip i) (equal i -1))))

Theorem: unsigned-byte-p-integer-length

(defthm unsigned-byte-p-integer-length
  (implies (and (integerp i)
                (>= i 0)
                (equal size (integer-length i)))
           (unsigned-byte-p size i))
  :rule-classes nil)

Theorem: integer-length-unsigned-byte

(defthm integer-length-unsigned-byte
  (implies (unsigned-byte-p size i)
           (<= (integer-length i) size))
  :rule-classes nil)

Theorem: signed-byte-p-integer-length

(defthm signed-byte-p-integer-length
  (implies (and (integerp i)
                (integerp size)
                (> size 0)
                (equal size (+ (integer-length i) 1)))
           (signed-byte-p size i))
  :rule-classes nil)

Theorem: integer-length-signed-byte

(defthm integer-length-signed-byte
  (implies (signed-byte-p size i)
           (<= (+ (integer-length i) 1) size))
  :rule-classes nil)