Bitwise logical `nand' of two integers
When integers are viewed in their two's complement representation,
lognand returns their bitwise logical `nand'.
The guard for lognand requires its arguments to be integers.
Lognand is defined in Common Lisp. See any Common Lisp documentation for
(defun lognand (i j)
(declare (xargs :guard (and (integerp i) (integerp j))))
(lognot (logand i j)))