Recursive definition of unsigned-byte-p.
Theorem:
(defthm unsigned-byte-p* (implies (and (integerp size) (> size 0)) (equal (unsigned-byte-p size i) (and (integerp size) (>= size 0) (integerp i) (>= i 0) (unsigned-byte-p (1- size) (logcdr i))))) :rule-classes ((:definition :clique (unsigned-byte-p) :controller-alist ((unsigned-byte-p t t)))))