		Search-engine friendly clone of the ACL2 documentation.

Logext

Logext-basics

Definitions and Theorems

Theorem: logext-bounds

(defthm logext-bounds
  (implies (< 0 size)
           (and (>= (logext size i)
                    (- (expt 2 (1- size))))
                (< (logext size i) (expt 2 (1- size)))))
  :rule-classes ((:linear :trigger-terms ((logext size i)))
                 (:rewrite)))

Theorem: signed-byte-p-logext

(defthm signed-byte-p-logext
  (implies (and (>= size1 size)
                (> size 0)
                (integerp size1)
                (integerp size))
           (signed-byte-p size1 (logext size i))))