Boole's expansion theorem

Boole's expansion theorem, often referred to as the Shannon expansion or decomposition, is the identity: , where  is any Boolean function,  is a variable,  is the complement of , and and  are  with the argument  set equal to  and to  respectively.

The terms  and  are sometimes called the positive and negative Shannon cofactors, respectively, of  with respect to . These are functions, computed by restrict operator,  and  (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 (BDDs), satisfiability solvers, and many other techniques relevant to computer engineering and formal verification of digital circuits.
In such engineering contexts (especially in BDDs), the expansion is interpreted as a if-then-else, with the variable  being the condition and the cofactors being the branches ( when  is true and respectively  when  is false).

Statement of the theorem
A more explicit way of stating the theorem is:

Variations and implications 
 XOR-Form  The statement also holds when the disjunction "+" is replaced by the XOR operator:
 
 Dual form There is a dual form of the Shannon expansion (which does not have a related XOR form):
 

Repeated application for each argument leads to the Sum of Products (SoP) canonical form of the Boolean function . For example for  that would be

Likewise, application of the dual form leads to the Product of Sums (PoS) canonical form (using the distributivity law of  over ):

Properties of cofactors 

 Linear properties of cofactors:
 For a Boolean function F which is made up of two Boolean functions G and H the following are true:
 If  then 
 If  then 
 If  then 
 If  then 
 Characteristics of unate functions:
 If F is a unate function and...
 If F is positive unate then 
 If F is negative unate then

Operations with cofactors 

 Boolean difference:
 The Boolean difference or Boolean derivative of the function F with respect to the literal x is defined as:
 
 Universal quantification:
 The universal quantification of F is defined as:
 
 Existential quantification:
 The existential quantification of F is defined as:

History
George Boole presented this expansion as his Proposition II, "To expand or develop a function involving any number of logical symbols", in his Laws of Thought (1854), and it was "widely applied by Boole and other nineteenth-century logicians".

Claude Shannon mentioned this expansion, among other Boolean identities, in a 1949 paper, and showed the switching network interpretations of the identity.  In the literature of computer design and switching theory, the identity is often incorrectly attributed to Shannon.

Application to switching circuits
 Binary decision diagrams follow from systematic use of this theorem
 Any Boolean function can be implemented directly in a switching circuit using a hierarchy of basic multiplexer by repeated application of this theorem.

References

See also
 Reed–Muller expansion

External links
 Shannon’s Decomposition Example with multiplexers.
 Optimizing Sequential Cycles Through Shannon Decomposition and Retiming (PDF) Paper on application.

Boolean algebra
Theorems in lattice theory