Skip to content

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.

Engine name: Reference expansionFR: Expansion d'une référenceDE: Expansion eines Verweises

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

eligible := A OR B
#ABCeligiblelhsrhs
0FALSEFALSEFALSEFALSEFALSEFALSE
1FALSEFALSETRUEFALSEFALSEFALSE
2FALSETRUEFALSETRUEFALSEFALSE
3FALSETRUETRUETRUETRUETRUE
4TRUEFALSEFALSETRUEFALSEFALSE
5TRUEFALSETRUETRUETRUETRUE
6TRUETRUEFALSETRUEFALSEFALSE
7TRUETRUETRUETRUETRUETRUE
lhs ≡ rhs holds · lhs and rhs agree on every assignment. · Exhaustively checked and solver cross-checked · 8 rows

The same law in four notations

Wordseligible AND C
Programmingeligible && C
Mathematicaleligible ∧ C
Algebraeligible·C
LaTeX\mathit{eligible} \cdot C
Words(A OR B) AND C
Programming(A || B) && C
Mathematical(A ∨ B) ∧ C
Algebra(A + B)·C
LaTeX\left(A + B\right) \cdot C
eligible := A OR B eligible := A OR B A B C eligiblePRIMARY lhs rhs OR AND AND OR
eligible := A OR B eligible := A OR B A B C eligiblePRIMARY lhs rhs OR AND AND OR

Proof by truth table: eligible AND C = (A OR B) AND C

eligible AND C = (A OR B) AND C
#ABCeligiblelhsrhs
0FALSEFALSEFALSEFALSEFALSEFALSE
1FALSEFALSETRUEFALSEFALSEFALSE
2FALSETRUEFALSETRUEFALSEFALSE
3FALSETRUETRUETRUETRUETRUE
4TRUEFALSEFALSETRUEFALSEFALSE
5TRUEFALSETRUETRUETRUETRUE
6TRUETRUEFALSETRUEFALSEFALSE
7TRUETRUETRUETRUETRUETRUE
lhs ≡ rhs holds · lhs and rhs agree on every assignment. · Exhaustively checked and solver cross-checked · 8 rows

The same law in four notations

Wordseligible AND C
Programmingeligible && C
Mathematicaleligible ∧ C
Algebraeligible·C
LaTeX\mathit{eligible} \cdot C
Words(A OR B) AND C
Programming(A || B) && C
Mathematical(A ∨ B) ∧ C
Algebra(A + B)·C
LaTeX\left(A + B\right) \cdot C
eligible AND C = (A OR B) AND C eligible AND C = (A OR B) AND C A B C eligiblePRIMARY lhs rhs OR AND AND OR
eligible AND C = (A OR B) AND C eligible AND C = (A OR B) AND C A B C eligiblePRIMARY lhs rhs OR AND AND OR

Questions

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

See also

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.