		Search-engine friendly clone of the ACL2 documentation.

Bitops/merge

Merge-2-bits

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

Signature
(merge-2-bits a1 a0) → result
Arguments: a1 — Guard (bitp a1).; a0 — Guard (bitp a0).
Returns: result — Type (natp result).

Definitions and Theorems

Function: merge-2-bits$inline

(defun
 acl2::merge-2-bits$inline (a1 a0)
 (declare (xargs :guard (and (bitp a1) (bitp a0))))
 (declare (type bit a1 a0))
 (declare (xargs :split-types t))
 (let ((__function__ 'merge-2-bits))
      (declare (ignorable __function__))
      (mbe :logic (logapp* 1 (bfix a0) (bfix a1) 0)
           :exec (b* ((ans a0))
                     (the (unsigned-byte 2)
                          (logior (the (unsigned-byte 2) (ash a1 1))
                                  (the (unsigned-byte 2) ans)))))))

Theorem: natp-of-merge-2-bits

(defthm acl2::natp-of-merge-2-bits
        (b* ((result (acl2::merge-2-bits$inline a1 a0)))
            (natp result))
        :rule-classes :type-prescription)

Theorem: unsigned-byte-p-2-of-merge-2-bits

(defthm unsigned-byte-p-2-of-merge-2-bits
        (unsigned-byte-p 2 (merge-2-bits a1 a0)))

Theorem: merge-2-bits-is-merge-unsigneds

(defthm merge-2-bits-is-merge-unsigneds
        (equal (merge-2-bits a1 a0)
               (merge-unsigneds 1 (list (bfix a1) (bfix a0)))))

Basic bit-equiv congruences.

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

(defthm bit-equiv-implies-equal-merge-2-bits-2
        (implies (bit-equiv a0 a0-equiv)
                 (equal (merge-2-bits a1 a0)
                        (merge-2-bits a1 a0-equiv)))
        :rule-classes (:congruence))

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

(defthm bit-equiv-implies-equal-merge-2-bits-1
        (implies (bit-equiv a1 a1-equiv)
                 (equal (merge-2-bits a1 a0)
                        (merge-2-bits a1-equiv a0)))
        :rule-classes (:congruence))