Theorem wl-df-3mintru2 35655

Description: Alternative definition of wcad 1608. See df-cad 1609 to learn how it is currently introduced. The only use case so far is being a binary addition primitive for df-sad 16158. If inputs are viewed as binary digits (true is 1, false is 0), the result is whether ordinary binary full addition yields a carry bit. That is what the name df-cad 1609 is derived from: "carry of an addition". Here we stick with this abbreviated form of our notation above, but still use "adder carry" as a shorthand for "at least 2 out of 3" in text.

The core meaning is to check whether at least two of three inputs are true. So, if the first input is true, at least one of the two remaining must be true, else even both. This theorem is the in-between of "at least 1 out of 3", given by triple disjunction df-3or 1087, and "(at least) 3 out of 3", expressed by triple conjunction df-3an 1088.

The notion above can be generalized to other input numbers with other minimum values as follows. Let us introduce informally a logical operation "n-mintru-m" taking n inputs, and requiring at least m of them be true to let the operation itself be true. There now exists a recursive scheme to define it for increasing n, m. We start with the base case n = 0. Here "n-mintru-0" is equivalent to ⊤ (any sequence of inputs contains at least zero true inputs), the other "0-mintru-m" is for any m > 0 equivalent to ⊥, because a sequence of zero inputs never has a positive number of them true. The general case adds a new input 𝜑 to a given sequence of n inputs, and reduces that case for all integers m to that of the smaller sequence by recursion, informally written as:

"(n+1)-mintru-(m+1)" ↔ if-(𝜑, "n-mintru-m" , "n-mintru-(m+1)" )

Our definition here matches "3-mintru-2" with inputs 𝜑, 𝜓 and 𝜒. Starting from the base cases we find after simplifications: "2-mintru-2" (𝜓, 𝜒) ↔ (𝜓 ∧ 𝜒) (wl-2mintru2 35662), and "2-mintru-1" (𝜓, 𝜒) ↔ (𝜓 ∨ 𝜒) (wl-2mintru1 35661). Plugging these expressions into the formula above for n = 3, m = 2 yields exactly our definition here. (Contributed by Wolf Lammen, 2-May-2024.)

Assertion

Ref	Expression
wl-df-3mintru2	⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ∨ 𝜒), (𝜓 ∧ 𝜒)))

Proof of Theorem wl-df-3mintru2

Step	Hyp	Ref	Expression
1		cadrot 1616	. 2 ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ cadd(𝜓, 𝜒, 𝜑))
2		cadifp 1622	. 2 ⊢ (cadd(𝜓, 𝜒, 𝜑) ↔ if-(𝜑, (𝜓 ∨ 𝜒), (𝜓 ∧ 𝜒)))
3	1, 2	bitri 274	1 ⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ∨ 𝜒), (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∨ wo 844  if-wif 1060  caddwcad 1608

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 397  df-or 845  df-ifp 1061  df-3or 1087  df-3an 1088  df-xor 1507  df-cad 1609

This theorem is referenced by:  wl-df2-3mintru2  35656  wl-df3-3mintru2  35657  wl-df3maxtru1  35663