(negate-slice64 x) computes the 64-bit two's complement negation
(negate-slice64 x) → ~x
We leave this enabled; we would usually not expect to try to reason about it.
(defun negate-slice64 (x) (declare (type (unsigned-byte 64) x)) (let ((__function__ 'negate-slice64)) (declare (ignorable __function__)) (mbe :logic (logand (+ 1 (lognot (nfix x))) (1- (expt 2 64))) :exec (the (unsigned-byte 64) (logand (the (signed-byte 65) (+ 1 (the (signed-byte 65) (lognot x)))) 18446744073709551615)))))
(defthm acl2::natp-of-negate-slice64 (b* ((~x (negate-slice64 x))) (natp ~x)) :rule-classes :type-prescription)
(defthm nat-equiv-implies-equal-negate-slice64-1 (implies (nat-equiv x x-equiv) (equal (negate-slice64 x) (negate-slice64 x-equiv))) :rule-classes (:congruence))
(defthm unsigned-byte-p-64-of-negate-slice64 (unsigned-byte-p 64 (negate-slice64 x)))