		Search-engine friendly clone of the ACL2 documentation.

Ihs/signed-byte-p-lemmas

Lemmas about signed-byte-p from the logops-lemmas book.

Definitions and Theorems

Theorem: signed-byte-p-base-cases

(defthm signed-byte-p-base-cases
  (and (equal (signed-byte-p size 0)
              (and (integerp size) (< 0 size)))
       (equal (signed-byte-p size -1)
              (and (integerp size) (< 0 size)))))

Theorem: backchain-signed-byte-p-to-unsigned-byte-p

(defthm backchain-signed-byte-p-to-unsigned-byte-p
  (implies (and (syntaxp (constant-syntaxp size))
                (< 0 size)
                (unsigned-byte-p (1- size) i))
           (signed-byte-p size i)))