Optimized version of
(parity4 x) → p
The basic idea is from Sean Anderson's bit twiddling
hacks page. The number
It seems that using
Function:
(defun parity4$inline (x) (declare (type (unsigned-byte 4) x)) (let ((__function__ 'parity4)) (declare (ignorable __function__)) (mbe :logic (parity 4 x) :exec (the bit (logand 1 (the (unsigned-byte 32) (ash (the (unsigned-byte 32) 27030) (the (integer -16 0) (- (the (unsigned-byte 4) x))))))))))
Theorem:
(defthm bitp-of-parity4 (b* ((p (parity4$inline x))) (bitp p)) :rule-classes :type-prescription)