Theorem wl-df-3xor 38359

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

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 1624, 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 1637	. 2 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)))
2		xnor 1543	. . . . 5 ⊢ ((𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ⊻ 𝜒))
3	2	a1i 11	. . . 4 ⊢ (⊤ → ((𝜓 ↔ 𝜒) ↔ ¬ (𝜓 ⊻ 𝜒)))
4		biidd 265	. . . 4 ⊢ (⊤ → ((𝜓 ⊻ 𝜒) ↔ (𝜓 ⊻ 𝜒)))
5	3, 4	ifpbi23d 1096	. . 3 ⊢ (⊤ → (if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒))))
6	5	mptru 1577	. 2 ⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒)))
7	1, 6	bitri 278	1 ⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ (𝜓 ⊻ 𝜒), (𝜓 ⊻ 𝜒)))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  if-wif 1078   ⊻ wxo 1541  ⊤wtru 1571  haddwhad 1623

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ifp 1079  df-xor 1542  df-tru 1573  df-had 1624

This theorem is used by:  wl-df3xor2  38360  wl-3xortru  38362  wl-3xorfal  38363