		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-32-bits

Concatenate 32 bits together to form an 32-bit natural.

Signature
(merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) → result
Arguments: a31 — Guard (bitp a31).; a30 — Guard (bitp a30).; a29 — Guard (bitp a29).; a28 — Guard (bitp a28).; a27 — Guard (bitp a27).; a26 — Guard (bitp a26).; a25 — Guard (bitp a25).; a24 — Guard (bitp a24).; a23 — Guard (bitp a23).; a22 — Guard (bitp a22).; a21 — Guard (bitp a21).; a20 — Guard (bitp a20).; a19 — Guard (bitp a19).; a18 — Guard (bitp a18).; a17 — Guard (bitp a17).; a16 — Guard (bitp a16).; a15 — Guard (bitp a15).; a14 — Guard (bitp a14).; a13 — Guard (bitp a13).; a12 — Guard (bitp a12).; a11 — Guard (bitp a11).; a10 — Guard (bitp a10).; a9 — Guard (bitp a9).; a8 — Guard (bitp a8).; a7 — Guard (bitp a7).; a6 — Guard (bitp a6).; a5 — Guard (bitp a5).; a4 — Guard (bitp a4).; a3 — Guard (bitp a3).; a2 — Guard (bitp a2).; a1 — Guard (bitp a1).; a0 — Guard (bitp a0).
Returns: result — Type (natp result).

Definitions and Theorems

Function: merge-32-bits$inline

(defun acl2::merge-32-bits$inline
       (a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
 (declare (xargs :guard (and (bitp a31)
                             (bitp a30)
                             (bitp a29)
                             (bitp a28)
                             (bitp a27)
                             (bitp a26)
                             (bitp a25)
                             (bitp a24)
                             (bitp a23)
                             (bitp a22)
                             (bitp a21)
                             (bitp a20)
                             (bitp a19)
                             (bitp a18)
                             (bitp a17)
                             (bitp a16)
                             (bitp a15)
                             (bitp a14)
                             (bitp a13)
                             (bitp a12)
                             (bitp a11)
                             (bitp a10)
                             (bitp a9)
                             (bitp a8)
                             (bitp a7)
                             (bitp a6)
                             (bitp a5)
                             (bitp a4)
                             (bitp a3)
                             (bitp a2)
                             (bitp a1)
                             (bitp a0))))
 (declare (type bit
                a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))
 (declare (xargs :split-types t))
 (let ((__function__ 'merge-32-bits))
   (declare (ignorable __function__))
   (mbe :logic
        (logapp* 1 (bfix a0)
                 (bfix a1)
                 (bfix a2)
                 (bfix a3)
                 (bfix a4)
                 (bfix a5)
                 (bfix a6)
                 (bfix a7)
                 (bfix a8)
                 (bfix a9)
                 (bfix a10)
                 (bfix a11)
                 (bfix a12)
                 (bfix a13)
                 (bfix a14)
                 (bfix a15)
                 (bfix a16)
                 (bfix a17)
                 (bfix a18)
                 (bfix a19)
                 (bfix a20)
                 (bfix a21)
                 (bfix a22)
                 (bfix a23)
                 (bfix a24)
                 (bfix a25)
                 (bfix a26)
                 (bfix a27)
                 (bfix a28)
                 (bfix a29)
                 (bfix a30)
                 (bfix a31)
                 0)
        :exec
        (b* ((ans a0)
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a1 1))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a2 2))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a3 3))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a4 4))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a5 5))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a6 6))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a7 7))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a8 8))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a9 9))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a10 10))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a11 11))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a12 12))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a13 13))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a14 14))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a15 15))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a16 16))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a17 17))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a18 18))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a19 19))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a20 20))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a21 21))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a22 22))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a23 23))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a24 24))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a25 25))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a26 26))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a27 27))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a28 28))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a29 29))
                               (the (unsigned-byte 32) ans))))
             (ans (the (unsigned-byte 32)
                       (logior (the (unsigned-byte 32) (ash a30 30))
                               (the (unsigned-byte 32) ans)))))
          (the (unsigned-byte 32)
               (logior (the (unsigned-byte 32) (ash a31 31))
                       (the (unsigned-byte 32) ans)))))))

Theorem: natp-of-merge-32-bits

