		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))