		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-8-u4s

Concatenate 8 nibbles together to form an 32-bit result.

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

Definitions and Theorems

Function: merge-8-u4s$inline

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

Theorem: natp-of-merge-8-u4s

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

Theorem: unsigned-byte-p-32-of-merge-8-u4s

(defthm unsigned-byte-p-32-of-merge-8-u4s
        (unsigned-byte-p 32
                         (merge-8-u4s a7 a6 a5 a4 a3 a2 a1 a0)))

Theorem: merge-8-u4s-is-merge-unsigneds

(defthm merge-8-u4s-is-merge-unsigneds
        (equal (merge-8-u4s a7 a6 a5 a4 a3 a2 a1 a0)
               (merge-unsigneds 4
                                (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-u4s-8

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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