Let \(\rho \) be a restriction on \(n\) variables, and let \(v\) be a free variable of \(\rho \). For any Boolean value \(b\), let \(\rho '\) be the restriction that agrees with \(\rho \) everywhere except at \(v\), where it assigns the fixed value \(b\). Then the number of free variables of \(\rho '\) is strictly less than the number of free variables of \(\rho \).

Let \(f\) be a DNF formula on \(n\) variables and let \(\rho \) be a restriction on those variables. Suppose that not every term of \(f\) is killed by \(\rho \), and that no term of \(f\) is fixed by \(\rho \). Then \(\rho \) leaves at least one variable free; that is, there exists an index \(v \in \mathrm{Fin}\, n\) with \(\rho (v)\) unset.

Let \(f\) be a DNF formula on \(n\) variables and \(\rho \) a restriction. Suppose that at least one term of \(f\) is not killed by \(\rho \), and that no term of \(f\) is fixed by \(\rho \). Then the branch-variable selection procedure applied to \(f\) and \(\rho \) succeeds, returning a variable \(v\) that is free in \(\rho \).

Let \(\rho \) be a restriction on \(n\) variables, let \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\) be a point, and let \(v \in \mathrm{Fin}\, n\) be a free variable of \(\rho \) with \(x(v) = b\). Let \(\rho [v \mapsto b]\) be the restriction obtained from \(\rho \) by fixing the value of variable \(v\) to \(b\) (and leaving every other variable as in \(\rho \)). Then \(\rho [v \mapsto b]\) and \(\rho \) have the same extension along \(x\); that is, \((\rho [v \mapsto b]).\mathrm{extend}\, x\) and \(\rho .\mathrm{extend}\, x\) agree as Boolean assignments.

Fix \(n\), and let \(\ell _1,\dots ,\ell _m\) be a list of literals over \(n\) variables, \(\rho \) a restriction on those variables, \(\mathrm{cont}\) a map sending each restriction to a decision tree, and \(x \in \{ \mathrm{true},\mathrm{false}\} ^n\) an assignment. Then evaluating the term sub-tree built from \(\ell _1,\dots ,\ell _m\), \(\rho \), and \(\mathrm{cont}\) at \(x\) gives the same Boolean value as evaluating \(\mathrm{cont}(\rho ^\ast )\) at \(x\), where \(\rho ^\ast \) is obtained from \(\rho \) by processing the literals in order: for each \(\ell _i\), if its variable is free in the current restriction, that variable is fixed to \(x\)’s value there, and otherwise the restriction is left unchanged.

Let \(\rho \) be a restriction on \(n\) variables, let \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\) be a point, and let \(\ell _1, \dots , \ell _m\) be a list of literals over these variables. Form a sequence of restrictions \(\rho _0 = \rho , \rho _1, \dots , \rho _m\) by processing the literals in order: for each \(k\), writing \(v_k\) for the variable of \(\ell _k\), if \(v_k\) is free in \(\rho _{k-1}\) then let \(\rho _k\) agree with \(\rho _{k-1}\) except that \(v_k\) is fixed to the value \(x(v_k)\), and otherwise let \(\rho _k = \rho _{k-1}\). Then the extension of \(\rho _m\) along \(x\) equals the extension of \(\rho \) along \(x\).

Let \(\rho : \mathrm{Fin}\, n \to \mathrm{Option}\, \mathrm{Bool}\) be a restriction on \(n\) variables, let \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\) be a Boolean assignment, and let \(\ell _1, \dots , \ell _m\) be literals on these variables. Process the literals from left to right, starting from \(\rho \): at each literal, if its variable is still free in the restriction accumulated so far, fix that variable to the value \(x\) assigns it, and otherwise change nothing. Then any variable \(v\) that already carries a fixed value under \(\rho \) (that is, \(\rho (v)\) leaves \(v\) set rather than free) still carries a fixed value in the final restriction; the fold never frees an already-fixed variable.

