		Search-engine friendly clone of the ACL2 documentation.

Signed-byte-listp

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

BOZO consider switching this book to use deflist.

Definitions and Theorems

Function: signed-byte-listp

(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: signed-byte-listp-when-atom

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

Theorem: signed-byte-listp-of-cons

(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: true-listp-when-signed-byte-listp

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

Subtopics

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