Algebraic Properties
Theorem:
(defthm logand-x-0 (equal (logand x 0) 0))
Theorem:
(defthm logand-0-y (equal (logand 0 y) 0))
Theorem:
(defthm logior-x-0 (implies (integerp x) (equal (logior x 0) x)))
Theorem:
(defthm logior-0-y (implies (integerp y) (equal (logior 0 y) y)))
Theorem:
(defthm logxor-x-0 (implies (integerp x) (equal (logxor x 0) x)))
Theorem:
(defthm logxor-0-y (implies (integerp y) (equal (logxor 0 y) y)))
Theorem:
(defthm logand-self (implies (case-split (integerp x)) (equal (logand x x) x)))
Theorem:
(defthm logior-self (implies (case-split (integerp x)) (equal (logior x x) x)))
Theorem:
(defthm logxor-self (equal (logxor x x) 0))
Theorem:
(defthm lognot-lognot (implies (case-split (integerp i)) (equal (lognot (lognot i)) i)))
Theorem:
(defthm logior-not-0 (implies (and (integerp x) (integerp y)) (iff (equal (logior x y) 0) (and (= x 0) (= y 0)))))
Theorem:
(defthm logxor-not-0 (implies (and (integerp x) (integerp y)) (iff (equal (logxor x y) 0) (= x y))))
Theorem:
(defthm logand-x-1 (implies (bvecp x 1) (equal (logand x 1) x)))
Theorem:
(defthm logand-1-x (implies (bvecp x 1) (equal (logand 1 x) x)))
Theorem:
(defthm logior-1-x (implies (bvecp x 1) (equal (logior 1 x) 1)))
Theorem:
(defthm logior-x-1 (implies (bvecp x 1) (equal (logior x 1) 1)))
Theorem:
(defthm logand-x-m1 (implies (integerp x) (equal (logand x -1) x)))
Theorem:
(defthm logand-m1-y (implies (integerp y) (equal (logand -1 y) y)))
Theorem:
(defthm logior-x-m1 (implies (integerp x) (equal (logior x -1) -1)))
Theorem:
(defthm logior-m1-y (implies (integerp y) (equal (logior -1 y) -1)))
Theorem:
(defthm logxor-x-m1 (implies (integerp x) (equal (logxor x -1) (lognot x))))
Theorem:
(defthm logxor-m1-x (implies (integerp x) (equal (logxor -1 x) (lognot x))))
Theorem:
(defthm logand-commutative (equal (logand y x) (logand x y)))
Theorem:
(defthm logior-commutative (equal (logior y x) (logior x y)))
Theorem:
(defthm logxor-commutative (equal (logxor y x) (logxor x y)))
Theorem:
(defthm logand-commutative-2 (equal (logand y x z) (logand x y z)))
Theorem:
(defthm logior-commutative-2 (equal (logior y x z) (logior x y z)))
Theorem:
(defthm logxor-commutative-2 (equal (logxor y x z) (logxor x y z)))
Theorem:
(defthm logand-associative (equal (logand (logand x y) z) (logand x (logand y z))))
Theorem:
(defthm logior-associative (equal (logior (logior x y) z) (logior x (logior y z))))
Theorem:
(defthm logxor-associative (equal (logxor (logxor x y) z) (logxor x (logxor y z))))
Theorem:
(defthm logior-logand (implies (and (integerp x) (integerp y) (integerp z)) (equal (logior x (logand y z)) (logand (logior x y) (logior x z)))))
Theorem:
(defthm logior-logand-1 (implies (and (integerp x) (integerp y)) (equal (logior x (logand x y)) x)))
Theorem:
(defthm logand-logior (implies (and (integerp x) (integerp y) (integerp z)) (equal (logand x (logior y z)) (logior (logand x y) (logand x z)))))
Theorem:
(defthm logior-logand-2 (implies (and (integerp x) (integerp y) (integerp z)) (equal (logand (logior y z) x) (logior (logand y x) (logand z x)))))
Theorem:
(defthm log3 (implies (and (integerp x) (integerp y) (integerp z)) (equal (logior (logand x y) (logior (logand x z) (logand y z))) (logior (logand x y) (logand (logxor x y) z)))))
Theorem:
(defthm logxor-rewrite (implies (and (integerp x) (integerp y)) (equal (logxor x y) (logior (logand x (lognot y)) (logand y (lognot x))))))
Theorem:
(defthm lognot-logxor (and (equal (logxor (lognot x) y) (lognot (logxor x y))) (equal (logxor y (lognot x)) (lognot (logxor x y)))))