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

BOZO consider switching this book to use deflist.

**Function: **

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

**Theorem: **

(defthm unsigned-byte-listp-when-not-consp (implies (not (consp x)) (equal (unsigned-byte-listp n x) (not x))))

**Theorem: **

(defthm unsigned-byte-listp-of-cons (equal (unsigned-byte-listp n (cons a x)) (and (unsigned-byte-p n a) (unsigned-byte-listp n x))))

**Theorem: **

(defthm unsigned-byte-p-of-car-when-unsigned-byte-listp (implies (unsigned-byte-listp width x) (equal (unsigned-byte-p width (car x)) (consp x))) :rule-classes (:rewrite :forward-chaining))

**Theorem: **

(defthm nat-listp-when-unsigned-byte-listp (implies (unsigned-byte-listp width x) (nat-listp x)))

**Theorem: **

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

**Theorem: **

(defthm unsigned-byte-listp-of-append (equal (unsigned-byte-listp width (append x y)) (and (unsigned-byte-listp width (list-fix x)) (unsigned-byte-listp width y))))

**Theorem: **

(defthm unsigned-byte-listp-of-list-fix-when-unsigned-byte-listp (implies (unsigned-byte-listp width x) (unsigned-byte-listp width (list-fix x))))

**Theorem: **

(defthm unsigned-byte-listp-of-repeat (equal (unsigned-byte-listp width (repeat n x)) (or (zp n) (unsigned-byte-p width x))))

**Theorem: **

(defthm unsigned-byte-listp-of-take (implies (unsigned-byte-listp width x) (equal (unsigned-byte-listp width (take n x)) (or (zp n) (<= n (len x))))))

**Theorem: **

(defthm unsigned-byte-listp-of-take-past-length (implies (and (natp k) (< (len x) k)) (not (unsigned-byte-listp width (take k x)))))

**Theorem: **

(defthm unsigned-byte-listp-of-nthcdr (implies (unsigned-byte-listp width x) (unsigned-byte-listp width (nthcdr n x))))

**Theorem: **

(defthm unsigned-byte-listp-when-take-and-nthcdr (implies (and (unsigned-byte-listp width (take n x)) (unsigned-byte-listp width (nthcdr n x))) (unsigned-byte-listp width x)))

**Theorem: **

(defthm unsigned-byte-listp-of-update-nth (implies (and (unsigned-byte-listp n l) (< key (len l))) (equal (unsigned-byte-listp n (update-nth key val l)) (unsigned-byte-p n val))))

**Theorem: **

(defthm unsigned-byte-listp-of-rev (equal (unsigned-byte-listp n (rev bytes)) (unsigned-byte-listp n (list-fix bytes))))

**Theorem: **

(defthm unsigned-byte-p-of-nth-when-unsigned-byte-listp (implies (unsigned-byte-listp bits l) (iff (unsigned-byte-p bits (nth n l)) (< (nfix n) (len l)))))

**Theorem: **

(defthm unsigned-byte-listp-of-make-list-ac (equal (unsigned-byte-listp n1 (make-list-ac n2 val ac)) (and (unsigned-byte-listp n1 ac) (or (zp n2) (unsigned-byte-p n1 val)))))

**Theorem: **

(defthm unsigned-byte-listp-of-revappend (equal (unsigned-byte-listp width (revappend x y)) (and (unsigned-byte-listp width (list-fix x)) (unsigned-byte-listp width y))))

- Defbytelist
- Introduce a
fixtype of true lists of unsigned or signed bytes of a specified size. - Unsigned-byte-list-fix
- Fixing function for
`unsigned-byte-listp`.