Theorem wl-df-3xor 37845

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

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 1602, 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 1613	. 2 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)))
2		xnor 1521	. . . . 5 ⊢ ((𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ⊻ 𝜒))
3	2	a1i 11	. . . 4 ⊢ (⊤ → ((𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ⊻ 𝜒)))
4		biidd 264	. . . 4 ⊢ (⊤ → ((𝜓 ⊻ 𝜒) ↔ (𝜓 ⊻ 𝜒)))
5	3, 4	ifpbi23d 1086	. . 3 ⊢ (⊤ → (if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒))))
6	5	mptru 1555	. 2 ⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒)))
7	1, 6	bitri 277	1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒)))

Syntax hints:  ¬ wn 3   ↔ wb 208  if-wif 1069   ⊻ wxo 1519  ⊤wtru 1549  haddwhad 1601

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 398  df-or 855  df-ifp 1070  df-xor 1520  df-tru 1551  df-had 1602

This theorem is referenced by:  wl-df3xor2  37846  wl-3xortru  37848  wl-3xorfal  37849