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 15793. 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 1085, and "(at least) 3 out
of 3", expressed by triple conjunction df-3an 1086.
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 34901), and
"2-mintru-1" (𝜓, 𝜒) ↔ (𝜓 ∨ 𝜒) (wl-2mintru1 34900). Plugging
these expressions into the formula above for n = 3, m = 2 yields exactly
our definition here. (Contributed by Wolf Lammen,
2-May-2024.) |