Fix \(n\) variables, let \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\) be a Boolean assignment, let \(\rho \) be a restriction on these variables, and let \(\ell _1, \dots , \ell _m\) be a list of literals. Process the literals from left to right, maintaining a current restriction that begins as \(\rho \): at each literal \(\ell \), if its underlying variable \(\ell .\mathrm{var}\) is free in the current restriction, update that restriction by fixing \(\ell .\mathrm{var}\) to the value \(x(\ell .\mathrm{var})\), and otherwise leave the restriction unchanged; write \(\rho ^*\) for the restriction obtained after the whole list has been processed. Then for every literal \(\ell \) in the list whose variable is free in the original restriction \(\rho \), the value \(\rho ^*(\ell .\mathrm{var})\) is set, i.e. \(\ell .\mathrm{var}\) is not free in \(\rho ^*\).

Let \(\rho \) be a restriction on \(n\) variables, let \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\) be a Boolean assignment, and let \(\ell _1, \dots , \ell _k\) be a list of literals on \(n\) variables. Process the literals from left to right, starting from \(\rho \): at each step, if the current literal’s variable is still free in the restriction obtained so far, fix that variable to the value \(x\) assigns it, and otherwise leave the restriction unchanged; write \(\rho '\) for the restriction produced after all \(k\) steps. If at least one literal in the list has its variable free in the original restriction \(\rho \), then \(\rho '\) has strictly fewer free variables than \(\rho \).

Let \(f\) be a DNF formula on \(n\) Boolean variables, let \(\rho \) be a restriction of those variables, and let \(m\) be a natural number strictly greater than the number of free variables of \(\rho \). Denote by \(T\) the decision tree obtained from \(f\) and \(\rho \) by the canonical fuel-bounded recursion run with fuel budget \(m\). Then \(T\) computes the restriction of \(f\) by \(\rho \): for every assignment \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\), evaluating \(T\) at \(x\) returns \(f\) applied to the extension of \(x\) along \(\rho \) — the assignment that uses \(\rho \)’s fixed value on each constrained coordinate and \(x\)’s value on each free coordinate.

Let \(f\) be a DNF formula on \(n\) Boolean variables and let \(\rho \) be a restriction of those variables. Then the canonical decision tree of \(f\) under \(\rho \) computes exactly the restriction of \(f\) by \(\rho \): for every Boolean assignment \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\), evaluating the tree at \(x\) yields the value of \(f\) on the assignment that takes \(\rho (i)\) wherever \(\rho \) fixes coordinate \(i\) and \(x_i\) on the free coordinates.

Let \(\rho \) be a restriction on \(n\) variables, let \(v \in \mathrm{Fin}\, n\), and let \(b\) be a Boolean value. Write \(\rho [v \mapsto b]\) for the restriction that agrees with \(\rho \) everywhere except at \(v\), where it takes the fixed value \(b\). Then the number of free variables of \(\rho [v \mapsto b]\) is at most the number of free variables of \(\rho \).

Let \(\ell \) be a list of literals on \(n\) variables and let \(\rho \) be a restriction. For a continuation \(c : \mathrm{Restriction}\, n \to \mathrm{DecisionTree}\, n\), write \(T(\ell , \rho , c)\) for the term sub-tree built from \(\ell \) starting at \(\rho \) with continuation \(c\). If two continuations \(c_1\) and \(c_2\) agree on every restriction \(\rho '\) whose number of free variables is at most the number of free variables of \(\rho \) — that is, \(c_1(\rho ') = c_2(\rho ')\) whenever \(\rho '\) has no more free variables than \(\rho \) — then \(T(\ell , \rho , c_1) = T(\ell , \rho , c_2)\).

