Rules about lognot applied to the signed integer 0 or 1.
We have two rules
to simplify applications of lognot-sint
to
Theorem:
(defthm lognot-sint-of-0 (equal (lognot-sint (sint-from-integer 0)) (sint-from-integer 1)))
Theorem:
(defthm lognot-sint-of-1 (equal (lognot-sint (sint-from-integer 1)) (sint-from-integer 0)))