Function:
(defun binary-bitop-cofactor1 (op bit) (declare (type (unsigned-byte 4) op)) (declare (xargs :guard (and (integerp op) (bitp bit)))) (let ((__function__ 'binary-bitop-cofactor1)) (declare (ignorable __function__)) (logior (logbit (lbfix bit) op) (ash (logbit (+ 2 (lbfix bit)) op) 1))))
Theorem:
(defthm integerp-of-binary-bitop-cofactor1 (b* ((unary-op (binary-bitop-cofactor1 op bit))) (integerp unary-op)) :rule-classes :type-prescription)
Theorem:
(defthm width-of-binary-bitop-cofactor1 (b* ((?unary-op (binary-bitop-cofactor1 op bit))) (unsigned-byte-p 2 unary-op)))
Theorem:
(defthm binary-bitop-cofactor1-correct (b* ((?unary-op (binary-bitop-cofactor1 op bit))) (equal (unary-bitop unary-op x) (binary-bitop op (- (bfix bit)) x))))
Theorem:
(defthm binary-bitop-cofactor1-of-ifix-op (equal (binary-bitop-cofactor1 (ifix op) bit) (binary-bitop-cofactor1 op bit)))
Theorem:
(defthm binary-bitop-cofactor1-int-equiv-congruence-on-op (implies (int-equiv op op-equiv) (equal (binary-bitop-cofactor1 op bit) (binary-bitop-cofactor1 op-equiv bit))) :rule-classes :congruence)
Theorem:
(defthm binary-bitop-cofactor1-of-bfix-bit (equal (binary-bitop-cofactor1 op (bfix bit)) (binary-bitop-cofactor1 op bit)))
Theorem:
(defthm binary-bitop-cofactor1-bit-equiv-congruence-on-bit (implies (bit-equiv bit bit-equiv) (equal (binary-bitop-cofactor1 op bit) (binary-bitop-cofactor1 op bit-equiv))) :rule-classes :congruence)