A ternary boolean function

A binary boolean function

Positive Shannon cofactor of a boolean function, with respect to its first argument

Negative Shannon cofactor of a boolean function, with respect to its first argument

Shannon's expansion over the first argument of a function. We have:

>>> shannon
Q.E.D.

Alternative form of Shannon's expansion over the first argument of a function. We have:

>>> shannon2
Q.E.D.

Computing the derivative of a boolean function (boolean difference). Defined as exclusive-or of Shannon cofactors with respect to that variable.

The no-wiggle theorem: If the derivative of a function with respect to a variable is constant False, then that variable does not "wiggle" the function; i.e., any changes to it won't affect the result of the function. In fact, we have an equivalence: The variable only changes the result of the function iff the derivative with respect to it is not False:

>>> noWiggle
Q.E.D.

Universal quantification of a boolean function with respect to a variable. Simply defined as the conjunction of the Shannon cofactors.

Show that universal quantification is really meaningful: That is, if the universal quantification with respect to a variable is True, then both cofactors are true for those arguments. Of course, this is a trivial theorem if you think about it for a moment, or you can just let SBV prove it for you:

>>> univOK
Q.E.D.

Existential quantification of a boolean function with respect to a variable. Simply defined as the conjunction of the Shannon cofactors.

Show that existential quantification is really meaningful: That is, if the existential quantification with respect to a variable is True, then one of the cofactors must be true for those arguments. Again, this is a trivial theorem if you think about it for a moment, but we will just let SBV prove it:

>>> existsOK
Q.E.D.