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- ( 𝜑 , ¬ ( 𝜓 ⊻ 𝜒 ) , ( 𝜓 ⊻ 𝜒 ) ) ) |
| 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- ( 𝜑 , ¬ ( 𝜓 ⊻ 𝜒 ) , ( 𝜓 ⊻ 𝜒 ) ) ) |