Boole's expansion theorem

Boole's expansion theorem, often referred to as the Shannon expansion or Shannon decomposition, is the identity ${\displaystyle F=x\cdot F_{x}+x'\cdot F_{x'}}$, where ${\displaystyle F}$ is any Boolean function, ${\displaystyle x}$ is a variable, ${\displaystyle x'}$ is the complement of ${\displaystyle x}$, and ${\displaystyle F_{x}}$and ${\displaystyle F_{x'}}$ are ${\displaystyle F}$ with the argument ${\displaystyle x}$ set equal to ${\displaystyle 1}$ and to ${\displaystyle 0}$ respectively.

The terms ${\displaystyle F_{x}}$ and ${\displaystyle F_{x'}}$ are sometimes called the positive and negative Shannon cofactors, respectively, of ${\displaystyle F}$ with respect to ${\displaystyle x}$. These are functions, computed by the ${\displaystyle \operatorname {restrict} }$ operator, ${\displaystyle \operatorname {restrict} (F,x,0)}$ and ${\displaystyle \operatorname {restrict} (F,x,1)}$. (See also valuation and partial application.)

The theorem has been called the "fundamental theorem of Boolean algebra". Besides its theoretical importance, it paved the way for binary decision diagrams (BDDs), satisfiability solvers, and many other techniques relevant to computer engineering and formal verification of digital circuits. In such contexts, particularly in BDDs, the expansion is interpreted as an if-then-else, with the variable ${\displaystyle x}$ being the condition and the cofactors being the branches (${\displaystyle F_{x}}$ when ${\displaystyle x}$ is true and respectively ${\displaystyle F_{x'}}$ when ${\displaystyle x}$ is false).