Fix a width \(w \ge 1\) and an index \(\mathrm{idx} \lt w\), together with a direction bit \(\mathrm{dir}\) and an arbitrary list of remaining entries \(\mathrm{rest}\). Parsing the list that begins with the entry \((\mathrm{idx}, \mathrm{dir})\), followed immediately by the termination marker \((w, \mathrm{false})\), and then by \(\mathrm{rest}\), produces the triple \((\mathrm{idx}, \mathrm{dir}, \mathrm{true})\) — with \(\mathrm{idx}\) viewed as an element of \(\{ 0, \dots , w-1\} \) and the final component recording that this entry is marked — prepended to the parse of \(\mathrm{rest}\).

Fix \(w \geq 1\), and consider parsing an aux list whose first two entries are \((\mathrm{idx}, \mathrm{dir})\) and \((\mathrm{idx}', \mathrm{dir}')\), both with in-range indices \(\mathrm{idx} \lt w\) and \(\mathrm{idx}' \lt w\), followed by any further list \(\mathrm{rest}\). Then parsing \((\mathrm{idx}, \mathrm{dir}) :: (\mathrm{idx}', \mathrm{dir}') :: \mathrm{rest}\) yields the triple \((\mathrm{idx}, \mathrm{dir}, \mathrm{false})\) — with no termination marker recorded — prepended to the parse of \((\mathrm{idx}', \mathrm{dir}') :: \mathrm{rest}\).

Fix \(w \ge 1\), and let \((\mathrm{idx}, \mathrm{dir})\) be a single entry whose index satisfies \(\mathrm{idx} \lt w\). Then parsing the one-element list \([(\mathrm{idx}, \mathrm{dir})]\) yields the singleton list \([(\mathrm{idx}, \mathrm{dir}, \mathrm{false})]\), where the index is viewed as an element of \(\{ 0, 1, \dots , w-1\} \) and the marker flag is \(\mathrm{false}\) (there is no following entry to carry a termination marker).

Fix a positive width \(w\). Parsing the empty aux list into triples yields the empty list of triples.

Fix a width \(w \ge 1\), and let \(ts\) be any finite list of triples \((p, d, m)\), where the position \(p\) ranges over \(\{ 0, 1, \dots , w-1\} \) and \(d, m\) are Boolean flags. Converting \(ts\) into an aux list of index–direction entries — appending a termination marker, the pair consisting of the out-of-range index \(w\) together with the flag false, after each triple whose flag \(m\) is true — and then parsing that aux list back into triples recovers exactly the original list \(ts\).

Fix a width \(w \in \mathbb {N}\), and let \(\Phi \) denote the triples-to-aux conversion, which turns a finite list of triples in \(\mathrm{Fin}(w) \times \mathrm{Bool} \times \mathrm{Bool}\) into an aux list of \((\mathbb {N}\times \mathrm{Bool})\) entries. Then \(\Phi \) carries concatenation to concatenation: for any two such lists \(T_1\) and \(T_2\),

Let \(n\) be a natural number, let \(\mathit{lits}\) be a list of literals on \(n\) variables each paired with its position index, let \(\mathit{path}\) be a list of variable–direction pairs, and let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables. Running the clause-processing procedure on \(\mathit{lits}\), \(\mathit{path}\), \(\rho _0\), and \(\sigma \) yields, among its outputs, a remaining path and a list of accumulated auxiliary pairs. The length of the auxiliary list plus the length of the remaining path is at most the length of \(\mathit{path}\).

Let \(w \in \mathbb {N}\) and let \(b\) be a nonempty list of pairs in \(\mathrm{Fin}\, w \times \mathrm{Bool}\). If one first marks the last entry of \(b\) (setting the marker flag to true on the final pair and false on all others) and then converts the resulting list of triples back into an aux list, the outcome is the list obtained from \(b\) by casting each pair \((i, d)\) to the entry \((i, d) \in \mathbb {N}\times \mathrm{Bool}\), followed by the single termination marker \((w, \mathrm{false})\).

Let \(w\) be a natural number and let \(\ell \) be a nonempty list of pairs in \(\mathrm{Fin}\, w \times \{ \mathrm{false},\mathrm{true}\} \). Then the marked list obtained from \(\ell \) by appending a boolean flag to each entry — true on the final entry and false on every other — is again nonempty.

Fix a width \(w\), and let \(B = ((i_1,b_1),\dots ,(i_k,b_k))\) be a finite list whose entries are pairs, each consisting of an index in \(\{ 0,1,\dots ,w-1\} \) together with a boolean. Form a new list of triples by appending to every entry a marker flag, set to true on the final entry of \(B\) and to false on all earlier entries. Then this list of triples has the same length as \(B\).

Let \(w\) be a natural number and let \(b\) be a list of pairs in \(\mathrm{Fin}\, w \times \{ \mathrm{true},\mathrm{false}\} \), and suppose that its marked form — the list of triples obtained by appending to each entry a marker flag that is \(\mathrm{true}\) on the final entry and \(\mathrm{false}\) on every other — is nonempty. Then the marker flag of the last triple of this marked list equals \(\mathrm{true}\).

Fix a natural number \(w\) and let \(l\) be a finite list of pairs \((i, b)\) with \(i \in \mathbb {N}\) and \(b\) a Boolean, every first coordinate of which satisfies \(i \lt w\). Recasting \(l\) into a list of pairs in \(\mathrm{Fin}\, w \times \{ \text{true}, \text{false}\} \) — by reinterpreting each index \(i\) as the element of \(\mathrm{Fin}\, w\) it names, while leaving the Booleans untouched — yields a list of the same length as \(l\).

Fix a natural number \(w\), and let \(l\) be a finite list of pairs \((i,b)\) with \(i \in \mathbb {N}\) and \(b\) a Boolean, subject to the requirement that \(i \lt w\) for every pair in \(l\). Reinterpret each such pair as \((\bar\imath , b)\), where \(\bar\imath \) is the element of \(\mathrm{Fin}\, w\) whose underlying value is \(i\), obtaining a list over \(\mathrm{Fin}\, w \times \mathrm{Bool}\). Applying the map \((j,b) \mapsto (j\text{'s underlying natural number}, b)\) to each entry of that list yields \(l\).

Fix \(w \in \mathbb {N}\), and let \(l\) be a list of pairs \((i, b) \in \mathbb {N}\times \{ \mathrm{true}, \mathrm{false}\} \) each of whose first coordinates satisfies \(i \lt w\). If \(l\) is nonempty, then its cast into a list of pairs in \(\mathrm{Fin}\, w \times \{ \mathrm{true}, \mathrm{false}\} \) is again nonempty.

Let \(t\) be a term on \(n\) variables (a list of literals), and let \(\ell \) be a list of literal–index pairs with the property that every pair in \(\ell \) occurs in the indexed enumeration of \(t\); that is, each entry of \(\ell \) is a literal of \(t\) paired with its position in \(t\). Then for any decision-tree path and any restrictions \(\rho _0,\sigma \), every pair \((i,b)\) appearing in the auxiliary output produced when \(\ell \) is processed against the path against \(t\) satisfies \(i \lt \lvert t\rvert \).

Let \(f\) be a DNF formula on \(n\) variables whose width does not exceed a positive integer \(w\), and fix a recursion-budget (fuel) parameter, a path \(P\) presented as a list of variable–direction pairs in \(\mathrm{Fin}\, n \times \mathrm{Bool}\), and two restrictions \(\rho _0\) and \(\sigma \) on the \(n\) variables. Run the Razborov encoder’s recursive worker on \(f\), \(w\), the fuel, \(P\), \(\rho _0\), and \(\sigma \) starting from an empty auxiliary accumulator, and let \(A\) be its auxiliary output, a list of pairs in \(\mathbb {N}\times \mathrm{Bool}\). Then there exists a list \(ts\) of triples in \(\mathrm{Fin}\, w \times \mathrm{Bool} \times \mathrm{Bool}\) such that \(A\) is exactly the aux list obtained from \(ts\) by the triples-to-aux conversion, the number of triples in \(ts\) is at most the length of \(P\), and, whenever \(ts\) is nonempty, the marker flag (the final Boolean component) of its last triple equals true.

Let \(f\) be a DNF formula on \(n\) variables whose width is at most \(w\), let \(w\) satisfy \(w \gt 0\), let \(d\) be a natural number, and let \(\gamma \) be a fixed restriction on the same \(n\) variables. Consider the collection of all restrictions \(\rho \) that are bad for the Boolean function computed by \(f\) at depth \(d\) — that is, the function \(x \mapsto f(\rho .\mathrm{extend}\, x)\) has decision-tree depth strictly greater than \(d\) — and whose Razborov encoding with parameters \(w,d\) has first component equal to \(\gamma \); write \(S\) for the set of auxiliary lists \(\mathrm{aux} \in (\mathbb {N}\times \mathrm{Bool})^{*}\) arising as the second component of the Razborov encoding of such a \(\rho \). Then there exists a map \(g\) from auxiliary lists to functions \(\mathrm{Fin}\, d \to \mathrm{Fin}\, w \times \mathrm{Bool} \times \mathrm{Bool}\) that is injective on \(S\).

Let \(f\) be a DNF formula on \(n\) variables whose width is at most \(w\), let \(d\) be a natural number, and let \(\gamma \) be a fixed restriction. Write the Razborov encoding of \(f\) with parameters \(w, d\) on a restriction \(\rho \) as a pair \((\gamma _\rho , \mathrm{aux}_\rho )\), where \(\gamma _\rho \) is the extended restriction and \(\mathrm{aux}_\rho \) is the auxiliary list. Consider those restrictions \(\rho \) that are bad for the Boolean function computed by \(f\) at depth \(d\) — that is, the restriction of that function by \(\rho \) has decision-tree depth strictly greater than \(d\) — and that satisfy \(\gamma _\rho = \gamma \). Then the number of distinct auxiliary lists \(\mathrm{aux}_\rho \) arising from such \(\rho \) is at most \((4w)^d\).

Let \(f\) be a DNF formula on \(n\) variables whose width is at most \(w\), and suppose no variable occurs twice within any single term of \(f\) (any two literals of a term sharing a variable are equal). Fix natural numbers \(s\) and \(d\) with \(d \le s\), and fix a target restriction \(\gamma \). Consider the restrictions \(\rho \) that are *bad* — having exactly \(s\) free variables while the Boolean function \(x \mapsto f(\rho .\mathrm{extend}\, x)\) computed by \(f\) under \(\rho \) has decision-tree depth strictly greater than \(d\) — and that the Razborov encoding sends to \(\gamma \), i.e. the first component of the encoding of \(f\) and \(\rho \) with parameters \(w, d\) equals \(\gamma \). The number of such restrictions \(\rho \) is at most \((4w)^d\).

Fix natural numbers \(n\) and \(k\). Among all restrictions on \(n\) variables — maps assigning each index \(i \in \mathrm{Fin}\, n\) either a fixed Boolean value or leaving it free — the number of those having exactly \(k\) free variables equals \(\binom {n}{k}\, 2^{\, n-k}\).

Let \(\rho \) be a restriction on \(n\) variables, let \(v\) be a variable that is free under \(\rho \), and let \(b\) be a Boolean value. Let \(\rho '\) be the restriction obtained from \(\rho \) by fixing \(v\) to the value \(b\) and leaving every other variable unchanged. Then the number of free variables of \(\rho '\) is one less than the number of free variables of \(\rho \); equivalently, if \(f(\rho )\) denotes the number of free variables of \(\rho \), then

Fix a list of literals with position indices and a decision-tree path, and let \(\rho _0\) and \(\sigma \) be two restrictions on \(n\) variables that agree on which variables are free: for every variable \(v\), \(\rho _0(v)\) is free if and only if \(\sigma (v)\) is free. Let \(\rho _0'\) and \(\sigma '\) be the updated restrictions produced by processing the clause’s literals against the path starting from \(\rho _0\) and \(\sigma \). Then \(\rho _0'\) and \(\sigma '\) again agree on their free variables: for every \(v\), \(\rho _0'(v)\) is free if and only if \(\sigma '(v)\) is free.

Fix a list of literals on \(n\) variables, each paired with its position index within its clause; a decision path presented as a list of variable–direction pairs; and two restrictions \(\rho _0, \sigma \) on \(n\) variables. For a restriction \(\rho \), write \(F(\rho )\) for the number of variables left free by \(\rho \). Suppose that \(\rho _0\) and \(\sigma \) are free at exactly the same variables (for every variable \(v\), \(\rho _0(v)\) is unset if and only if \(\sigma (v)\) is unset), that each listed literal’s variable is free in \(\rho _0\), and that the listed literals have pairwise distinct variables. Let \(\sigma '\) be the restriction returned as the \(\sigma \)-component of processing these literals against the path. Then

where \(\ell \) is the number of literals and \(m\) is the length of the path.

Let \(f\) be a DNF formula on \(n\) Boolean variables, let \(\rho \) be a restriction of those variables, and let \(d\) be a natural number. Write \(f|_\rho \) for the restricted Boolean function, which sends an assignment \(x\) to the value of \(f\) on the assignment that agrees with \(\rho \) on its fixed variables and with \(x\) on its free variables. Suppose \(\rho \) is bad for \(f\) at depth \(d\), meaning that the decision-tree depth of \(f|_\rho \) — the least depth of any decision tree computing \(f|_\rho \) — is strictly greater than \(d\). Then the deepest root-to-leaf path of the canonical decision tree of \(f\) under \(\rho \) has length strictly greater than \(d\).

Let \(f\) be a DNF formula on \(n\) variables, let \(\rho \) be a restriction of those variables, and let \(d\) be a natural number. Suppose \(\rho \) is bad for \(f\) at depth \(d\): the restriction \(x \mapsto f(\rho .\mathrm{extend}\, x)\) of the Boolean function computed by \(f\) has decision-tree depth strictly greater than \(d\). Then the deepest root-to-leaf path of the canonical decision tree of \(f\) under \(\rho \), truncated to its first \(d\) steps, is a sequence of exactly \(d\) pairs (queried variable, branch direction) — equivalently, that path has length at least \(d\).

Run the clause-processing operation on a list of literals — each tagged with its position in the clause — and a decision-tree path (a list of variable–direction pairs), starting from restrictions \(\rho _0\) and \(\sigma \). Writing \(\ell \) for the number of literals and \(m\) for the length of the path, the residual path returned by the operation has length exactly \(m - \min (\ell , m)\); equivalently, this residual length together with \(\min (\ell , m)\) sums to \(m\).

Let \(\rho \) be a restriction on \(n\) variables, let \(v\) be one of these variables, and let \(b\) be a Boolean value. Let \(\rho '\) be the restriction that fixes \(v\) to \(b\) and agrees with \(\rho \) on every other variable. Writing \(f(\sigma )\) for the number of free variables of a restriction \(\sigma \), we have \(f(\rho ') + 1 \ge f(\rho )\); that is, fixing a single variable reduces the number of free variables by at most one.

Let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables, let \(L\) be a list of literals each paired with its position index in a clause, and let \(P\) be a decision-tree path (a list of variable–direction pairs). Suppose the length of \(P\) is at most the number of free variables of \(\rho _0\). Write \((P', \rho _0', \sigma ', A)\) for the result of processing \(L\) against \(P\) starting from \(\rho _0\) and \(\sigma \), so that \(P'\) is the remaining path and \(\rho _0'\) the updated first restriction. Then the length of \(P'\) is at most the number of free variables of \(\rho _0'\).

Let \(f\) be a DNF formula on \(n\) Boolean variables and let \(\rho \) be a restriction on those variables. If every term of \(f\) is killed by \(\rho \), then the canonical decision tree for \(f|_\rho \) has depth \(0\).

Let \(f\) be a DNF formula on \(n\) Boolean variables and let \(\rho \) be a restriction on those variables. If some term of \(f\) is fixed by \(\rho \) — that is, at least one conjunction of literals in \(f\) has every literal fixed to true by \(\rho \) — then the canonical decision tree of \(f\) under \(\rho \) has depth \(0\).

Let \(t\) be a term over \(n\) variables, that is, a finite list of literals, and let \(p\) be a predicate on literals. Form from \(t\) the indexed list in which each literal is paired with its position in \(t\). Then the number of entries of this indexed list whose literal component satisfies \(p\) equals the number of literals of \(t\) that satisfy \(p\).

Let \(t = (\ell _0,\ell _1,\dots ,\ell _{m-1})\) be a term, that is a list of literals over \(\mathrm{Fin}\, n\), and let \(p\) be a Boolean predicate on literals. Annotate each literal with its position to obtain the list of pairs \((\ell _i, i)\), and retain those pairs whose literal satisfies \(p\); separately, retain the literals of \(t\) that satisfy \(p\). Then for every index \(k\) that is smaller than the length of both retained lists, the literal in the \(k\)-th retained pair equals the \(k\)-th retained literal of \(t\).

Let \(f\) be a DNF formula on \(n\) Boolean variables and \(\rho \) a restriction, and let \(t\) be the first term of \(f\), in list order, that is not killed by \(\rho \). Suppose the literals of \(t\) are pairwise distinct and no two of them share a variable, and write \(l_{i_0}, l_{i_1}, \ldots \) for the subsequence of literals of \(t\) whose variables are free under \(\rho \), taken in their order of occurrence in \(t\). Then for every index \(k\) smaller than both the number of these free literals and the length of the deepest root-to-leaf path of the canonical decision tree of \(f\) under \(\rho \), the variable queried at the \(k\)-th step of that path equals the variable of the \(k\)-th free literal \(l_{i_k}\).

Let \(\ell \) be a list of free literals of a clause, each paired with its position index, and let \(p\) be a decision-tree path, that is, a list of variable–direction pairs; let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables. Then the remaining path returned by processing \(\ell \) against \(p\) (starting from \(\rho _0\) and \(\sigma \)) is exactly the suffix of \(p\) obtained by deleting its first \(\min (|\ell |,\, |p|)\) entries.

Let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables, and write \(f(\rho )\) for the number of free variables of a restriction \(\rho \). Present a single clause as a list of \(k\) literals, each paired with its position index, and a decision-tree path as a list of \(m\) variable–direction pairs. Suppose that every literal’s variable is free in \(\rho _0\) and that the listed literals have pairwise distinct variables. Let \(\rho _0'\) be the updated restriction returned in place of \(\rho _0\) when these literals are processed against the path. Then

so processing fixes exactly \(\min (k, m)\) of the previously free variables of \(\rho _0\).

Let \(t\) be a term on \(n\) variables whose literals have pairwise distinct variables, let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables, and let \(c\) be a continuation sending each restriction to a decision tree. Let \(S\) be the sub-tree built for \(t\) under \(\rho _0\) with continuation \(c\), and let \(\pi \) denote its deepest root-to-leaf path. Write \(F\) for the sublist of \(t\) consisting of those literals whose variable is free under \(\rho _0\), and set \(m = |F|\). Suppose \(L\) is a list of \(m\) literal–index pairs whose literal components are exactly \(F\), in order, and that \(P\) is a list of variable–direction pairs coinciding with the length-\(|P|\) prefix of \(\pi \), with \(m \le |P| \le |\pi |\). Then dropping the first \(m\) entries of \(\pi \) leaves exactly the deepest path of \(c\) evaluated at the restriction obtained from \(\rho _0\) and \(\sigma \) by processing the literals \(L\) against the path \(P\) (the updated \(\rho _0\) component that this process returns).

Fix \(n\), a DNF formula \(f\) on \(n\) variables, and two restrictions \(\rho _0\) and \(\sigma \) on those variables. Suppose \(t\) is the first term of \(f\) not killed by \(\rho _0\), that \(t\) has no repeated literal, and that any two literals of \(t\) with equal variables are themselves equal. Let \(\mathrm{lits}\) be the list of literals of \(t\) whose variable is free under \(\rho _0\), each tagged with its position in \(t\), and let \(\mathrm{path}\) be a canonical path for \(f|_{\rho _0}\) — an initial segment of the deepest root-to-leaf path of the canonical decision tree of \(f|_{\rho _0}\) — of length at most the depth of the canonical decision tree of \(f|_{\rho _0}\). Assume that for every index \(k\) below the smaller of the lengths of \(\mathrm{lits}\) and \(\mathrm{path}\), the variable of the \(k\)-th literal of \(\mathrm{lits}\) equals the variable queried at the \(k\)-th step of \(\mathrm{path}\). Process \(\mathrm{lits}\) against \(\mathrm{path}\) in lockstep, one path step per literal, forming a restriction \(\rho _0'\) and a shortened path \(\mathrm{path}'\) as follows: a literal with variable \(v\) and negation flag \(b\) aligned with a path step of direction \(d\) contributes the assignment \(v \mapsto d\) to \(\rho _0'\) (and the assignment \(v \mapsto \lnot b\) to \(\sigma \)), and its path step is dropped; \(\rho _0'\) agrees with \(\rho _0\) on every other variable, and \(\mathrm{path}'\) is the unconsumed tail of \(\mathrm{path}\). Then \(\mathrm{path}'\) is a canonical path for \(f|_{\rho _0'}\), and the length of \(\mathrm{path}'\) is at most the depth of the canonical decision tree of \(f|_{\rho _0'}\).

Let \(t\) be a term on \(n\) variables (a list of literals) and let \(\rho \) be a restriction on those variables. Suppose that \(t\) contains no repeated literal, and that any two literals of \(t\) sharing the same underlying variable are in fact equal. Form the list of literals of \(t\) whose variable is free under \(\rho \), each kept together with its position in \(t\). Then this list has pairwise distinct variables: any two of its entries carry different variables.

Let \(f\) be a DNF formula on \(n\) Boolean variables in which, within each term, any two literals on the same variable are equal and no literal occurs more than once, and fix an arbitrary width \(w \in \mathbb {N}\). Let \(\rho _0\) and \(\sigma \) be restrictions on these \(n\) variables that leave exactly the same variables free (for every variable \(v\), \(\rho _0(v)\) is unset iff \(\sigma (v)\) is), and let \(\mathrm{path}\) be a prefix of the deepest root-to-leaf path of the canonical decision tree for \(f|_{\rho _0}\), of length at most the depth of that tree. If the fuel parameter strictly exceeds the length of \(\mathrm{path}\), then the restriction returned by the Razborov encoder run on \(f\) with width \(w\), this fuel, \(\mathrm{path}\), \(\rho _0\), and \(\sigma \) has exactly \(\lvert \mathrm{path}\rvert \) fewer free variables than \(\sigma \); that is, its number of free variables plus \(\lvert \mathrm{path}\rvert \) equals the number of free variables of \(\sigma \).

Let \(f\) be a DNF formula on \(n\) Boolean variables in which no term repeats a literal, and within each term any two literals on the same variable coincide (so each variable occurs at most once per term). Let \(\rho \) be a restriction with exactly \(s\) free variables, and let \(w\) and \(d\) be natural numbers with \(d \le s\). Suppose \(\rho \) is bad for \(f\) at depth \(d\), meaning the restricted Boolean function \(f|_\rho \) has decision-tree depth strictly greater than \(d\). Then the restriction forming the first component of the Razborov encoding of \(f\) and \(\rho \) with parameters \(w\) and \(d\) has exactly \(s - d\) free variables.

Let \(f\) be a DNF formula on \(n\) Boolean variables in which no two literals of the same term share a variable and no term lists the same literal twice, and suppose every term of \(f\) has at most \(w\) literals. Fix natural numbers \(d \le s\). Then the number of restrictions of the \(n\) variables that leave exactly \(s\) variables free and are bad for \(f\) at depth \(d\) — that is, for which the restricted function \(x \mapsto f(\rho .\mathrm{extend}\, x)\) has decision-tree depth strictly greater than \(d\) — is at most

Let \(f\) be a DNF formula in \(n\) variables, and let \(d\) and \(s\) be natural numbers with \(s \le d\). Then no restriction of the \(n\) variables that leaves exactly \(s\) variables free is bad for the Boolean function computed by \(f\) at depth \(d\); that is, the set of restrictions \(\rho \) that both have exactly \(s\) free variables and whose restricted function \(x \mapsto f(\rho .\mathrm{extend}\, x)\) has decision-tree depth strictly greater than \(d\) is empty.

Let \(f \colon (\mathrm{Fin}\, n \to \mathrm{Bool}) \to \mathrm{Bool}\) be a Boolean function on \(n\) variables, and let \(d\) be its decision-tree depth. Then there exists a decision tree \(T\) of depth at most \(d\) that computes \(f\), meaning \(T\) evaluated at \(x\) equals \(f(x)\) for every input \(x\).

Let \(f : (\mathrm{Fin}\, n \to \mathbb {F}_2) \to \{ 0,1\} \) be a Boolean function, and let \(d\) be a natural number such that the decision-tree depth of \(f\) is at most \(d\). Then \(f\) is computed by a DNF formula of width at most \(d\) and by a CNF formula of width at most \(d\); that is, there exist a disjunction of terms and a conjunction of clauses, each term or clause containing at most \(d\) literals, that both agree with \(f\) on every input.

Let \(l\) be a literal over \(n\) Boolean variables, given by a variable index and a polarity that marks it as positive or negated, and let \(x \in \{ \text{true},\text{false}\} ^n\) be an assignment. Writing \(\bar{l}\) for the literal obtained from \(l\) by flipping its polarity while keeping the same variable, the value of \(\bar{l}\) under \(x\) is the negation of the value of \(l\) under \(x\); that is, \(\bar{l}(x) = \lnot \, l(x)\).

Let \(l\) be a literal on \(n\) variables, that is, a variable \(v \in \{ 0,1,\dots ,n-1\} \) together with a polarity bit. The literal obtained from \(l\) by flipping its polarity has the same underlying variable \(v\) as \(l\).

Fix \(n \in \mathbb {N}\), and recall that a literal is a pair consisting of a variable in \(\{ 0, 1, \dots , n-1\} \) together with a polarity bit, and that flipping a literal’s polarity toggles this bit while leaving the variable unchanged. Then the polarity-flipping operation is injective: if two literals have the same polarity flip, they are equal.

Let \(\psi \) be a CNF formula over \(n\) variables, and let \(\psi ^{*}\) be its De Morgan dual DNF, obtained by negating every literal so that each clause becomes a term. Then \(\psi ^{*}\) and \(\psi \) have the same width; that is, the maximum term-length of \(\psi ^{*}\) equals the maximum clause-width of \(\psi \).

Let \(\psi \) be a formula in conjunctive normal form over \(n\) Boolean variables — a conjunction of clauses, each clause a disjunction of literals — and let its De Morgan dual DNF be obtained by negating every literal of \(\psi \), so that each clause \(\bigvee _j l_{ij}\) becomes the term \(\bigwedge _j \lnot l_{ij}\). Then for every assignment \(x \colon \{ 0,\dots ,n-1\} \to \{ \mathrm{true},\mathrm{false}\} \), evaluating this dual DNF at \(x\) yields exactly the negation of the value of \(\psi \) at \(x\).

Let \(T\) be a decision tree on \(n\) Boolean variables, and let \(x \colon \{ 0,\dots ,n-1\} \to \{ \mathtt{false},\mathtt{true}\} \) be an assignment of the variables. Then the tree obtained from \(T\) by negating every leaf value evaluates on \(x\) to the negation of the value of \(T\) on \(x\); that is, its output equals \(\lnot \, (T(x))\).

Let \(T\) be a decision tree on \(n\) Boolean variables, and let \(T'\) be the tree obtained from \(T\) by negating the Boolean value at every leaf while leaving its branching structure unchanged. Then \(T'\) has the same depth as \(T\).

Let \(f\) be a Boolean function on \(n\) variables, and let \(\bar f\) denote its pointwise negation, so that \(\bar f(x) = 1 - f(x)\) for every input \(x\). Then \(f\) and \(\bar f\) have the same decision-tree depth: \(\operatorname {depth}_{\mathrm{DT}}(\bar f) = \operatorname {depth}_{\mathrm{DT}}(f)\).

Let \(f : (\mathrm{Fin}\, n \to \mathbb {F}_2) \to \mathbb {F}_2\) be a Boolean function and \(\rho \) a restriction on \(n\) variables. Then restricting the negation of \(f\) agrees, at every point \(x\), with the negation of the restriction of \(f\); that is, \((\lnot f)\) restricted by \(\rho \) equals the pointwise negation of \(f\) restricted by \(\rho \).

Let \(f : (\mathrm{Fin}\, n \to \mathrm{Bool}) \to \mathrm{Bool}\) be a Boolean function, \(d\) a natural number, and \(\rho \) a restriction on the \(n\) variables. Then \(\rho \) is bad for the negation \(\lnot f\) at depth \(d\) if and only if \(\rho \) is bad for \(f\) at depth \(d\); that is, the restricted function of \(\lnot f\) under \(\rho \) has decision-tree depth greater than \(d\) exactly when the restricted function of \(f\) under \(\rho \) does.

Let \(\psi \) be a CNF formula whose clauses are lists of literals, and suppose that every clause of \(\psi \) contains no repeated literal. Then every term of the De Morgan dual DNF obtained from \(\psi \) — the DNF formed by negating each literal of each clause — likewise contains no repeated literal.

Let \(\psi \) be a CNF formula on \(n\) variables with the property that, within each of its clauses, any two literals having the same variable are in fact the same literal (so no variable occurs in a clause with both polarities, nor is any literal repeated). Then the De Morgan dual DNF obtained from \(\psi \) by negating every literal has the same property term by term: within each of its terms, any two literals sharing a variable are equal.

Let \(n\), \(s\), and \(d\) be natural numbers satisfying \(5s \le n\) and \(d \le s\). Then