Let \(L\) be a list of literals on \(n\) variables and \(\rho \) a restriction on those variables, and suppose at least one literal in \(L\) has its variable free under \(\rho \). Let \(c_1\) and \(c_2\) be two continuations — maps sending each restriction to a decision tree — that agree on every restriction having strictly fewer free variables than \(\rho \). Then the two term sub-trees built from \(L\) and \(\rho \), one using the continuation \(c_1\) and the other using \(c_2\), are identical.

Let \(f\) be a DNF formula on \(n\) variables, and let \(\rho \) be a restriction on those variables having \(k\) free variables. Write \(G(f, m, \rho )\) for the fuel-bounded recursion that builds a decision tree from the DNF \(f\) and the restriction \(\rho \), in which the natural-number fuel budget \(m\) serves as an upper bound on the recursion depth. Then for any two fuel budgets \(m_1\) and \(m_2\) that both strictly exceed \(k\), the two trees coincide: \(G(f, m_1, \rho ) = G(f, m_2, \rho )\).

The canonical decision tree of a DNF formula \(f\) under a restriction \(\rho \) is built by a fuel-limited recursion; write \(G_k(f,\rho )\) for the decision tree it returns when run with fuel budget \(k \in \mathbb {N}\) starting from \(\rho \), so that the canonical decision tree of \(f\) under \(\rho \) is \(G_{m(\rho )+1}(f,\rho )\), where \(m(\rho )\) denotes the number of free variables of \(\rho \). Let \(f\) be a DNF formula on \(n\) variables, let \(t\) be a term with \(t \in f\), and let \(\rho _{\mathrm{orig}}\) and \(\rho '\) be restrictions with \(m(\rho _{\mathrm{orig}}) \ge m(\rho ') + 1\). Then the tree that returns the constant-true leaf if \(t\) is fixed by \(\rho '\) and returns \(G_{m(\rho _{\mathrm{orig}})}(f,\rho ')\) otherwise is equal to the canonical decision tree of \(f\) under \(\rho '\).

Let \(l\) be a literal on \(n\) Boolean variables, write \(i\) for its underlying variable, let \(\mathit{rest}\) be a further list of literals, let \(\rho \) be a restriction on these \(n\) variables, and let the continuation assign a decision tree to each restriction. If \(i\) is free under \(\rho \), then the sub-tree built for the list \(l :: \mathit{rest}\) under \(\rho \) (with this continuation) is the branch that queries \(i\), whose false-child is the sub-tree built for \(\mathit{rest}\) under the restriction obtained from \(\rho \) by fixing \(i\) to false, and whose true-child is the sub-tree built for \(\mathit{rest}\) under the restriction obtained from \(\rho \) by fixing \(i\) to true, both with the same continuation.

Let \(\rho \) be a restriction on \(n\) variables, let \(l\) be a literal whose underlying variable \(v\) is not free under \(\rho \) (that is, \(\rho \) already assigns \(v\) a fixed Boolean value), let \(\mathit{rest}\) be a list of literals, and let \(\mathrm{cont} : \mathrm{Restriction}\, n \to \mathrm{DecisionTree}\, n\) be a continuation. Then the sub-tree built for the term \(l :: \mathit{rest}\) under \(\rho \) with continuation \(\mathrm{cont}\) coincides with the one built for \(\mathit{rest}\) under \(\rho \) with the same continuation; the fixed head literal \(l\) contributes no branch.

Fix a restriction \(\rho \) on \(n\) variables and a continuation \(c\) that assigns a decision tree to each restriction. Let \(l\) be a literal whose variable \(v\) is free in \(\rho \), and let \(\mathit{rest}\) be a further list of literals. Then there is a Boolean value \(b\) such that the deepest root-to-leaf path of the term sub-tree built from the literal list \(l :: \mathit{rest}\), the restriction \(\rho \), and the continuation \(c\) begins with the pair \((v, b)\) and continues with the deepest root-to-leaf path of the term sub-tree built from \(\mathit{rest}\), the restriction \(\rho \) with \(v\) now fixed to the value \(b\), and the same continuation \(c\).

Let \(\rho : \mathrm{Fin}\, n \to \mathrm{Option}\, \mathrm{Bool}\) be a restriction, let \(R\) be a list of literals on the variables \(\mathrm{Fin}\, n\), and let \(v \in \mathrm{Fin}\, n\) and \(b \in \mathrm{Bool}\). Write \(\rho [v \mapsto b]\) for the restriction that agrees with \(\rho \) everywhere except at \(v\), where it takes the fixed value \(b\). If the variable of every literal in \(R\) is distinct from \(v\), then selecting from \(R\) those literals whose variable is free under \(\rho [v \mapsto b]\) yields the same list as selecting those whose variable is free under \(\rho \).

Let \(\mathit{lits}\) be a list of literals on \(n\) Boolean variables whose variables are pairwise distinct, let \(\rho \) be a restriction, and let \(g\) be a map sending each restriction to a decision tree. Let \(T\) be the sub-tree built for the term \(\mathit{lits}\) under \(\rho \) with continuation \(g\): reading the literals of \(\mathit{lits}\) in order, it branches on each literal whose variable is free under \(\rho \), skips the others, and evaluates \(g\) at each leaf. Write \(\mathit{lits}_\rho \) for the sublist of \(\mathit{lits}\), in order, consisting of exactly those literals whose variable is free under \(\rho \). Then for every index \(k\) smaller than both the length of \(\mathit{lits}_\rho \) and the length of the deepest root-to-leaf path of \(T\), the variable queried at position \(k\) of that deepest path equals the variable of the \(k\)-th literal of \(\mathit{lits}_\rho \).

Let \(\rho \) be a restriction on \(n\) variables, let \(\mathit{lits}\) be a list of literals whose underlying variables are pairwise distinct, and let \(\mathrm{cont}\) be a continuation assigning a decision tree to every restriction. Then there is a restriction \(\rho '\) that agrees with \(\rho \) at every variable not occurring among the literals of \(\mathit{lits}\), and such that the deepest root-to-leaf path of the term sub-tree built from \(\mathit{lits}\), \(\rho \), and \(\mathrm{cont}\) has length equal to the number of literals in \(\mathit{lits}\) whose variable is free under \(\rho \), plus the length of the deepest root-to-leaf path of \(\mathrm{cont}(\rho ')\).

