Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-df-3xor | Structured version Visualization version GIF version |
Description: Alternative definition of
whad 1594 based on hadifp 1607. See df-had 1595 to
learn how it is currently introduced. The only use case so far is being a
binary addition primitive for df-sad 15810. 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, 𝜑 being the additional one, recursively on that of n inputs: "(n+1)-xor" ↔ if-(𝜑, ¬ "n-xor" , "n-xor" ). The base case is "0-xor" being ⊥, because zero inputs never contain an odd number among them. Then we find, after simplifying, in our informal notation: "2-xor" (𝜑, 𝜓) ↔ (𝜑 ⊻ 𝜓) (see wl-2xor 35051). 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 1595, 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 |
---|---|
wl-df-3xor | ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hadifp 1607 | . 2 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒))) | |
2 | xnor 1504 | . . . . 5 ⊢ ((𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ⊻ 𝜒)) | |
3 | 2 | a1i 11 | . . . 4 ⊢ (⊤ → ((𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ⊻ 𝜒))) |
4 | biidd 265 | . . . 4 ⊢ (⊤ → ((𝜓 ⊻ 𝜒) ↔ (𝜓 ⊻ 𝜒))) | |
5 | 3, 4 | ifpbi23d 1077 | . . 3 ⊢ (⊤ → (if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒)))) |
6 | 5 | mptru 1545 | . 2 ⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒))) |
7 | 1, 6 | bitri 278 | 1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 if-wif 1058 ⊻ wxo 1502 ⊤wtru 1539 haddwhad 1594 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ifp 1059 df-xor 1503 df-tru 1541 df-had 1595 |
This theorem is referenced by: wl-df3xor2 35037 wl-3xortru 35039 wl-3xorfal 35040 |
Copyright terms: Public domain | W3C validator |