		Search-engine friendly clone of the ACL2 documentation.

Logsat

Logsat-basics

Definitions and Theorems

Theorem: logsat-bounds

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

Theorem: signed-byte-p-logsat

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