Recursive definition of signed-byte-p.
Theorem:
(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)))))