		Search-engine friendly clone of the ACL2 documentation.

Signed-byte-p-logops

Lemmas showing the basic preservation of signed-byte-p by operations like logand, logior, etc.

Definitions and Theorems

Theorem: signed-byte-p-logops

(defthm signed-byte-p-logops
  (and (implies (signed-byte-p size i)
                (signed-byte-p size (lognot i)))
       (implies (and (signed-byte-p size i)
                     (signed-byte-p size j))
                (and (signed-byte-p size (logior i j))
                     (signed-byte-p size (logxor i j))
                     (signed-byte-p size (logand i j))
                     (signed-byte-p size (logeqv i j))
                     (signed-byte-p size (lognand i j))
                     (signed-byte-p size (lognor i j))
                     (signed-byte-p size (logandc1 i j))
                     (signed-byte-p size (logandc2 i j))
                     (signed-byte-p size (logorc1 i j))
                     (signed-byte-p size (logorc2 i j))))))