Fix \(n\) and let \(l\) be a literal on \(n\) variables, with underlying variable \(v \in \mathrm{Fin}\, n\) and polarity flag \(b \in \{ \text{false}, \text{true}\} \) (with \(b = \text{true}\) marking a negated literal). Let \(\rho \) be a restriction on \(n\) variables that kills \(l\), meaning \(\rho \) fixes \(v\) to the value \(b\). Then for every assignment \(x : \mathrm{Fin}\, n \to \{ \text{false}, \text{true}\} \), the literal \(l\) evaluates to false at the extension of \(x\) along \(\rho \).

Let \(l\) be a literal on \(n\) variables and let \(\rho \) be a restriction on those same variables that fixes \(l\), meaning \(\rho \) assigns \(l\)’s variable the Boolean value that makes \(l\) true. Then for every assignment \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\), the literal \(l\) evaluates to true on the extension of \(x\) along \(\rho \) (the assignment using \(\rho \)’s fixed value on each set variable and \(x\) on the free ones).

Let \(f : (\mathrm{Fin}\, n \to \mathrm{Bool}) \to \mathrm{Bool}\) be a Boolean function, and let \(T\) be a decision tree on \(n\) variables of depth at most \(d\) that computes \(f\), meaning \(T\) evaluates to \(f(x)\) on every input \(x\). Then the decision-tree depth of \(f\) is at most \(d\).

Let \(l\) be a finite list of elements of a type \(\alpha \), and let \(p \colon \alpha \to \{ \mathrm{true}, \mathrm{false}\} \) be a Boolean predicate. If \(p(x) = \mathrm{false}\) for every entry \(x\) of \(l\), then the Boolean existential \(\bigvee _{x \in l} p(x)\) — the value \(\mathrm{true}\) exactly when some entry of \(l\) satisfies \(p\) — is \(\mathrm{false}\).

Let \(l\) be a list of elements of a type \(\alpha \) and let \(p \colon \alpha \to \{ \mathrm{true}, \mathrm{false}\} \) be a Boolean predicate. If some element \(a\) of \(l\) satisfies \(p(a) = \mathrm{false}\), then the test whether every entry of \(l\) satisfies \(p\) evaluates to \(\mathrm{false}\).

Let \(f\) be a DNF formula on \(n\) Boolean variables and let \(\rho \) be a restriction of those variables. If at least one term of \(f\) is fixed by \(\rho \), then the restricted Boolean function \(x \mapsto f(\rho \text{-extension of }x)\) has decision-tree depth \(0\).

Let \(f\) be a DNF formula on \(n\) Boolean variables and let \(\rho \) be a restriction on these variables. If every term of \(f\) is killed by \(\rho \) — that is, each term contains a literal whose variable \(\rho \) fixes to the value making that literal false — then the restricted function \(x \mapsto f\bigl(\rho .\mathrm{extend}\, x\bigr)\) has decision-tree depth \(0\).

Let \(t\) be a term on \(n\) variables and let \(\rho , \sigma : \mathrm{Fin}\, n \to \mathrm{Option}\, \mathrm{Bool}\) be two restrictions such that \(\sigma (v) = \rho (v)\) for every variable \(v\) that \(\rho \) fixes (that is, whenever \(\rho (v) \neq \mathrm{none}\)). If \(t\) is killed by \(\rho \), then \(t\) is also killed by \(\sigma \).

Let \(f\) be a DNF formula on \(n\) variables — a list of terms, each a conjunction of literals — and let \(\rho \) and \(\sigma \) be restrictions of these \(n\) variables. Suppose \(\sigma \) agrees with \(\rho \) on every variable that \(\rho \) fixes, that is, \(\sigma (v) = \rho (v)\) for every variable \(v\) on which \(\rho \) takes a Boolean value rather than leaving it free. Let \(t\) be the first term of \(f\) (in list order) that is not killed by \(\rho \), and suppose in addition that \(t\) is not killed by \(\sigma \). Then \(t\) is also the first term of \(f\) that is not killed by \(\sigma \).

Let \(f\) be a DNF formula in \(n\) variables, that is, a disjunction \(t_1 \vee \cdots \vee t_m\) of terms, where each term is a conjunction of literals, and let its width be the largest number of literals occurring in any of its terms (and \(0\) if \(f\) has no terms). Then for every term \(t\) appearing in \(f\), the number of literals in \(t\) is at most the width of \(f\).

Let \(l\) be a list over a type \(\alpha \), let \(p\colon \alpha \to \{ \text{true},\text{false}\} \) be a predicate, and fix a starting index \(s\). Form the indexed list obtained by pairing each entry of \(l\) with its position, numbered consecutively from \(s\). If the first pair in this indexed list whose first component satisfies \(p\) is the pair \((x,\mathrm{idx})\), then \(x\) is the first entry of \(l\) satisfying \(p\).

Let \(t\) be a list over a type \(\alpha \), and tag each entry of \(t\) with its zero-based position, forming the list of pairs \((t_i, i)\). If a pair \((l, i)\) occurs among these tagged entries — equivalently, the entry of \(t\) at position \(i\) is \(l\) — then deleting the first \(i\) entries of \(t\) leaves a nonempty list whose first element is \(l\); that is, there is a list \(\mathit{rest}\) with \(t\) from position \(i\) onward equal to \(l\) prepended to \(\mathit{rest}\).

Let \(t\) be a finite list of elements of a type \(\alpha \), and tag each entry of \(t\) with its position to form the list of pairs \((t_i, i)\), whose second coordinates run through \(0, 1, \dots , |t| - 1\). Let \(p\) be any Boolean predicate on such pairs, and let \(w\) be a natural number with \(|t| \le w\). If a pair \((l, \mathit{idx})\) occurs in the sublist obtained by keeping exactly those tagged pairs on which \(p\) is true, then \(\mathit{idx} \lt w\).