Function:
(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:
(defthm integerp-of-binary-bitop-cofactor2 (b* ((unary-op (binary-bitop-cofactor2 op bit))) (integerp unary-op)) :rule-classes :type-prescription)
Theorem:
(defthm width-of-binary-bitop-cofactor2 (b* ((?unary-op (binary-bitop-cofactor2 op bit))) (unsigned-byte-p 2 unary-op)))
Theorem:
(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:
(defthm binary-bitop-cofactor2-of-ifix-op (equal (binary-bitop-cofactor2 (ifix op) bit) (binary-bitop-cofactor2 op bit)))
Theorem:
(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:
(defthm binary-bitop-cofactor2-of-bfix-bit (equal (binary-bitop-cofactor2 op (bfix bit)) (binary-bitop-cofactor2 op bit)))
Theorem:
(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)