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