• 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-16-bits

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

Signature

(merge-16-bits a15 a14 a13 a12 
               a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0) 
 
  → 
result

Arguments

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

(defun acl2::merge-16-bits$inline
       (a15 a14 a13 a12
            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
 (declare (xargs :guard (and (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 a15 a14 a13 a12
                a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0))
 (declare (xargs :split-types t))
 (let ((__function__ 'merge-16-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)
                 0)
        :exec
        (b* ((ans a0)
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a1 1))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a2 2))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a3 3))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a4 4))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a5 5))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a6 6))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a7 7))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a8 8))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a9 9))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a10 10))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a11 11))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a12 12))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a13 13))
                               (the (unsigned-byte 16) ans))))
             (ans (the (unsigned-byte 16)
                       (logior (the (unsigned-byte 16) (ash a14 14))
                               (the (unsigned-byte 16) ans)))))
          (the (unsigned-byte 16)
               (logior (the (unsigned-byte 16) (ash a15 15))
                       (the (unsigned-byte 16) ans)))))))

Theorem: natp-of-merge-16-bits

(defthm acl2::natp-of-merge-16-bits
  (b* ((result (acl2::merge-16-bits$inline
                    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-16-of-merge-16-bits

(defthm unsigned-byte-p-16-of-merge-16-bits
  (unsigned-byte-p
       16
       (merge-16-bits a15 a14 a13 a12
                      a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)))

Theorem: merge-16-bits-is-merge-unsigneds

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

(defthm bit-equiv-implies-equal-merge-16-bits-16
  (implies
       (bit-equiv a0 a0-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-15

(defthm bit-equiv-implies-equal-merge-16-bits-15
  (implies
       (bit-equiv a1 a1-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-14

(defthm bit-equiv-implies-equal-merge-16-bits-14
  (implies
       (bit-equiv a2 a2-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-13

(defthm bit-equiv-implies-equal-merge-16-bits-13
  (implies
       (bit-equiv a3 a3-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-12

(defthm bit-equiv-implies-equal-merge-16-bits-12
  (implies
       (bit-equiv a4 a4-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-11

(defthm bit-equiv-implies-equal-merge-16-bits-11
  (implies
       (bit-equiv a5 a5-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-10

(defthm bit-equiv-implies-equal-merge-16-bits-10
  (implies
       (bit-equiv a6 a6-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-9

(defthm bit-equiv-implies-equal-merge-16-bits-9
  (implies
       (bit-equiv a7 a7-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-8

(defthm bit-equiv-implies-equal-merge-16-bits-8
  (implies
       (bit-equiv a8 a8-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-7

(defthm bit-equiv-implies-equal-merge-16-bits-7
  (implies
       (bit-equiv a9 a9-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-6

(defthm bit-equiv-implies-equal-merge-16-bits-6
  (implies
       (bit-equiv a10 a10-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-5

(defthm bit-equiv-implies-equal-merge-16-bits-5
  (implies
       (bit-equiv a11 a11-equiv)
       (equal (merge-16-bits a15 a14 a13 a12
                             a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
              (merge-16-bits 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-16-bits-4

(defthm bit-equiv-implies-equal-merge-16-bits-4
 (implies
      (bit-equiv a12 a12-equiv)
      (equal (merge-16-bits a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-16-bits 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-16-bits-3

(defthm bit-equiv-implies-equal-merge-16-bits-3
 (implies
      (bit-equiv a13 a13-equiv)
      (equal (merge-16-bits a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-16-bits 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-16-bits-2

(defthm bit-equiv-implies-equal-merge-16-bits-2
 (implies
      (bit-equiv a14 a14-equiv)
      (equal (merge-16-bits a15 a14 a13 a12
                            a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a0)
             (merge-16-bits 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-16-bits-1

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