		Search-engine friendly clone of the ACL2 documentation.

Signed-byte-p*

Recursive definition of signed-byte-p.

Definitions and Theorems

Theorem: signed-byte-p*

(defthm signed-byte-p*
  (equal (signed-byte-p size i)
         (and (integerp size)
              (> size 0)
              (integerp i)
              (or (equal i 0)
                  (equal i -1)
                  (signed-byte-p (1- size) (logcdr i)))))
  :rule-classes
  ((:definition :clique (signed-byte-p)
                :controller-alist ((signed-byte-p t t)))))