		Search-engine friendly clone of the ACL2 documentation.

Unsigned-byte-list-fix

Fixing function for unsigned-byte-listp.

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

This lifts unsigned-byte-fix to lists. See that function for more information, in particular about the fixing of bits to a natural number.

Definitions and Theorems

Function: unsigned-byte-list-fix

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

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

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

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

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

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

(defthm unsigned-byte-list-fix-when-unsigned-byte-listp
  (implies (unsigned-byte-listp (nfix bits) x)
           (equal (unsigned-byte-list-fix bits x)
                  x)))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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