Metamath Proof Explorer

Theorem wl-df-3xor

Description: Alternative definition of whad based on hadifp . See df-had to learn how it is currently introduced. The only use case so far is being a binary addition primitive for df-sad . If inputs are viewed as binary digits (true is 1, false is 0), the result is what a binary single-bit addition with carry-in yields in the low bit of their sum.

The core meaning is to check whether an odd number of three inputs are true. The \/_ operation tests this for two inputs. So, if the first input is true, the two remaining inputs need to amount to an even (or: not an odd) number, else to an odd number.

The idea of an odd number of inputs being true carries over to other than 3 inputs by recursion: In an informal notation we depend the case with n+1 inputs, ph being the additional one, recursively on that of n inputs: "(n+1)-xor" <-> if- ( ph , -. "n-xor" , "n-xor" ) . The base case is "0-xor" being F. , because zero inputs never contain an odd number among them. Then we find, after simplifying, in our informal notation:

"2-xor" ( ph , ps ) <-> ( ph \/_ ps ) (see wl-2xor ).

Our definition here follows exactly the above pattern.

In microprocessor technology an addition limited to a range (a one-bit range in our case) is called a "wrap-around operation". The name "had", as in df-had , by contrast, is somehow suggestive of a "half adder" instead. Such a circuit, for one, takes two inputs only, no carry-in, and then yields two outputs - both sum and carry. That's why we use "3xor" instead of "had" here. (Contributed by Wolf Lammen, 24-Apr-2024)

Ref Expression
Assertion wl-df-3xor ⊢ hadd φ ψ χ ↔ if- φ ¬ ψ ⊻ χ ψ ⊻ χ

Proof

Step Hyp Ref Expression
1 hadifp ⊢ hadd φ ψ χ ↔ if- φ ψ ↔ χ ψ ⊻ χ
2 xnor ⊢ ψ ↔ χ ↔ ¬ ψ ⊻ χ
3 2 a1i ⊢ ⊤ → ψ ↔ χ ↔ ¬ ψ ⊻ χ
4 biidd ⊢ ⊤ → ψ ⊻ χ ↔ ψ ⊻ χ
5 3 4 ifpbi23d ⊢ ⊤ → if- φ ψ ↔ χ ψ ⊻ χ ↔ if- φ ¬ ψ ⊻ χ ψ ⊻ χ
6 5 mptru ⊢ if- φ ψ ↔ χ ψ ⊻ χ ↔ if- φ ¬ ψ ⊻ χ ψ ⊻ χ
7 1 6 bitri ⊢ hadd φ ψ χ ↔ if- φ ¬ ψ ⊻ χ ψ ⊻ χ