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