		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-8-u16s

Concatenate 8 16-bit numbers together to form an 128-bit result.

Signature
(merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0) → result
Returns: result — Type (natp result).

Definitions and Theorems

Function: merge-8-u16s

(defun merge-8-u16s (a7 a6 a5 a4 a3 a2 a1 a0)
  (declare (type (unsigned-byte 16)
                 a7 a6 a5 a4 a3 a2 a1 a0))
  (declare (xargs :guard t))
  (let ((__function__ 'merge-8-u16s))
    (declare (ignorable __function__))
    (mbe :logic (logapp* 16 (nfix a0)
                         (nfix a1)
                         (nfix a2)
                         (nfix a3)
                         (nfix a4)
                         (nfix a5)
                         (nfix a6)
                         (nfix a7)
                         0)
         :exec (merge-2-u64s (the (unsigned-byte 64)
                                  (merge-4-u16s a7 a6 a5 a4))
                             (the (unsigned-byte 64)
                                  (merge-4-u16s a3 a2 a1 a0))))))

Theorem: natp-of-merge-8-u16s

(defthm acl2::natp-of-merge-8-u16s
  (b* ((result (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0)))
    (natp result))
  :rule-classes :type-prescription)

Theorem: unsigned-byte-p-128-of-merge-8-u16s

(defthm unsigned-byte-p-128-of-merge-8-u16s
 (unsigned-byte-p 128
                  (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0))
 :rule-classes
 ((:rewrite
      :corollary
      (implies
           (>= (nfix n) 128)
           (unsigned-byte-p n
                            (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0)))
      :hints (("Goal" :in-theory (disable unsigned-byte-p))))))

Theorem: merge-8-u16s-is-merge-unsigneds

(defthm merge-8-u16s-is-merge-unsigneds
  (equal (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0)
         (merge-unsigneds 16
                          (list (nfix a7)
                                (nfix a6)
                                (nfix a5)
                                (nfix a4)
                                (nfix a3)
                                (nfix a2)
                                (nfix a1)
                                (nfix a0)))))

Basic nat-equiv congruences.

Theorem: nat-equiv-implies-equal-merge-8-u16s-8

(defthm nat-equiv-implies-equal-merge-8-u16s-8
  (implies (nat-equiv a0 a0-equiv)
           (equal (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0-equiv)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-8-u16s-7

(defthm nat-equiv-implies-equal-merge-8-u16s-7
  (implies (nat-equiv a1 a1-equiv)
           (equal (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-u16s a7 a6 a5 a4 a3 a2 a1-equiv a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-8-u16s-6

(defthm nat-equiv-implies-equal-merge-8-u16s-6
  (implies (nat-equiv a2 a2-equiv)
           (equal (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-u16s a7 a6 a5 a4 a3 a2-equiv a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-8-u16s-5

(defthm nat-equiv-implies-equal-merge-8-u16s-5
  (implies (nat-equiv a3 a3-equiv)
           (equal (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-u16s a7 a6 a5 a4 a3-equiv a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-8-u16s-4

(defthm nat-equiv-implies-equal-merge-8-u16s-4
  (implies (nat-equiv a4 a4-equiv)
           (equal (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-u16s a7 a6 a5 a4-equiv a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-8-u16s-3

(defthm nat-equiv-implies-equal-merge-8-u16s-3
  (implies (nat-equiv a5 a5-equiv)
           (equal (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-u16s a7 a6 a5-equiv a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-8-u16s-2

(defthm nat-equiv-implies-equal-merge-8-u16s-2
  (implies (nat-equiv a6 a6-equiv)
           (equal (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-u16s a7 a6-equiv a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-8-u16s-1

(defthm nat-equiv-implies-equal-merge-8-u16s-1
  (implies (nat-equiv a7 a7-equiv)
           (equal (merge-8-u16s a7 a6 a5 a4 a3 a2 a1 a0)
                  (merge-8-u16s a7-equiv a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))