• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
        • Bitops/merge
          • Merge-64-u8s
          • Merge-64-bits
          • Merge-32-u8s
          • Merge-32-u4s
          • Merge-32-u2s
          • Merge-32-u16s
          • Merge-32-bits
          • Merge-16-bits
          • Merge-16-u32s
          • Merge-16-u16s
          • Merge-16-u8s
          • Merge-16-u4s
          • Merge-16-u2s
          • Merge-8-bits
          • Merge-8-u2s
          • Merge-8-u64s
          • Merge-8-u4s
          • Merge-8-u32s
          • Merge-8-u16s
          • Merge-8-u8s
          • Merge-4-bits
          • Merge-4-u8s
          • Merge-4-u4s
          • Merge-4-u16s
          • Merge-4-u2s
          • Merge-4-u64s
          • Merge-4-u32s
          • Merge-4-u128s
          • Merge-2-u64s
          • Merge-2-u256s
          • Merge-2-u16s
          • Merge-2-u128s
          • Merge-2-bits
          • Merge-2-u8s
          • Merge-2-u4s
          • Merge-2-u32s
          • Merge-2-u2s
          • Merge-unsigneds
          • Merge-unsigneds-aux
          • Indexed-subst-templates
        • Bitops-compatibility
        • Bitops-books
        • Logbitp-reasoning
        • Bitops/signed-byte-p
        • Fast-part-select
        • Bitops/integer-length
        • Bitops/extra-defs
        • Install-bit
        • Trailing-0-count
        • Bitops/defaults
        • Logbitp-mismatch
        • Trailing-1-count
        • Bitops/rotate
        • Bitops/equal-by-logbitp
        • Bitops/ash-bounds
        • Bitops/fast-logrev
        • Limited-shifts
        • Bitops/part-select
        • Bitops/parity
        • Bitops/saturate
        • Bitops/part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra
  • Testing-utilities

• Bitops/merge

Merge-64-bits

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

Signature

(merge-64-bits a63 a62 
               a61 a60 a59 a58 a57 a56 a55 a54 a53 a52 
               a51 a50 a49 a48 a47 a46 a45 a44 a43 a42 
               a41 a40 a39 a38 a37 a36 a35 a34 a33 a32 
               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

a63 — Guard (bitp a63).

a62 — Guard (bitp a62).

a61 — Guard (bitp a61).

a60 — Guard (bitp a60).

a59 — Guard (bitp a59).

a58 — Guard (bitp a58).

a57 — Guard (bitp a57).

a56 — Guard (bitp a56).

a55 — Guard (bitp a55).

a54 — Guard (bitp a54).

a53 — Guard (bitp a53).

a52 — Guard (bitp a52).

a51 — Guard (bitp a51).

a50 — Guard (bitp a50).

a49 — Guard (bitp a49).

a48 — Guard (bitp a48).

a47 — Guard (bitp a47).

a46 — Guard (bitp a46).

a45 — Guard (bitp a45).

a44 — Guard (bitp a44).

a43 — Guard (bitp a43).

a42 — Guard (bitp a42).

a41 — Guard (bitp a41).

a40 — Guard (bitp a40).

a39 — Guard (bitp a39).

a38 — Guard (bitp a38).

a37 — Guard (bitp a37).

a36 — Guard (bitp a36).

a35 — Guard (bitp a35).

a34 — Guard (bitp a34).

a33 — Guard (bitp a33).

a32 — Guard (bitp a32).

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-64-bits$inline

(defun acl2::merge-64-bits$inline
       (a63 a62
            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
            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 a63)
                             (bitp a62)
                             (bitp a61)
                             (bitp a60)
                             (bitp a59)
                             (bitp a58)
                             (bitp a57)
                             (bitp a56)
                             (bitp a55)
                             (bitp a54)
                             (bitp a53)
                             (bitp a52)
                             (bitp a51)
                             (bitp a50)
                             (bitp a49)
                             (bitp a48)
                             (bitp a47)
                             (bitp a46)
                             (bitp a45)
                             (bitp a44)
                             (bitp a43)
                             (bitp a42)
                             (bitp a41)
                             (bitp a40)
                             (bitp a39)
                             (bitp a38)
                             (bitp a37)
                             (bitp a36)
                             (bitp a35)
                             (bitp a34)
                             (bitp a33)
                             (bitp a32)
                             (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 a63 a62
                a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                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-64-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)
                 (bfix a32)
                 (bfix a33)
                 (bfix a34)
                 (bfix a35)
                 (bfix a36)
                 (bfix a37)
                 (bfix a38)
                 (bfix a39)
                 (bfix a40)
                 (bfix a41)
                 (bfix a42)
                 (bfix a43)
                 (bfix a44)
                 (bfix a45)
                 (bfix a46)
                 (bfix a47)
                 (bfix a48)
                 (bfix a49)
                 (bfix a50)
                 (bfix a51)
                 (bfix a52)
                 (bfix a53)
                 (bfix a54)
                 (bfix a55)
                 (bfix a56)
                 (bfix a57)
                 (bfix a58)
                 (bfix a59)
                 (bfix a60)
                 (bfix a61)
                 (bfix a62)
                 (bfix a63)
                 0)
        :exec
        (b* ((ans a0)
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a1 1))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a2 2))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a3 3))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a4 4))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a5 5))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a6 6))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a7 7))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a8 8))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a9 9))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a10 10))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a11 11))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a12 12))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a13 13))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a14 14))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a15 15))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a16 16))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a17 17))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a18 18))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a19 19))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a20 20))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a21 21))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a22 22))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a23 23))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a24 24))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a25 25))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a26 26))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a27 27))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a28 28))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a29 29))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a30 30))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a31 31))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a32 32))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a33 33))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a34 34))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a35 35))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a36 36))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a37 37))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a38 38))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a39 39))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a40 40))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a41 41))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a42 42))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a43 43))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a44 44))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a45 45))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a46 46))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a47 47))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a48 48))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a49 49))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a50 50))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a51 51))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a52 52))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a53 53))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a54 54))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a55 55))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a56 56))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a57 57))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a58 58))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a59 59))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a60 60))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a61 61))
                               (the (unsigned-byte 64) ans))))
             (ans (the (unsigned-byte 64)
                       (logior (the (unsigned-byte 64) (ash a62 62))
                               (the (unsigned-byte 64) ans)))))
          (the (unsigned-byte 64)
               (logior (the (unsigned-byte 64) (ash a63 63))
                       (the (unsigned-byte 64) ans)))))))

