Complementation
Theorem:
(defthm lognot-def (implies (integerp x) (equal (lognot x) (1- (- x)))))
Theorem:
(defthm lognot-shift (implies (and (integerp x) (natp k)) (equal (lognot (* (expt 2 k) x)) (+ (* (expt 2 k) (lognot x)) (1- (expt 2 k))))))
Theorem:
(defthm lognot-fl (implies (and (integerp x) (not (zp n))) (equal (lognot (fl (/ x n))) (fl (/ (lognot x) n)))))
Theorem:
(defthm mod-lognot (implies (and (integerp x) (natp n)) (equal (mod (lognot x) (expt 2 n)) (1- (- (expt 2 n) (mod x (expt 2 n)))))))
Theorem:
(defthm bits-lognot (implies (and (natp i) (natp j) (<= j i) (integerp x)) (equal (bits (lognot x) i j) (- (1- (expt 2 (- (1+ i) j))) (bits x i j)))))
Theorem:
(defthm bitn-lognot (implies (and (integerp x) (natp n)) (not (equal (bitn (lognot x) n) (bitn x n)))) :rule-classes nil)
Theorem:
(defthm bits-lognot-bits (implies (and (integerp x) (natp i) (natp j) (natp k) (natp l) (<= l k) (<= k (- i j))) (equal (bits (lognot (bits x i j)) k l) (bits (lognot x) (+ k j) (+ l j)))))
Theorem:
(defthm bits-lognot-bits-lognot (implies (and (integerp x) (natp i) (natp j) (natp k) (natp l) (<= l k) (<= k (- i j))) (equal (bits (lognot (bits (lognot x) i j)) k l) (bits x (+ k j) (+ l j)))))
Theorem:
(defthm logand-bits-lognot (implies (and (integerp x) (integerp n) (bvecp y n)) (equal (logand y (bits (lognot x) (1- n) 0)) (logand y (lognot (bits x (1- n) 0))))))