		Search-engine friendly clone of the ACL2 documentation.

Ihs/ash-lemmas

Lemmas about ash from the logops-lemmas book.

Definitions and Theorems

Theorem: ash-0

(defthm ash-0
  (implies (zip i)
           (equal (ash i count) 0)))

Theorem: unsigned-byte-p-ash

(defthm unsigned-byte-p-ash
  (implies (and (unsigned-byte-p size i)
                (integerp count)
                (<= count 0))
           (unsigned-byte-p size (ash i count))))

Theorem: ash-goes-to-0

(defthm ash-goes-to-0
  (implies (and (unsigned-byte-p size i)
                (integerp count)
                (<= count 0)
                (<= size (- count)))
           (equal (ash i count) 0)))