Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-df-3xor Structured version   Visualization version   GIF version

Theorem wl-df-3xor 37383
Description: Alternative definition of whad 1590 based on hadifp 1602. See df-had 1591 to learn how it is currently introduced. The only use case so far is being a binary addition primitive for df-sad 16491. 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 37398).

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 1591, 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.)

Assertion
Ref Expression
wl-df-3xor (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ (𝜓𝜒), (𝜓𝜒)))

Proof of Theorem wl-df-3xor
StepHypRef Expression
1 hadifp 1602 . 2 (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓𝜒), (𝜓𝜒)))
2 xnor 1510 . . . . 5 ((𝜓𝜒) ↔ ¬ (𝜓𝜒))
32a1i 11 . . . 4 (⊤ → ((𝜓𝜒) ↔ ¬ (𝜓𝜒)))
4 biidd 262 . . . 4 (⊤ → ((𝜓𝜒) ↔ (𝜓𝜒)))
53, 4ifpbi23d 1080 . . 3 (⊤ → (if-(𝜑, (𝜓𝜒), (𝜓𝜒)) ↔ if-(𝜑, ¬ (𝜓𝜒), (𝜓𝜒))))
65mptru 1544 . 2 (if-(𝜑, (𝜓𝜒), (𝜓𝜒)) ↔ if-(𝜑, ¬ (𝜓𝜒), (𝜓𝜒)))
71, 6bitri 275 1 (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ (𝜓𝜒), (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  if-wif 1063  wxo 1508  wtru 1538  haddwhad 1590
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 207  df-an 396  df-or 847  df-ifp 1064  df-xor 1509  df-tru 1540  df-had 1591
This theorem is referenced by:  wl-df3xor2  37384  wl-3xortru  37386  wl-3xorfal  37387
  Copyright terms: Public domain W3C validator