Bitwise complement of a value of type
Function:
(defun bitnot-ullong (x) (declare (xargs :guard (and (ullongp x)))) (ullong-from-integer-mod (lognot (integer-from-ullong x))))
Theorem:
(defthm ullongp-of-bitnot-ullong (ullongp (bitnot-ullong x)))
Theorem:
(defthm bitnot-ullong-of-ullong-fix-x (equal (bitnot-ullong (ullong-fix x)) (bitnot-ullong x)))
Theorem:
(defthm bitnot-ullong-ullong-equiv-congruence-on-x (implies (ullong-equiv x x-equiv) (equal (bitnot-ullong x) (bitnot-ullong x-equiv))) :rule-classes :congruence)