		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-unsigneds-aux

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

Definitions and Theorems

Function: merge-unsigneds-aux

(defun merge-unsigneds-aux (width elts acc)
       (declare (xargs :guard (and (natp width)
                                   (integer-listp elts)
                                   (natp acc))))
       (let ((__function__ 'merge-unsigneds-aux))
            (declare (ignorable __function__))
            (if (atom elts)
                (lnfix acc)
                (merge-unsigneds-aux width (cdr elts)
                                     (logapp width (car elts)
                                             (lnfix acc))))))

Theorem: natp-of-merge-unsigneds-aux

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

Theorem: width-of-merge-unsigneds-aux

(defthm width-of-merge-unsigneds-aux
        (b* ((?packed (merge-unsigneds-aux width elts acc)))
            (unsigned-byte-p (+ (integer-length (nfix acc))
                                (* (nfix width) (len elts)))
                             packed)))

Theorem: merge-unsigneds-aux-of-nil

(defthm merge-unsigneds-aux-of-nil
        (equal (merge-unsigneds-aux width nil acc)
               (nfix acc)))

Theorem: merge-unsigneds-aux-of-cons

(defthm
  merge-unsigneds-aux-of-cons
  (equal (merge-unsigneds-aux width (cons a b)
                              acc)
         (merge-unsigneds-aux width b (logapp width a (nfix acc)))))