Let \(f, g : (\mathrm{Fin}\, n \to \mathrm{Bool}) \to \mathrm{Bool}\) be two Boolean functions that agree at every point, so that \(f(x) = g(x)\) for all \(x\). Then for every restriction \(\rho \) on \(n\) variables, the restricted functions coincide: the restriction of \(f\) by \(\rho \) equals the restriction of \(g\) by \(\rho \).

Let \(f, g : (\mathrm{Fin}\, n \to \mathrm{Bool}) \to \mathrm{Bool}\) be Boolean functions on \(n\) variables that agree at every input, and fix a real parameter \(p\) and a threshold \(t \in \mathbb {N}\). Then the Bernoulli(\(p\)) restriction probability of the event that a random restriction \(\rho \) produces a restricted function of decision-tree depth strictly greater than \(t\) is the same for \(f\) as for \(g\).

Let \(t\) be a term over \(n\) variables, that is, a list of literals, each a variable in \(\{ 0,\dots ,n-1\} \) together with a negation flag. Form a new term \(t'\) by scanning \(t\) and retaining a literal exactly when no already-retained literal has the same variable, discarding any literal whose variable has already occurred. Then \(t'\) has no repeated literal: no literal occurs twice in \(t'\).

Let \(t\) be a term over \(n\) variables, that is, a list of literals, each literal consisting of a variable in \(\{ 0,1,\dots ,n-1\} \) together with a negation flag. Let \(t'\) be the de-duplicated term obtained by scanning \(t\) and retaining each literal only when no earlier-retained literal already uses the same variable. Then within \(t'\) the variable of a literal determines that literal: any two literals \(l_1, l_2 \in t'\) whose variables agree are equal, that is, they have the same variable and the same negation flag.

Let \(t\) be a term, that is, a finite list of literals over the variables \(\{ 0, 1, \dots , n-1\} \), and let \(t'\) be the term obtained from \(t\) by scanning it and keeping each literal only when no literal already kept uses the same variable. Then \(t'\) has length at most that of \(t\).

Let \(t\) be a term (a conjunction of literals) over the variables \(x_0,\dots ,x_{n-1}\). If \(t\) contains two literals on the same variable with opposite polarities — one negated and one not — then \(t\) evaluates to false under every assignment \(x : \{ 0,\dots ,n-1\} \to \{ \mathrm{true},\mathrm{false}\} \).

Let \(t\) be a term over \(n\) variables, that is, a list of literals \(l\), each carrying a variable \(l.\mathrm{var} \in \{ 0,\dots ,n-1\} \) and a polarity flag, and interpreted conjunctively: \(t\) evaluates to true on an assignment \(x \in \{ 0,1\} ^n\) exactly when every literal in \(t\) holds under \(x\). Suppose \(t\) is consistent, meaning it contains no two literals on the same variable with opposite polarities. Let \(t'\) be the term obtained from \(t\) by keeping, for each variable, only its first occurrence and discarding every later literal whose variable has already appeared. Then \(t'\) and \(t\) have the same value on every assignment \(x\).

Let \(d\) be a DNF formula in \(n\) Boolean variables — a disjunction of terms, each term a conjunction of literals over the variables \(\{ 0,\dots ,n-1\} \) — and form the cleaned formula by first discarding every term that contains some variable together with its negation, and then, in each surviving term, keeping only the first literal on each variable and deleting any later literal repeating that variable. Then the cleaned formula and \(d\) compute the same Boolean function: for every assignment \(x \colon \{ 0,\dots ,n-1\} \to \{ \mathrm{true},\mathrm{false}\} \), the cleaned formula evaluates to true at \(x\) if and only if \(d\) does.

Let \(t\) be a term over \(n\) Boolean variables — a list of literals, each a variable together with a polarity — and suppose \(t\) contains two literals on the same variable with opposite polarities, one negated and one not. Then, read as a single clause under disjunction semantics, \(t\) evaluates to true under every assignment \(x : \{ 0,\dots ,n-1\} \to \{ \mathrm{true},\mathrm{false}\} \); that is, some literal of \(t\) holds under \(x\), for every \(x\).

Let \(t\) be a term over the variables \(x_0,\dots ,x_{n-1}\), that is, a list of literals, and let \(x \in \{ 0,1\} ^n\) be an assignment. Suppose \(t\) contains no two literals on the same variable with opposite polarities. Let \(t'\) be the term obtained from \(t\) by scanning it and keeping a literal only when no earlier-kept literal uses the same variable, so that each variable of \(t\) occurs at most once in \(t'\). Then \(t'\) and \(t\) have the same value as a clause under \(x\): some literal of \(t'\) is satisfied by \(x\) if and only if some literal of \(t\) is.

Represent a CNF formula over the variables indexed by \(\{ 0,1,\dots ,n-1\} \) as a conjunction of clauses, each clause being a disjunction of literals, where a literal is a variable or its negation. Cleaning such a formula proceeds in two steps: first delete every clause that contains some variable together with both polarities (one literal negated, one not), and then, within each surviving clause, keep a literal only when its variable has not already occurred among the literals retained earlier in that clause. Then for every CNF formula \(c\) and every Boolean assignment \(x \colon \{ 0,\dots ,n-1\} \to \{ \mathrm{true},\mathrm{false}\} \), the cleaned formula and \(c\) take the same Boolean value at \(x\).

Let \(d\) be a DNF formula over \(n\) variables — a disjunction of terms, each term a conjunction of literals — and form its cleaned version by first deleting every contradictory term (one containing a variable together with its negation) and then, in each surviving term, discarding any literal whose variable already occurs in an earlier retained literal of that term. The width of a term is its number of literals, and the width of a formula is the largest width of any of its terms (with width \(0\) for the empty formula). Then the width of the cleaned formula is at most the width of \(d\).

Let \(c\) be a CNF formula, that is, a list of clauses, each clause being a list of literals over the variables \(\{ 0,\dots ,n-1\} \). Define the width of a clause to be its number of literals and the width of \(c\) to be the maximum width among its clauses (and \(0\) if \(c\) has no clauses). Form the cleaned formula from \(c\) by discarding every clause that contains some variable together with both of its polarities, and then, within each surviving clause, keeping only the first occurrence of each variable and deleting all later literals on a variable already seen. Then the width of the cleaned formula is at most the width of \(c\).

Let \(d\) be a DNF formula over \(n\) variables — a list of terms, each term a list of literals, where a literal names a variable in \(\{ 0,\dots ,n-1\} \) together with a polarity (negated or not). Form a new formula \(d'\) from \(d\) by first discarding every term that contains two literals on the same variable with opposite polarities, and then, in each surviving term, keeping only the first literal encountered on each variable and deleting all later literals that repeat an already-kept variable. Then in every term of \(d'\) the variable determines the literal: for any two literals \(l_1, l_2\) occurring in such a term, if \(l_1\) and \(l_2\) name the same variable, then \(l_1 = l_2\).

Let \(d\) be a DNF formula in \(n\) variables, and clean it by first deleting every term that contains some variable together with its negation, and then, within each surviving term, keeping only the first literal on each variable and discarding any later literal whose variable has already appeared. Every term of the resulting formula is then duplicate-free: no literal occurs twice in it, where two literals count as equal when they share both variable and polarity.

Let \(c\) be a CNF formula over the variable set \(\{ 0,\dots ,n-1\} \), and let \(\hat c\) be the formula obtained from \(c\) by first deleting every clause that contains some variable together with its negation, and then, in each surviving clause, keeping only one literal per variable. Then within any single clause of \(\hat c\) the variable of a literal determines that literal completely: if two literals of the clause share the same variable, they are equal (and in particular have the same polarity).

Let \(c\) be a CNF formula over \(n\) variables, and form its cleaned version by first discarding every clause that contains some variable both positively and negatively, and then deleting from each surviving clause every literal whose variable already occurs earlier in that clause. Then each clause of the resulting formula, viewed as a list of literals, contains no repeated literal.

Let \(C\) be a Boolean circuit on \(n\) variables of the form \(g(c_1,\dots ,c_k)\), a single gate \(g\) (either AND or OR) applied to a list of child circuits \(c_1,\dots ,c_k\). If the depth of \(C\) is at most \(1\), then every child \(c_i\) is a literal, that is, \(c_i = \ell _i\) for some literal \(\ell _i\) (a variable index together with a polarity).

Let \(g = \mathrm{node}(\mathit{isAnd}, cs)\) be a Boolean circuit consisting of a single gate (an AND gate if \(\mathit{isAnd}\) is true, an OR gate otherwise) applied to a list \(cs\) of child circuits, and suppose its depth satisfies \(\mathrm{depth}(g) \le 2\). Then every child circuit \(c\) in \(cs\) has depth \(\mathrm{depth}(c) \le 1\).

Let \(cs\) be a finite list of Boolean circuits on \(n\) variables, regarded as the children of a top-level OR gate \(\varphi \), and suppose \(\varphi \) has depth at most \(2\). Form a DNF \(D\) from \(cs\) by turning each literal child into a singleton term, each AND child into the single term consisting of all its literals, and each OR child into the collection of singleton terms of its literals (in each case reading a circuit literal as the corresponding DNF literal, keeping the same variable and polarity). Then \(D\) and \(\varphi \) compute the same Boolean function: \(D(x) = \varphi (x)\) for every assignment \(x \colon \{ 0,\dots ,n-1\} \to \{ \mathrm{true},\mathrm{false}\} \).

Let \(cs\) be a list of Boolean circuits on \(n\) variables, viewed as the children of a top-level AND gate, and suppose the AND-of-children circuit \(\bigwedge cs\) has depth at most \(2\). Then the depth-\(2\) AND-to-CNF conversion applied to \(cs\) produces a CNF formula computing the same Boolean function as \(\bigwedge cs\): for every assignment \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\), the value of the resulting CNF at \(x\) equals the value of \(\bigwedge cs\) at \(x\).

Let \(cs\) be a list of Boolean circuits on \(n\) variables, regarded as the children of a top-level OR gate, and suppose that this OR gate has depth at most \(2\). Form the DNF obtained from \(cs\) by converting each literal child into a singleton term, each AND child into the term consisting of its literals, and each OR child into the singleton terms of its literals. Then the width of this DNF (the maximum number of literals in any of its terms) is at most the maximum fan-in of the OR gate.

Let \(cs\) be a list of Boolean circuits on \(n\) variables, regarded as the children of a top AND gate, and suppose this AND gate has depth at most \(2\). Then the CNF formula obtained by converting these children — each literal child becoming a singleton clause, each OR child the clause of its literals, and each AND child contributing the singleton clauses of its literals — has width at most the maximum fanin of the AND gate.