Named-output reference expansion (Tangibool rewriting step)
Reference expansion replaces a named output used inside another formula by its definition, so eligible AND C with eligible := A OR B becomes (A OR B) AND C.
A named output used in a formula is replaced by its definition.
A Tangibool model can define several outputs and let one refer to another by name. Checks, simplification and exports work on the expanded form, and the expansion is recorded as a step under this law's name. The identity on this page is proved like any other: the engine builds a model with the definition and both formulas and checks them equivalent on every row.
Reference expansion is what lets a long rule be written as a few readable named parts without changing what it computes, and it is why renaming a definition updates every reference: references are held by identity, not by text. The page is an internal step reference rather than a law students look up, so it is not indexed.
Statement
eligible := A OR Beligible AND C = (A OR B) AND C Proof by truth table: eligible := A OR B
| # | A | B | C | eligible | lhs | rhs |
|---|---|---|---|---|---|---|
| 0 | FALSE | FALSE | FALSE | FALSE | FALSE | FALSE |
| 1 | FALSE | FALSE | TRUE | FALSE | FALSE | FALSE |
| 2 | FALSE | TRUE | FALSE | TRUE | FALSE | FALSE |
| 3 | FALSE | TRUE | TRUE | TRUE | TRUE | TRUE |
| 4 | TRUE | FALSE | FALSE | TRUE | FALSE | FALSE |
| 5 | TRUE | FALSE | TRUE | TRUE | TRUE | TRUE |
| 6 | TRUE | TRUE | FALSE | TRUE | FALSE | FALSE |
| 7 | TRUE | TRUE | TRUE | TRUE | TRUE | TRUE |
The same law in four notations
eligible AND Celigible && Celigible ∧ Celigible·C\mathit{eligible} \cdot C(A OR B) AND C(A || B) && C(A ∨ B) ∧ C(A + B)·C\left(A + B\right) \cdot CProof by truth table: eligible AND C = (A OR B) AND C
| # | A | B | C | eligible | lhs | rhs |
|---|---|---|---|---|---|---|
| 0 | FALSE | FALSE | FALSE | FALSE | FALSE | FALSE |
| 1 | FALSE | FALSE | TRUE | FALSE | FALSE | FALSE |
| 2 | FALSE | TRUE | FALSE | TRUE | FALSE | FALSE |
| 3 | FALSE | TRUE | TRUE | TRUE | TRUE | TRUE |
| 4 | TRUE | FALSE | FALSE | TRUE | FALSE | FALSE |
| 5 | TRUE | FALSE | TRUE | TRUE | TRUE | TRUE |
| 6 | TRUE | TRUE | FALSE | TRUE | FALSE | FALSE |
| 7 | TRUE | TRUE | TRUE | TRUE | TRUE | TRUE |
The same law in four notations
eligible AND Celigible && Celigible ∧ Celigible·C\mathit{eligible} \cdot C(A OR B) AND C(A || B) && C(A ∨ B) ∧ C(A + B)·C\left(A + B\right) \cdot CQuestions
Can references form a cycle?
No. The engine rejects a definition that refers to itself directly or through other outputs (the validation code is “cycle”), because such a model has no value to compute.
Related
Tools
- Boolean algebra calculator and simplifier with steps (every law named and verified)
- Logical equivalence checker: two expressions, exact verdict, counterexample
See also
- Subcircuit expansion (Tangibool rewriting step)
- Traffic-light safety property: never both greens, checked as “always true”
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.