Boole's expansion theorem

The terms F x {displaystyle F_{x}} and F x ′ {displaystyle F_{x'}} are sometimes called the positive and negative Shannon cofactors, respectively, of F {displaystyle F} with respect to x {displaystyle x} . These are functions, computed by restrict operator, restrict ⁡ ( F , x , 0 ) {displaystyle operatorname {restrict} (F,x,0)} and restrict ⁡ ( F , x , 1 ) {displaystyle operatorname {restrict} (F,x,1)} (see valuation (logic) and partial application). It has been called the 'fundamental theorem of Boolean algebra'. Besides its theoretical importance, it paved the way for binary decision diagrams, satisfiability solvers, and many other techniques relevant to computer engineering and formal verification of digital circuits.