XOR development

[wdcraft01]

trafficstars

We already have a well-developed (and well used) disjunction (logical OR) operation and theory package. It can be useful to now add the exclusive disjunction or XOR operation in its own package, modeled after the inclusive disjunction we already have.

I'll plan to put this development work in its own branch and develop it gradually in parallel to some other work. I plan to use the (fairly) common literal $\oplus$ for formatted expressions and a simple 'xor' for the string representation. Apparently some texts use $\underline{\lor}$ (an underlined version of the standard $\lor$) for the exclusive case, but I'll stick with the more common $\oplus$ for now.

[wdcraft01]

XOr class work is mostly done, with a pretty thorough translation of Or class theorems and methods completed and tested.

A notable distinction between the Or and XOr operations ends up propagating into a notable distinction in a few of the theorems and methods: Or(A, B, ..., Z) is TRUE if any of the operands A, B, ..., Z is TRUE, but the analogous XOr(A, B, ... Z) is TRUE if and only if exactly an odd number of the operands A, B, ..., Z is/are TRUE and the remainder are FALSE. As a result of that difference between the Or and Xor operation, we have some nice quantification-related theorems for Or that do not have nice analogs for XOr, such as:

@wwitzel It would be interesting to try to formulate something(s) analogous for the XOr case, something along the lines of:

$(P(i) \oplus P(i+1) \oplus \cdots \oplus P(j)) = \exists_{k_{1},\ldots,k_{n} \in \{i, \ldots, j\}|n \text{ is odd}}\Big[P(k_{1}) \land P(k_{2}) \land \cdots \land P(k_{n}) \Big]$,

but the theorem would also need to acknowledge that each of remaining operands is FALSE. Perhaps there is an elegant way to do this?

And here is a related idea, perhaps a useful pair of "reduction" theorems, something like this:

$\forall_{m,n \in \mathbb{N}}\forall_{A_{1},\ldots,A_{m},B,C,D_{1},\ldots,D_{n}|B=TRUE}\Big[\big(A_{1}\oplus \cdots \oplus A_{m} \oplus B \oplus C \oplus D_{1} \oplus \cdots \oplus D_{n}\big) = \big(A_{1}\oplus \cdots \oplus A_{m} \oplus (\lnot C) \oplus D_{1} \oplus \cdots \oplus D_{n}\big)\Big]$

$\forall_{m,n \in \mathbb{N}}\forall_{A_{1},\ldots,A_{m},B,C,D_{1},\ldots,D_{n}|B=FALSE}\Big[\big(A_{1}\oplus \cdots \oplus A_{m} \oplus B \oplus C \oplus D_{1} \oplus \cdots \oplus D_{n}\big) = \big(A_{1}\oplus \cdots \oplus A_{m} \oplus C \oplus D_{1} \oplus \cdots \oplus D_{n}\big)\Big]$