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