Recognizer for lists of signed-byte-p's.

BOZO consider switching this book to use deflist.

**Function: **

(defun signed-byte-listp (n x) (if (atom x) (null x) (and (signed-byte-p n (car x)) (signed-byte-listp n (cdr x)))))

**Theorem: **

(defthm signed-byte-listp-when-atom (implies (atom x) (equal (signed-byte-listp n x) (not x))))

**Theorem: **

(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))))

**Theorem: **

(defthm true-listp-when-signed-byte-listp (implies (signed-byte-listp width x) (true-listp x)))

- Signed-byte-list-fix
- Fixing function for
`signed-byte-listp`.