		Search-engine friendly clone of the ACL2 documentation.

Linear-memory

Combine-n-bytes

Signature
(combine-n-bytes low num bytes) → *
Arguments: low — Index of the first byte.
Guard (natp low).; num — Number of bytes to combine, starting at pos.
Guard (natp num).; bytes — LSB first.
Guard (byte-listp bytes).

Definitions and Theorems

Function: combine-n-bytes

(defun combine-n-bytes (low num bytes)
  (declare (xargs :guard (and (natp low)
                              (natp num)
                              (byte-listp bytes))))
  (declare (xargs :guard (<= (+ low num) (len bytes))))
  (let ((__function__ 'combine-n-bytes))
    (declare (ignorable __function__))
    (if (mbt (and (<= (+ low num) (len bytes))
                  (byte-listp bytes)
                  (natp low)
                  (natp num)))
        (combine-bytes (take num (nthcdr low bytes)))
      0)))

Theorem: combine-bytes-and-take-degenerate-case-1

(defthm combine-bytes-and-take-degenerate-case-1
  (implies (zp n)
           (equal (combine-bytes (take n bytes))
                  0)))

Theorem: combine-bytes-and-take-degenerate-case-2

(defthm combine-bytes-and-take-degenerate-case-2
  (equal (combine-bytes (take n nil)) 0))

Theorem: natp-of-combine-bytes-of-take

(defthm natp-of-combine-bytes-of-take
  (implies (byte-listp bytes)
           (<= 0 (combine-bytes (take num bytes)))))

Theorem: natp-combine-n-bytes

(defthm natp-combine-n-bytes
 (implies (force (byte-listp bytes))
          (natp (combine-n-bytes low num bytes)))
 :rule-classes
 ((:type-prescription)
  (:linear
      :corollary (implies (byte-listp bytes)
                          (<= 0 (combine-n-bytes low num bytes))))))

Theorem: unsigned-byte-p-of-combine-n-bytes

(defthm unsigned-byte-p-of-combine-n-bytes
  (implies (and (equal n (ash num 3)) (natp num))
           (unsigned-byte-p n (combine-n-bytes low num bytes))))

Theorem: size-of-combine-n-bytes

(defthm size-of-combine-n-bytes
  (< (combine-n-bytes low num bytes)
     (expt 2 (ash num 3)))
  :rule-classes :linear)