Same as lit->neg, but with a type declaration that the input is 32 bits unsigned.
(lit->neg^ lit) → *
Function:
(defun lit->neg^$inline (lit) (declare (type (unsigned-byte 32) lit)) (declare (xargs :guard (litp lit))) (let ((__function__ 'lit->neg^)) (declare (ignorable __function__)) (mbe :logic (lit->neg lit) :exec (the bit (logand 1 (the (unsigned-byte 32) lit))))))
Theorem:
(defthm lit->neg^$inline-of-lit-fix-lit (equal (lit->neg^$inline (lit-fix lit)) (lit->neg^$inline lit)))
Theorem:
(defthm lit->neg^$inline-lit-equiv-congruence-on-lit (implies (lit-equiv lit lit-equiv) (equal (lit->neg^$inline lit) (lit->neg^$inline lit-equiv))) :rule-classes :congruence)