Trailing One Prediction
Theorem:
(defthm top-thm-1 (implies (and (natp k) (integerp a) (integerp b)) (equal (equal (bits (+ a b 1) k 0) 0) (equal (bits (lognot (logxor a b)) k 0) 0))) :rule-classes nil)
Theorem:
(defthm top-thm-2 (implies (and (natp n) (integerp a) (integerp b) (natp k) (< k n) (or (equal c 0) (equal c 1))) (equal (equal (bits (+ a b c) k 0) 0) (equal (bits (logxor (logxor a b) (cat (logior a b) n c 1)) k 0) 0))) :rule-classes nil)