		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-unsigneds

Concatenate the given list of integers together at the given width, most-significant first, to form a single natural number.

Signature
(merge-unsigneds width elts) → packed
Arguments: width — Guard (natp width).; elts — Guard (integer-listp elts).
Returns: packed — Type (natp packed).

Definitions and Theorems

Function: merge-unsigneds

(defun merge-unsigneds (width elts)
  (declare (xargs :guard (and (natp width)
                              (integer-listp elts))))
  (let ((__function__ 'merge-unsigneds))
    (declare (ignorable __function__))
    (merge-unsigneds-aux width elts 0)))

Theorem: natp-of-merge-unsigneds

(defthm natp-of-merge-unsigneds
  (b* ((packed (merge-unsigneds width elts)))
    (natp packed))
  :rule-classes :type-prescription)

Theorem: width-of-merge-unsigneds

(defthm width-of-merge-unsigneds
  (b* ((?packed (merge-unsigneds width elts)))
    (implies (and (<= (* (nfix width) (len elts)) n)
                  (natp n))
             (unsigned-byte-p n packed))))

Theorem: merge-unsigneds-alt-def

(defthm merge-unsigneds-alt-def
  (equal (merge-unsigneds width elts)
         (if (atom elts)
             0
           (logapp (* (nfix width) (len (cdr elts)))
                   (merge-unsigneds width (cdr elts))
                   (loghead width (car elts)))))
  :rule-classes
  ((:definition :controller-alist ((merge-unsigneds nil t)))))