Theorem: natp-of-merge-64-bits

(defthm acl2::natp-of-merge-64-bits
  (b* ((result (acl2::merge-64-bits$inline
                    a63 a62
                    a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                    a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                    a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                    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-64-of-merge-64-bits

(defthm unsigned-byte-p-64-of-merge-64-bits
  (unsigned-byte-p
       64
       (merge-64-bits a63 a62
                      a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                      a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                      a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                      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-64-bits-is-merge-unsigneds

(defthm merge-64-bits-is-merge-unsigneds
  (equal (merge-64-bits a63 a62
                        a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                        a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                        a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                        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 a63)
                                (bfix a62)
                                (bfix a61)
                                (bfix a60)
                                (bfix a59)
                                (bfix a58)
                                (bfix a57)
                                (bfix a56)
                                (bfix a55)
                                (bfix a54)
                                (bfix a53)
                                (bfix a52)
                                (bfix a51)
                                (bfix a50)
                                (bfix a49)
                                (bfix a48)
                                (bfix a47)
                                (bfix a46)
                                (bfix a45)
                                (bfix a44)
                                (bfix a43)
                                (bfix a42)
                                (bfix a41)
                                (bfix a40)
                                (bfix a39)
                                (bfix a38)
                                (bfix a37)
                                (bfix a36)
                                (bfix a35)
                                (bfix a34)
                                (bfix a33)
                                (bfix a32)
                                (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-64-bits-64

(defthm bit-equiv-implies-equal-merge-64-bits-64
  (implies
       (bit-equiv a0 a0-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60
                             a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                             a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                             a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-63

(defthm bit-equiv-implies-equal-merge-64-bits-63
  (implies
       (bit-equiv a1 a1-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60
                             a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                             a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                             a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-62

(defthm bit-equiv-implies-equal-merge-64-bits-62
  (implies
       (bit-equiv a2 a2-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60
                             a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                             a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                             a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-61

(defthm bit-equiv-implies-equal-merge-64-bits-61
  (implies
       (bit-equiv a3 a3-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60
                             a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                             a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                             a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-60

(defthm bit-equiv-implies-equal-merge-64-bits-60
  (implies
       (bit-equiv a4 a4-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60
                             a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                             a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                             a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-59

(defthm bit-equiv-implies-equal-merge-64-bits-59
  (implies
       (bit-equiv a5 a5-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60
                             a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                             a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                             a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-58

(defthm bit-equiv-implies-equal-merge-64-bits-58
  (implies
       (bit-equiv a6 a6-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60
                             a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                             a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                             a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-57

(defthm bit-equiv-implies-equal-merge-64-bits-57
  (implies
       (bit-equiv a7 a7-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60
                             a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                             a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                             a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-56

(defthm bit-equiv-implies-equal-merge-64-bits-56
  (implies
       (bit-equiv a8 a8-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60
                             a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                             a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                             a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-55

(defthm bit-equiv-implies-equal-merge-64-bits-55
  (implies
       (bit-equiv a9 a9-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60
                             a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                             a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                             a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-54

(defthm bit-equiv-implies-equal-merge-64-bits-54
  (implies
       (bit-equiv a10 a10-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60 a59 a58
                             a57 a56 a55 a54 a53 a52 a51 a50 a49 a48
                             a47 a46 a45 a44 a43 a42 a41 a40 a39 a38
                             a37 a36 a35 a34 a33 a32 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-64-bits-53

(defthm bit-equiv-implies-equal-merge-64-bits-53
  (implies
       (bit-equiv a11 a11-equiv)
       (equal (merge-64-bits a63 a62
                             a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                             a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                             a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                             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-64-bits a63 a62 a61 a60 a59
                             a58 a57 a56 a55 a54 a53 a52 a51 a50 a49
                             a48 a47 a46 a45 a44 a43 a42 a41 a40 a39
                             a38 a37 a36 a35 a34 a33 a32 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-64-bits-52

(defthm bit-equiv-implies-equal-merge-64-bits-52
 (implies
      (bit-equiv a12 a12-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-51

(defthm bit-equiv-implies-equal-merge-64-bits-51
 (implies
      (bit-equiv a13 a13-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-50

(defthm bit-equiv-implies-equal-merge-64-bits-50
 (implies
      (bit-equiv a14 a14-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-49

(defthm bit-equiv-implies-equal-merge-64-bits-49
 (implies
      (bit-equiv a15 a15-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-48

(defthm bit-equiv-implies-equal-merge-64-bits-48
 (implies
      (bit-equiv a16 a16-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-47

(defthm bit-equiv-implies-equal-merge-64-bits-47
 (implies
      (bit-equiv a17 a17-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-46

(defthm bit-equiv-implies-equal-merge-64-bits-46
 (implies
      (bit-equiv a18 a18-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-45

(defthm bit-equiv-implies-equal-merge-64-bits-45
 (implies
      (bit-equiv a19 a19-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-44

(defthm bit-equiv-implies-equal-merge-64-bits-44
 (implies
      (bit-equiv a20 a20-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60 a59 a58
                            a57 a56 a55 a54 a53 a52 a51 a50 a49 a48
                            a47 a46 a45 a44 a43 a42 a41 a40 a39 a38
                            a37 a36 a35 a34 a33 a32 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-64-bits-43

(defthm bit-equiv-implies-equal-merge-64-bits-43
 (implies
      (bit-equiv a21 a21-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60 a59
                            a58 a57 a56 a55 a54 a53 a52 a51 a50 a49
                            a48 a47 a46 a45 a44 a43 a42 a41 a40 a39
                            a38 a37 a36 a35 a34 a33 a32 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-64-bits-42

(defthm bit-equiv-implies-equal-merge-64-bits-42
 (implies
      (bit-equiv a22 a22-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-41

(defthm bit-equiv-implies-equal-merge-64-bits-41
 (implies
      (bit-equiv a23 a23-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-40

(defthm bit-equiv-implies-equal-merge-64-bits-40
 (implies
      (bit-equiv a24 a24-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-39

(defthm bit-equiv-implies-equal-merge-64-bits-39
 (implies
      (bit-equiv a25 a25-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-38

(defthm bit-equiv-implies-equal-merge-64-bits-38
 (implies
      (bit-equiv a26 a26-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-37

(defthm bit-equiv-implies-equal-merge-64-bits-37
 (implies
      (bit-equiv a27 a27-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-36

(defthm bit-equiv-implies-equal-merge-64-bits-36
 (implies
      (bit-equiv a28 a28-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-35

(defthm bit-equiv-implies-equal-merge-64-bits-35
 (implies
      (bit-equiv a29 a29-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32 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-64-bits-34

(defthm bit-equiv-implies-equal-merge-64-bits-34
 (implies
      (bit-equiv a30 a30-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60 a59 a58
                            a57 a56 a55 a54 a53 a52 a51 a50 a49 a48
                            a47 a46 a45 a44 a43 a42 a41 a40 a39 a38
                            a37 a36 a35 a34 a33 a32 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-64-bits-33

(defthm bit-equiv-implies-equal-merge-64-bits-33
 (implies
      (bit-equiv a31 a31-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60 a59
                            a58 a57 a56 a55 a54 a53 a52 a51 a50 a49
                            a48 a47 a46 a45 a44 a43 a42 a41 a40 a39
                            a38 a37 a36 a35 a34 a33 a32 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))

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

(defthm bit-equiv-implies-equal-merge-64-bits-32
 (implies
      (bit-equiv a32 a32-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33 a32-equiv
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-31
 (implies
      (bit-equiv a33 a33-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34 a33-equiv a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-30
 (implies
      (bit-equiv a34 a34-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35 a34-equiv a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-29
 (implies
      (bit-equiv a35 a35-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36 a35-equiv a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-28
 (implies
      (bit-equiv a36 a36-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37 a36-equiv a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-27
 (implies
      (bit-equiv a37 a37-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38 a37-equiv a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-26
 (implies
      (bit-equiv a38 a38-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39 a38-equiv a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-25
 (implies
      (bit-equiv a39 a39-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42 a41 a40
                            a39-equiv a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-24
 (implies
      (bit-equiv a40 a40-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60 a59 a58
                            a57 a56 a55 a54 a53 a52 a51 a50 a49 a48
                            a47 a46 a45 a44 a43 a42 a41 a40-equiv
                            a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-23
 (implies
      (bit-equiv a41 a41-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60 a59
                            a58 a57 a56 a55 a54 a53 a52 a51 a50 a49
                            a48 a47 a46 a45 a44 a43 a42 a41-equiv
                            a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-22
 (implies
      (bit-equiv a42 a42-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43 a42-equiv
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-21
 (implies
      (bit-equiv a43 a43-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44 a43-equiv a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-20
 (implies
      (bit-equiv a44 a44-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45 a44-equiv a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-19
 (implies
      (bit-equiv a45 a45-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46 a45-equiv a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-18
 (implies
      (bit-equiv a46 a46-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47 a46-equiv a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-17
 (implies
      (bit-equiv a47 a47-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48 a47-equiv a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-16
 (implies
      (bit-equiv a48 a48-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49 a48-equiv a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-15
 (implies
      (bit-equiv a49 a49-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52 a51 a50
                            a49-equiv a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-14
 (implies
      (bit-equiv a50 a50-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60 a59 a58
                            a57 a56 a55 a54 a53 a52 a51 a50-equiv
                            a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-13
 (implies
      (bit-equiv a51 a51-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60 a59
                            a58 a57 a56 a55 a54 a53 a52 a51-equiv
                            a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-12
 (implies
      (bit-equiv a52 a52-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53 a52-equiv
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-11
 (implies
      (bit-equiv a53 a53-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54 a53-equiv a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-10
 (implies
      (bit-equiv a54 a54-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55 a54-equiv a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-9
 (implies
      (bit-equiv a55 a55-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56 a55-equiv a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-8
 (implies
      (bit-equiv a56 a56-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57 a56-equiv a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-7
 (implies
      (bit-equiv a57 a57-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58 a57-equiv a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-6
 (implies
      (bit-equiv a58 a58-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59 a58-equiv a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-5
 (implies
      (bit-equiv a59 a59-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60
                            a59-equiv a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-4
 (implies
      (bit-equiv a60 a60-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61 a60-equiv
                            a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-3
 (implies
      (bit-equiv a61 a61-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62 a61-equiv
                            a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-2
 (implies
      (bit-equiv a62 a62-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63 a62-equiv
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-64-bits-1
 (implies
      (bit-equiv a63 a63-equiv)
      (equal (merge-64-bits a63 a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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-64-bits a63-equiv a62
                            a61 a60 a59 a58 a57 a56 a55 a54 a53 a52
                            a51 a50 a49 a48 a47 a46 a45 a44 a43 a42
                            a41 a40 a39 a38 a37 a36 a35 a34 a33 a32
                            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)))
 :rule-classes (:congruence))