Counting-constraint expansion: AT_LEAST(2; A, B, C) = (A AND B) OR (A AND C) OR (B AND C)
Counting-constraint expansion rewrites AT_LEAST(k; …), AT_MOST(k; …) and EXACTLY(k; …) over their operands with AND, OR and NOT, so that normal forms, Karnaugh maps and gate bases can work on a plain formula: AT_LEAST(2; A, B, C) = (A AND B) OR (A AND C) OR (B AND C).
A counting constraint is rewritten over its operands: "at least k" is built by counting the operands one by one with AND and OR, "at most k" is the negation of "at least k + 1", and "exactly k" is both.
A counting constraint takes two or more operand formulas and a whole number k, and is TRUE when at least, at most or exactly k of the operands are TRUE. The engine evaluates it by counting, draws it as one gate (≥2, ≤2, =2) and reads it literally as “at least 2 of A, B, C”. The expansion is the named step that replaces the gate by ordinary operators when a transformation needs them: “at least k” is built by counting the operands one by one with AND and OR, “at most k” is the negation of “at least k + 1”, and “exactly k” is the AND of the two.
For three operands and k = 2 the expansion is the majority function, the OR of the three pairs, and the equivalence check on this page confirms the identity on all eight rows. For “exactly one” it gives the three-term formula of the worked example, and for “at most one” the negation of a majority. The expanded form grows with the number of operands, so the step runs within the normal-form limits and reports “Not determined” beyond them rather than a partial formula.
The law matters for reading results: a simplification, a CNF or DNF, a Karnaugh map or a NAND-only form of a rule with a count is computed on the expansion, and the step name tells you so. Score thresholds, which compare a points total with a cutoff, are not expanded by this law; they stay references unless you ask for their expansion.
Statement
AT_LEAST(2; A, B, C) = (A AND B) OR (A AND C) OR (B AND C) Proof by truth table: AT_LEAST(2; A, B, C) = (A AND B) OR (A AND C) OR (B AND C)
| # | A | B | C | lhs | rhs |
|---|---|---|---|---|---|
| 0 | FALSE | FALSE | FALSE | FALSE | FALSE |
| 1 | FALSE | FALSE | TRUE | FALSE | FALSE |
| 2 | FALSE | TRUE | FALSE | FALSE | FALSE |
| 3 | FALSE | TRUE | TRUE | TRUE | TRUE |
| 4 | TRUE | FALSE | FALSE | FALSE | FALSE |
| 5 | TRUE | FALSE | TRUE | TRUE | TRUE |
| 6 | TRUE | TRUE | FALSE | TRUE | TRUE |
| 7 | TRUE | TRUE | TRUE | TRUE | TRUE |
The same law in four notations
AT_LEAST(2; A, B, C)AT_LEAST(2; A, B, C)AT_LEAST(2; A, B, C)AT_LEAST(2; A, B, C)\mathrm{count}_{\geq 2}(A, B, C)(A AND B) OR (A AND C) OR (B AND C)(A && B) || (A && C) || (B && C)(A ∧ B) ∨ (A ∧ C) ∨ (B ∧ C)(A·B) + (A·C) + (B·C)\left(A \cdot B\right) + \left(A \cdot C\right) + \left(B \cdot C\right)The common slip
Writing “at least two of three” as A XOR B XOR C, or “exactly one” as the same chain. A chain of XOR is parity, TRUE for one or for three true operands; the expansion of AT_LEAST(2; A, B, C) is the three pairs, and the equivalence checker reports the rows where the chain differs.
Questions
Why not always write the expansion by hand?
Because it grows quickly: at least three of six operands is twenty triples, while the count stays one gate however many operands it has. The expansion exists so that the algebra can still run; the gate is the form to read, test and export.
Does the expansion change what the rule means?
No. It is an identity, checked by the exact equivalence checker on every assignment of the operands, like every other law on these pages. Only the shape changes.
Related
Tools
- Boolean algebra calculator and simplifier with steps (every law named and verified)
- Logical equivalence checker: two expressions, exact verdict, counterexample
See also
- Majority of three (2-out-of-3 voting): truth table, K-map and NAND form
- Quorum: at least three of four, truth table and K-map
- Exactly one of three: why XOR is the wrong tool
- XOR of three inputs is odd parity, not “exactly one”
- Lesson 13: Categories, scales, and counting (intermediate, 20 min)
- Minterm expansion: the canonical sum of products (Σm)
Laws
Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build . Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.