		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Binary-bitop-cofactor2

Signature
(binary-bitop-cofactor2 op bit) → unary-op
Arguments: op — Guard (integerp op).; bit — Guard (bitp bit).
Returns: unary-op — Type (integerp unary-op).

Definitions and Theorems

Function: binary-bitop-cofactor2

(defun binary-bitop-cofactor2 (op bit)
  (declare (type (unsigned-byte 4) op))
  (declare (xargs :guard (and (integerp op) (bitp bit))))
  (let ((__function__ 'binary-bitop-cofactor2))
    (declare (ignorable __function__))
    (loghead 2 (logtail (* 2 (lbfix bit)) op))))

Theorem: integerp-of-binary-bitop-cofactor2

(defthm integerp-of-binary-bitop-cofactor2
  (b* ((unary-op (binary-bitop-cofactor2 op bit)))
    (integerp unary-op))
  :rule-classes :type-prescription)

Theorem: width-of-binary-bitop-cofactor2

(defthm width-of-binary-bitop-cofactor2
  (b* ((?unary-op (binary-bitop-cofactor2 op bit)))
    (unsigned-byte-p 2 unary-op)))

Theorem: binary-bitop-cofactor2-correct

(defthm binary-bitop-cofactor2-correct
  (b* ((?unary-op (binary-bitop-cofactor2 op bit)))
    (equal (unary-bitop unary-op x)
           (binary-bitop op x (- (bfix bit))))))

Theorem: binary-bitop-cofactor2-of-ifix-op

(defthm binary-bitop-cofactor2-of-ifix-op
  (equal (binary-bitop-cofactor2 (ifix op) bit)
         (binary-bitop-cofactor2 op bit)))

Theorem: binary-bitop-cofactor2-int-equiv-congruence-on-op

(defthm binary-bitop-cofactor2-int-equiv-congruence-on-op
  (implies (int-equiv op op-equiv)
           (equal (binary-bitop-cofactor2 op bit)
                  (binary-bitop-cofactor2 op-equiv bit)))
  :rule-classes :congruence)

Theorem: binary-bitop-cofactor2-of-bfix-bit

(defthm binary-bitop-cofactor2-of-bfix-bit
  (equal (binary-bitop-cofactor2 op (bfix bit))
         (binary-bitop-cofactor2 op bit)))

Theorem: binary-bitop-cofactor2-bit-equiv-congruence-on-bit

(defthm binary-bitop-cofactor2-bit-equiv-congruence-on-bit
  (implies (bit-equiv bit bit-equiv)
           (equal (binary-bitop-cofactor2 op bit)
                  (binary-bitop-cofactor2 op bit-equiv)))
  :rule-classes :congruence)