		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.