		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-16-u4s

Concatenate 16 nibbles together to form an 64-bit result.

Signature
(merge-16-u4s a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) → result
Returns: result — Type (natp result).

Definitions and Theorems

Function: merge-16-u4s

(defun merge-16-u4s (a15 a14 a13 a12
                         a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
 (declare (type (unsigned-byte 4)
                a15 a14 a13 a12
                a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))
 (declare (xargs :guard t))
 (let ((__function__ 'merge-16-u4s))
  (declare (ignorable __function__))
  (mbe
     :logic (logapp* 4 (nfix a0)
                     (nfix a1)
                     (nfix a2)
                     (nfix a3)
                     (nfix a4)
                     (nfix a5)
                     (nfix a6)
                     (nfix a7)
                     (nfix a8)
                     (nfix a9)
                     (nfix a10)
                     (nfix a11)
                     (nfix a12)
                     (nfix a13)
                     (nfix a14)
                     (nfix a15)
                     0)
     :exec
     (merge-2-u32s (the (unsigned-byte 32)
                        (merge-8-u4s a15 a14 a13 a12 a11 a10 a9 a8))
                   (the (unsigned-byte 32)
                        (merge-8-u4s a7 a6 a5 a4 a3 a2 a1 a0))))))

Theorem: natp-of-merge-16-u4s

(defthm acl2::natp-of-merge-16-u4s
 (b* ((result (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
   (natp result))
 :rule-classes :type-prescription)

Theorem: unsigned-byte-p-64-of-merge-16-u4s

(defthm unsigned-byte-p-64-of-merge-16-u4s
 (unsigned-byte-p
      64
      (merge-16-u4s a15 a14 a13 a12
                    a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))
 :rule-classes
 ((:rewrite
    :corollary
    (implies
         (>= (nfix n) 64)
         (unsigned-byte-p
              n
              (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
    :hints (("Goal" :in-theory (disable unsigned-byte-p))))))

Theorem: merge-16-u4s-is-merge-unsigneds

(defthm merge-16-u4s-is-merge-unsigneds
  (equal (merge-16-u4s a15 a14 a13 a12
                       a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
         (merge-unsigneds 4
                          (list (nfix a15)
                                (nfix a14)
                                (nfix a13)
                                (nfix a12)
                                (nfix a11)
                                (nfix a10)
                                (nfix a9)
                                (nfix a8)
                                (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-16-u4s-16

(defthm nat-equiv-implies-equal-merge-16-u4s-16
  (implies
       (nat-equiv a0 a0-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11 a10
                            a9 a8 a7 a6 a5 a4 a3 a2 a1 a0-equiv)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-15

(defthm nat-equiv-implies-equal-merge-16-u4s-15
  (implies
       (nat-equiv a1 a1-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11 a10
                            a9 a8 a7 a6 a5 a4 a3 a2 a1-equiv a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-14

(defthm nat-equiv-implies-equal-merge-16-u4s-14
  (implies
       (nat-equiv a2 a2-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11 a10
                            a9 a8 a7 a6 a5 a4 a3 a2-equiv a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-13

(defthm nat-equiv-implies-equal-merge-16-u4s-13
  (implies
       (nat-equiv a3 a3-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11 a10
                            a9 a8 a7 a6 a5 a4 a3-equiv a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-12

(defthm nat-equiv-implies-equal-merge-16-u4s-12
  (implies
       (nat-equiv a4 a4-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11 a10
                            a9 a8 a7 a6 a5 a4-equiv a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-11

(defthm nat-equiv-implies-equal-merge-16-u4s-11
  (implies
       (nat-equiv a5 a5-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11 a10
                            a9 a8 a7 a6 a5-equiv a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-10

(defthm nat-equiv-implies-equal-merge-16-u4s-10
  (implies
       (nat-equiv a6 a6-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11 a10
                            a9 a8 a7 a6-equiv a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-9

(defthm nat-equiv-implies-equal-merge-16-u4s-9
  (implies
       (nat-equiv a7 a7-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11 a10
                            a9 a8 a7-equiv a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-8

(defthm nat-equiv-implies-equal-merge-16-u4s-8
  (implies
       (nat-equiv a8 a8-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11 a10
                            a9 a8-equiv a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-7

(defthm nat-equiv-implies-equal-merge-16-u4s-7
  (implies
       (nat-equiv a9 a9-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11 a10
                            a9-equiv a8 a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-6

(defthm nat-equiv-implies-equal-merge-16-u4s-6
  (implies
       (nat-equiv a10 a10-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11 a10-equiv
                            a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-5

(defthm nat-equiv-implies-equal-merge-16-u4s-5
  (implies
       (nat-equiv a11 a11-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12 a11-equiv
                            a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-4

(defthm nat-equiv-implies-equal-merge-16-u4s-4
  (implies
       (nat-equiv a12 a12-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13 a12-equiv
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-3

(defthm nat-equiv-implies-equal-merge-16-u4s-3
  (implies
       (nat-equiv a13 a13-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14 a13-equiv a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-2

(defthm nat-equiv-implies-equal-merge-16-u4s-2
  (implies
       (nat-equiv a14 a14-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15 a14-equiv a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: nat-equiv-implies-equal-merge-16-u4s-1

(defthm nat-equiv-implies-equal-merge-16-u4s-1
  (implies
       (nat-equiv a15 a15-equiv)
       (equal (merge-16-u4s a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-u4s a15-equiv a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))