		Search-engine friendly clone of the ACL2 documentation.

Signed-byte-list-fix

Fixing function for signed-byte-listp.

Signature
(signed-byte-list-fix bits x) → fixed-x
Arguments: bits — Guard (posp bits).; x — Guard (signed-byte-listp bits x).
Returns: fixed-x — Type (signed-byte-listp bits fixed-x), given (posp bits).

This lifts signed-byte-fix to lists. See that function for more information, in particular about the fixing of bits to a positive integer.

Definitions and Theorems

Function: signed-byte-list-fix

(defun
 signed-byte-list-fix (bits x)
 (declare (xargs :guard (and (posp bits)
                             (signed-byte-listp bits x))))
 (let
   ((__function__ 'signed-byte-list-fix))
   (declare (ignorable __function__))
   (mbe :logic (cond ((atom x) nil)
                     (t (cons (signed-byte-fix bits (car x))
                              (signed-byte-list-fix bits (cdr x)))))
        :exec x)))

Theorem: return-type-of-signed-byte-list-fix

(defthm return-type-of-signed-byte-list-fix
        (implies (posp bits)
                 (b* ((fixed-x (signed-byte-list-fix bits x)))
                     (signed-byte-listp bits fixed-x)))
        :rule-classes :rewrite)

Theorem: integer-listp-of-signed-byte-list-fix

(defthm integer-listp-of-signed-byte-list-fix
        (b* ((fixed-x (signed-byte-list-fix bits x)))
            (integer-listp fixed-x))
        :rule-classes :rewrite)

Theorem: signed-byte-list-fix-when-signed-byte-listp

(defthm signed-byte-list-fix-when-signed-byte-listp
        (implies (signed-byte-listp (pos-fix bits) x)
                 (equal (signed-byte-list-fix bits x)
                        x)))

Theorem: signed-byte-list-fix-of-nil

(defthm signed-byte-list-fix-of-nil
        (equal (signed-byte-list-fix bits nil)
               nil))

Theorem: signed-byte-list-fix-of-cons

(defthm signed-byte-list-fix-of-cons
        (equal (signed-byte-list-fix bits (cons x y))
               (cons (signed-byte-fix bits x)
                     (signed-byte-list-fix bits y))))

Theorem: signed-byte-list-fix-of-append

(defthm signed-byte-list-fix-of-append
        (equal (signed-byte-list-fix bits (append x y))
               (append (signed-byte-list-fix bits x)
                       (signed-byte-list-fix bits y))))

Theorem: len-of-signed-byte-list-fix

(defthm len-of-signed-byte-list-fix
        (equal (len (signed-byte-list-fix bits x))
               (len x)))

Theorem: consp-of-signed-byte-list-fix

(defthm consp-of-signed-byte-list-fix
        (equal (consp (signed-byte-list-fix bits x))
               (consp x)))

Theorem: car-of-signed-byte-list-fix

(defthm car-of-signed-byte-list-fix
        (implies (consp x)
                 (equal (car (signed-byte-list-fix bits x))
                        (signed-byte-fix bits (car x)))))

Theorem: cdr-of-signed-byte-list-fix

(defthm cdr-of-signed-byte-list-fix
        (implies (consp x)
                 (equal (cdr (signed-byte-list-fix bits x))
                        (signed-byte-list-fix bits (cdr x)))))

Theorem: rev-of-signed-byte-list-fix

(defthm rev-of-signed-byte-list-fix
        (equal (rev (signed-byte-list-fix bits x))
               (signed-byte-list-fix bits (rev x))))