Same as lit-negate-cond, but with a type declaration that the input literal is 32 bits unsigned.
Function:
(defun lit-negate-cond^$inline (lit neg) (declare (type (unsigned-byte 32) lit) (type bit neg)) (declare (xargs :guard (and (litp lit) (bitp neg)))) (declare (xargs :guard (unsigned-byte-p 32 lit) :split-types t)) (let ((__function__ 'lit-negate-cond^)) (declare (ignorable __function__)) (mbe :logic (lit-negate-cond lit neg) :exec (the (unsigned-byte 32) (logxor neg (the (unsigned-byte 32) lit))))))
Theorem:
(defthm lit-negate-cond^$inline-of-lit-fix-lit (equal (lit-negate-cond^$inline (lit-fix lit) neg) (lit-negate-cond^$inline lit neg)))
Theorem:
(defthm lit-negate-cond^$inline-lit-equiv-congruence-on-lit (implies (lit-equiv lit lit-equiv) (equal (lit-negate-cond^$inline lit neg) (lit-negate-cond^$inline lit-equiv neg))) :rule-classes :congruence)
Theorem:
(defthm lit-negate-cond^$inline-of-bfix-neg (equal (lit-negate-cond^$inline lit (bfix neg)) (lit-negate-cond^$inline lit neg)))
Theorem:
(defthm lit-negate-cond^$inline-bit-equiv-congruence-on-neg (implies (bit-equiv neg neg-equiv) (equal (lit-negate-cond^$inline lit neg) (lit-negate-cond^$inline lit neg-equiv))) :rule-classes :congruence)