Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-df-had | Structured version Visualization version GIF version |
Description: Alternative definition of
whad 1593 based on hadifp 1606. See df-had 1594 to
learn how it is currently introduced.
Check whether an odd number of three inputs are true. The ⊻ operation tests this for two inputs, and for evenness we can use ↔. So, if the first input is true, the two remaining inputs need to amount to an even number, else to an odd number. If the inputs are viewed as binary digits (true is 1, false is 0), the result is what a binary full addition leaves in the lowest bit of their sum. That is what the name "had" is derived from: "half adder". (Contributed by Wolf Lammen, 24-Apr-2024.) |
Ref | Expression |
---|---|
wl-df-had | ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hadifp 1606 | 1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 if-wif 1057 ⊻ wxo 1501 haddwhad 1593 |
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 209 df-an 399 df-or 844 df-ifp 1058 df-xor 1502 df-had 1594 |
This theorem is referenced by: wl-had1 34762 wl-had0 34763 wl-dfhad2 34764 |
Copyright terms: Public domain | W3C validator |