Logical ``exclusive or''
Xor is the ACL2 exclusive-or function. (xor P Q) means that either P or Q, but not both, is false (i.e., nil).
Function: xor
(defun xor (p q) (declare (xargs :guard t)) (if p (if q nil t) (if q t nil)))