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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hadifp | ||
2 | xnor | ||
3 | 2 | a1i | |
4 | biidd | ||
5 | 3 4 | ifpbi23d | |
6 | 5 | mptru | |
7 | 1 6 | bitri |