Let \(\mathit{lits}\) be a list of literals on \(n\) variables in which no two literals share the same variable, let \(\rho \) be a restriction on \(n\) variables, and let \(c\) be a continuation, that is, a map sending each restriction to a decision tree. Then there exist a list \(P\) of (variable, branch-direction) pairs and a restriction \(\rho '\) such that the deepest path of the sub-tree for the term \(\mathit{lits}\) built from \(\rho \) and \(c\) equals \(P\) followed by the deepest path of \(c(\rho ')\); the length of \(P\) equals the number of literals of \(\mathit{lits}\) whose variable is free under \(\rho \); and \(\rho '\) agrees with \(\rho \) on every variable that does not occur among the variables of \(\mathit{lits}\).

Fix \(n\) Boolean variables, and let \(f\) be a DNF formula (a list of terms) and \(\rho \) a restriction. Write \(T(f, k, \rho )\) for the fuel-bounded canonical decision tree of \(f\) under \(\rho \) built with fuel budget \(k\), and for a term \(s\), a restriction \(\sigma \), and a continuation \(c\) mapping restrictions to decision trees, write \(S(s, \sigma , c)\) for the term sub-tree of \(s\) under \(\sigma \) with continuation \(c\). Suppose that, under \(\rho \), not every term of \(f\) is killed and no term of \(f\) is fixed, and let \(t\) be the first term of \(f\), in list order, that is not killed by \(\rho \). Then

where the continuation \(c\) sends a restriction \(\rho '\) to the leaf that outputs true when \(t\) is fixed by \(\rho '\), and to \(T(f,\ \mathit{fuel},\ \rho ')\) otherwise.

Let \(f\) be a DNF formula and \(\rho \) a restriction on \(n\) variables such that \(\rho \) does not kill every term of \(f\) and fixes no term of \(f\), and let \(t\) be the first term of \(f\), in list order, that \(\rho \) does not kill. Then the canonical decision tree of \(f\) under \(\rho \) equals the term sub-tree built for \(t\) over \(\rho \) whose continuation, evaluated at each leaf restriction \(\rho '\) reached along a root-to-leaf path, returns the constant-true leaf when \(\rho '\) fixes \(t\) and otherwise returns the fuel-bounded canonical construction for \(f\) under \(\rho '\) run with fuel budget equal to the number of free variables of \(\rho \).

Fix a restriction \(\rho \) on \(n\) variables and a continuation \(c\) assigning a decision tree to each restriction. For a list of literals \(L\), write \(T(L)\) for the term sub-tree built from \(L\) under \(\rho \) with continuation \(c\): it branches, in order, on each literal of \(L\) whose variable is free in \(\rho \), skipping the rest, and at every leaf invokes \(c\) on the restriction updated along that path. Let \(P\) and \(R\) be lists of literals, and suppose every literal in \(P\) has its variable already fixed by \(\rho \), that is, not among the free variables of \(\rho \). Then prepending \(P\) to \(R\) leaves the resulting tree unchanged:

where \(P \frown R\) denotes the concatenation of \(P\) followed by \(R\).

Let \(\rho \) be a restriction on \(n\) variables and \(g\) a continuation assigning a decision tree to each restriction on \(n\) variables. Fix a variable \(v\), a Boolean value \(b\), and a literal \(\ell \) whose variable is \(v\), and let \(\mathit{rest}\) be a further list of literals. Write \(\rho [v \mapsto b]\) for the restriction that agrees with \(\rho \) everywhere except at \(v\), where it is fixed to the value \(b\). Then the term sub-tree built from the list obtained by prepending \(\ell \) to \(\mathit{rest}\), under \(\rho [v \mapsto b]\) with continuation \(g\), coincides with the term sub-tree built from \(\mathit{rest}\) alone under the same restriction and the same continuation.

Let \(f : (\mathrm{Fin}\, n \to \mathrm{Bool}) \to \mathrm{Bool}\) be a Boolean function, and let \(T\) be a decision tree on \(n\) Boolean variables that computes \(f\), in the sense that \(T\) evaluates to \(f(x)\) on every input \(x\). Then the depth of \(T\) is at least the decision-tree depth of \(f\); that is, \(\mathrm{depth}(T)\) is no smaller than the least depth of any decision tree computing \(f\).

Let \(f\) be a DNF formula on \(n\) Boolean variables and let \(\rho \) be a restriction on those variables, and write \(f|_\rho \) for the restricted Boolean function \(x \mapsto f\big(\rho .\mathrm{extend}\, x\big)\), which evaluates \(f\) on the assignment that takes the fixed value of \(\rho \) where one is set and reads the remaining coordinates from \(x\). Then the depth of the canonical decision tree for \(f\) under \(\rho \) is at least the decision-tree depth of \(f|_\rho \); that is, the least depth of any decision tree computing \(f|_\rho \) does not exceed the depth of the canonical tree.

Let \(f : (\mathrm{Fin}\, n \to \mathrm{Bool}) \to \mathrm{Bool}\) be a Boolean function and let \(\rho \) be a restriction on \(n\) variables, fixing some coordinates to Boolean values and leaving the rest free. Then the decision-tree depth of the restricted function \(f\! \restriction _\rho \), which sends \(x\) to \(f\) evaluated with the free coordinates taken from \(x\) and the remaining coordinates set by \(\rho \), is at most the number of free variables of \(\rho \).