Recognizer for lists of signed-byte-p's.
BOZO consider switching this book to use deflist.
(defun signed-byte-listp (n x) (if (atom x) (null x) (and (signed-byte-p n (car x)) (signed-byte-listp n (cdr x)))))
(defthm signed-byte-listp-when-atom (implies (atom x) (equal (signed-byte-listp n x) (not x))))
(defthm signed-byte-listp-of-cons (equal (signed-byte-listp n (cons a x)) (and (signed-byte-p n a) (signed-byte-listp n x))))
(defthm true-listp-when-signed-byte-listp (implies (signed-byte-listp width x) (true-listp x)))