(defthm acl2::natp-of-merge-32-bits
  (b* ((result (acl2::merge-32-bits$inline
                    a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                    a21 a20 a19 a18 a17 a16 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-32-of-merge-32-bits

(defthm unsigned-byte-p-32-of-merge-32-bits
  (unsigned-byte-p
       32
       (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                      a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                      a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))

Theorem: merge-32-bits-is-merge-unsigneds

(defthm merge-32-bits-is-merge-unsigneds
  (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                        a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                        a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
         (merge-unsigneds 1
                          (list (bfix a31)
                                (bfix a30)
                                (bfix a29)
                                (bfix a28)
                                (bfix a27)
                                (bfix a26)
                                (bfix a25)
                                (bfix a24)
                                (bfix a23)
                                (bfix a22)
                                (bfix a21)
                                (bfix a20)
                                (bfix a19)
                                (bfix a18)
                                (bfix a17)
                                (bfix a16)
                                (bfix a15)
                                (bfix a14)
                                (bfix a13)
                                (bfix a12)
                                (bfix a11)
                                (bfix a10)
                                (bfix a9)
                                (bfix a8)
                                (bfix a7)
                                (bfix a6)
                                (bfix a5)
                                (bfix a4)
                                (bfix a3)
                                (bfix a2)
                                (bfix a1)
                                (bfix a0)))))

Basic bit-equiv congruences.

Theorem: bit-equiv-implies-equal-merge-32-bits-32

(defthm bit-equiv-implies-equal-merge-32-bits-32
  (implies
       (bit-equiv a0 a0-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30
                             a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                             a19 a18 a17 a16 a15 a14 a13 a12 a11 a10
                             a9 a8 a7 a6 a5 a4 a3 a2 a1 a0-equiv)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-31

(defthm bit-equiv-implies-equal-merge-32-bits-31
  (implies
       (bit-equiv a1 a1-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30
                             a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                             a19 a18 a17 a16 a15 a14 a13 a12 a11 a10
                             a9 a8 a7 a6 a5 a4 a3 a2 a1-equiv a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-30

(defthm bit-equiv-implies-equal-merge-32-bits-30
  (implies
       (bit-equiv a2 a2-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30
                             a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                             a19 a18 a17 a16 a15 a14 a13 a12 a11 a10
                             a9 a8 a7 a6 a5 a4 a3 a2-equiv a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-29

(defthm bit-equiv-implies-equal-merge-32-bits-29
  (implies
       (bit-equiv a3 a3-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30
                             a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                             a19 a18 a17 a16 a15 a14 a13 a12 a11 a10
                             a9 a8 a7 a6 a5 a4 a3-equiv a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-28

(defthm bit-equiv-implies-equal-merge-32-bits-28
  (implies
       (bit-equiv a4 a4-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30
                             a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                             a19 a18 a17 a16 a15 a14 a13 a12 a11 a10
                             a9 a8 a7 a6 a5 a4-equiv a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-27

(defthm bit-equiv-implies-equal-merge-32-bits-27
  (implies
       (bit-equiv a5 a5-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30
                             a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                             a19 a18 a17 a16 a15 a14 a13 a12 a11 a10
                             a9 a8 a7 a6 a5-equiv a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-26

(defthm bit-equiv-implies-equal-merge-32-bits-26
  (implies
       (bit-equiv a6 a6-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30
                             a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                             a19 a18 a17 a16 a15 a14 a13 a12 a11 a10
                             a9 a8 a7 a6-equiv a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-25

(defthm bit-equiv-implies-equal-merge-32-bits-25
  (implies
       (bit-equiv a7 a7-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30
                             a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                             a19 a18 a17 a16 a15 a14 a13 a12 a11 a10
                             a9 a8 a7-equiv a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-24

(defthm bit-equiv-implies-equal-merge-32-bits-24
  (implies
       (bit-equiv a8 a8-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30
                             a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                             a19 a18 a17 a16 a15 a14 a13 a12 a11 a10
                             a9 a8-equiv a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-23

(defthm bit-equiv-implies-equal-merge-32-bits-23
  (implies
       (bit-equiv a9 a9-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30
                             a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                             a19 a18 a17 a16 a15 a14 a13 a12 a11 a10
                             a9-equiv a8 a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-22

(defthm bit-equiv-implies-equal-merge-32-bits-22
  (implies
       (bit-equiv a10 a10-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30 a29 a28
                             a27 a26 a25 a24 a23 a22 a21 a20 a19 a18
                             a17 a16 a15 a14 a13 a12 a11 a10-equiv
                             a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-21

(defthm bit-equiv-implies-equal-merge-32-bits-21
  (implies
       (bit-equiv a11 a11-equiv)
       (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                             a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-32-bits a31 a30 a29
                             a28 a27 a26 a25 a24 a23 a22 a21 a20 a19
                             a18 a17 a16 a15 a14 a13 a12 a11-equiv
                             a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
  :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-20

(defthm bit-equiv-implies-equal-merge-32-bits-20
 (implies
      (bit-equiv a12 a12-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                            a19 a18 a17 a16 a15 a14 a13 a12-equiv
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-19

(defthm bit-equiv-implies-equal-merge-32-bits-19
 (implies
      (bit-equiv a13 a13-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                            a19 a18 a17 a16 a15 a14 a13-equiv a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-18

(defthm bit-equiv-implies-equal-merge-32-bits-18
 (implies
      (bit-equiv a14 a14-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                            a19 a18 a17 a16 a15 a14-equiv a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-17

(defthm bit-equiv-implies-equal-merge-32-bits-17
 (implies
      (bit-equiv a15 a15-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                            a19 a18 a17 a16 a15-equiv a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-16

(defthm bit-equiv-implies-equal-merge-32-bits-16
 (implies
      (bit-equiv a16 a16-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                            a19 a18 a17 a16-equiv a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-15

(defthm bit-equiv-implies-equal-merge-32-bits-15
 (implies
      (bit-equiv a17 a17-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                            a19 a18 a17-equiv a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-14

(defthm bit-equiv-implies-equal-merge-32-bits-14
 (implies
      (bit-equiv a18 a18-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                            a19 a18-equiv a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-13

(defthm bit-equiv-implies-equal-merge-32-bits-13
 (implies
      (bit-equiv a19 a19-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25 a24 a23 a22 a21 a20
                            a19-equiv a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-12

(defthm bit-equiv-implies-equal-merge-32-bits-12
 (implies
      (bit-equiv a20 a20-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30 a29 a28
                            a27 a26 a25 a24 a23 a22 a21 a20-equiv
                            a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-11

(defthm bit-equiv-implies-equal-merge-32-bits-11
 (implies
      (bit-equiv a21 a21-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30 a29
                            a28 a27 a26 a25 a24 a23 a22 a21-equiv
                            a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-10

(defthm bit-equiv-implies-equal-merge-32-bits-10
 (implies
      (bit-equiv a22 a22-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25 a24 a23 a22-equiv
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-9

(defthm bit-equiv-implies-equal-merge-32-bits-9
 (implies
      (bit-equiv a23 a23-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25 a24 a23-equiv a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-8

(defthm bit-equiv-implies-equal-merge-32-bits-8
 (implies
      (bit-equiv a24 a24-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25 a24-equiv a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-7

(defthm bit-equiv-implies-equal-merge-32-bits-7
 (implies
      (bit-equiv a25 a25-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26 a25-equiv a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-6

(defthm bit-equiv-implies-equal-merge-32-bits-6
 (implies
      (bit-equiv a26 a26-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27 a26-equiv a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-5

(defthm bit-equiv-implies-equal-merge-32-bits-5
 (implies
      (bit-equiv a27 a27-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28 a27-equiv a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-4

(defthm bit-equiv-implies-equal-merge-32-bits-4
 (implies
      (bit-equiv a28 a28-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29 a28-equiv a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-3

(defthm bit-equiv-implies-equal-merge-32-bits-3
 (implies
      (bit-equiv a29 a29-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30
                            a29-equiv a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-2

(defthm bit-equiv-implies-equal-merge-32-bits-2
 (implies
      (bit-equiv a30 a30-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31 a30-equiv
                            a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))

Theorem: bit-equiv-implies-equal-merge-32-bits-1

(defthm bit-equiv-implies-equal-merge-32-bits-1
 (implies
      (bit-equiv a31 a31-equiv)
      (equal (merge-32-bits a31 a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-32-bits a31-equiv
                            a30 a29 a28 a27 a26 a25 a24 a23 a22
                            a21 a20 a19 a18 a17 a16 a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))
 :rule-classes (:congruence))