Theorem wl-df-3xor 35566

Description: Alternative definition of whad 1595 based on hadifp 1608. See df-had 1596 to learn how it is currently introduced. The only use case so far is being a binary addition primitive for df-sad 16086. 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 35581).

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 1596, 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

Step	Hyp	Ref	Expression
1		hadifp 1608	. 2 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)))
2		xnor 1505	. . . . 5 ⊢ ((𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ⊻ 𝜒))
3	2	a1i 11	. . . 4 ⊢ (⊤ → ((𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ⊻ 𝜒)))
4		biidd 261	. . . 4 ⊢ (⊤ → ((𝜓 ⊻ 𝜒) ↔ (𝜓 ⊻ 𝜒)))
5	3, 4	ifpbi23d 1078	. . 3 ⊢ (⊤ → (if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒))))
6	5	mptru 1546	. 2 ⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒)))
7	1, 6	bitri 274	1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒)))

Syntax hints:  ¬ wn 3   ↔ wb 205  if-wif 1059   ⊻ wxo 1503  ⊤wtru 1540  haddwhad 1595

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 206  df-an 396  df-or 844  df-ifp 1060  df-xor 1504  df-tru 1542  df-had 1596

This theorem is referenced by:  wl-df3xor2  35567  wl-3xortru  35569  wl-3xorfal  35570