If \(v\) is a free variable of a restriction \(\rho \), then fixing \(v\) to a value \(b\) strictly decreases the number of free variables: \(\mathrm{numFree}(\rho [v \mapsto b]) \lt \mathrm{numFree}(\rho )\).

For a DNF \(f\) and restriction \(\rho \), if not every term is killed by \(\rho \) and no term is fixed by \(\rho \), then \(\rho \) has at least one free variable \(v \in \rho .\mathrm{freeVars}\).

When not every term of \(f\) is killed by \(\rho \) and no term is fixed by \(\rho \), the function \(\mathrm{selectBranchVar}\, f\, \rho \) returns some variable \(v\), and that \(v\) is free in \(\rho \).

If \(v\) is free in \(\rho \) and the input \(x\) satisfies \(x(v) = b\), then extending the updated restriction \(\rho [v \mapsto b]\) by \(x\) yields the same total assignment as extending \(\rho \) by \(x\).

Evaluating \(\mathrm{termSubTree}\, \mathit{lits}\, \rho \, \mathrm{cont}\) at \(x\) equals evaluating the continuation at \(x\), applied to the restriction obtained by folding \(x\)’s values into \(\rho \) along the free literals of \(\mathit{lits}\).

After \(\mathrm{termSubTree}\) assigns all free variables of \(\mathit{lits}\) from \(x\), the resulting restriction extends by \(x\) to the same total assignment as \(\rho \) does: \((\mathrm{fold}\, \mathit{lits}\, \rho ).\mathrm{extend}\, x = \rho .\mathrm{extend}\, x\).

If \(\rho (v) \neq \mathrm{none}\), then after the \(\mathrm{termSubTree}\) fold over \(\mathit{lits}\) the entry at \(v\) remains non-none; that is, the fold never unsets an already-fixed variable.

If a literal \(l \in \mathit{lits}\) has variable free in \(\rho \), then after the \(\mathrm{termSubTree}\) fold the entry at \(l.\mathrm{var}\) is no longer none (it has been set to some value).

When at least one literal of \(\mathit{lits}\) has a variable free in \(\rho \), the \(\mathrm{termSubTree}\) fold strictly decreases \(\mathrm{numFree}\).

Provided the fuel exceeds \(\rho .\mathrm{numFree}\), the tree \(\mathrm{canonicalDTree.go}\, f\, \mathit{fuel}\, \rho \) computes the restricted function: for all \(x\), its evaluation equals \(\mathrm{restrictFn}\, (f.\mathrm{eval})\, \rho \, x\).

For every \(x\), the canonical decision tree evaluates correctly: \((\mathrm{canonicalDTree}\, f\, \rho ).\mathrm{eval}\, x = \mathrm{restrictFn}\, (f.\mathrm{eval})\, \rho \, x\).

Fixing a variable \(v\) to a value \(b\) never increases the number of free variables: \(\mathrm{numFree}(\rho [v \mapsto b]) \le \mathrm{numFree}(\rho )\).

If two continuations \(\mathrm{cont}_1, \mathrm{cont}_2\) agree on all restrictions \(\rho '\) with \(\rho '.\mathrm{numFree} \le \rho .\mathrm{numFree}\), then \(\mathrm{termSubTree}\, \mathit{lits}\, \rho \, \mathrm{cont}_1 = \mathrm{termSubTree}\, \mathit{lits}\, \rho \, \mathrm{cont}_2\).

If \(\mathit{lits}\) contains at least one literal free in \(\rho \), then the two continuations need only agree on restrictions \(\rho '\) with \(\rho '.\mathrm{numFree} \lt \rho .\mathrm{numFree}\) for the two \(\mathrm{termSubTree}\) trees to be equal.

Once the fuel exceeds \(\rho .\mathrm{numFree}\), the resulting tree does not depend on the exact fuel: for any \(\mathit{fuel}_1, \mathit{fuel}_2 \gt \rho .\mathrm{numFree}\), \(\mathrm{canonicalDTree.go}\, f\, \mathit{fuel}_1\, \rho = \mathrm{canonicalDTree.go}\, f\, \mathit{fuel}_2\, \rho \).

For \(t \in f\) and a restriction \(\rho '\) with \(\rho _{\mathrm{orig}}.\mathrm{numFree} \ge \rho '.\mathrm{numFree} + 1\), the standard continuation \(\bigl(\text{if } t \text{ fixed by } \rho ' \text{ then } \mathrm{leaf}\ \mathrm{true}\ \text{else}\ \mathrm{canonicalDTree.go}\, f\, \rho _{\mathrm{orig}}.\mathrm{numFree}\, \rho '\bigr)\) equals \(\mathrm{canonicalDTree}\, f\, \rho '\).

When the head literal \(l\) is free in \(\rho \), \(\mathrm{termSubTree}\, (l :: \mathit{rest})\, \rho \, \mathrm{cont}\) is a branch on \(l.\mathrm{var}\) whose two children are the recursive \(\mathrm{termSubTree}\) calls on \(\mathit{rest}\) with \(\rho \) updated to \(\mathrm{some}\ \mathrm{false}\) and \(\mathrm{some}\ \mathrm{true}\).

When the head literal \(l\) is not free in \(\rho \), it is skipped: \(\mathrm{termSubTree}\, (l :: \mathit{rest})\, \rho \, \mathrm{cont} = \mathrm{termSubTree}\, \mathit{rest}\, \rho \, \mathrm{cont}\).

When the head literal \(l\) is free in \(\rho \), the deepest root-to-leaf path of \(\mathrm{termSubTree}\, (l :: \mathit{rest})\, \rho \, \mathrm{cont}\) begins with \((l.\mathrm{var}, b)\) for some \(b\) (the direction of the deeper child), followed by the deep path of the recursive call on \(\rho [l.\mathrm{var} \mapsto b]\).

If every literal of \(\mathit{rest}\) has variable distinct from \(v\), then filtering \(\mathit{rest}\) by freeness under \(\rho [v \mapsto b]\) gives the same list as filtering by freeness under \(\rho \).

For \(\mathit{lits}\) with pairwise distinct variables, the \(k\)-th variable of the deep path of \(\mathrm{termSubTree}\, \mathit{lits}\, \rho \, \mathrm{cont}\) equals the variable of the \(k\)-th literal in the free-filtered list of \(\mathit{lits}\).

For \(\mathit{lits}\) with pairwise distinct variables there is a restriction \(\rho '\), agreeing with \(\rho \) off the variables of \(\mathit{lits}\), such that the deep-path length of \(\mathrm{termSubTree}\, \mathit{lits}\, \rho \, \mathrm{cont}\) equals the number of free literals of \(\mathit{lits}\) plus the deep-path length of \(\mathrm{cont}\, \rho '\).

For \(\mathit{lits}\) with pairwise distinct variables, the deep path of \(\mathrm{termSubTree}\, \mathit{lits}\, \rho \, \mathrm{cont}\) splits as a prefix (one entry per free literal of \(\mathit{lits}\)) appended with the deep path of \(\mathrm{cont}\, \rho '\), where \(\rho '\) agrees with \(\rho \) off the variables of \(\mathit{lits}\).

When not all terms are killed and none is fixed, and \(t\) is the first non-killed clause, \(\mathrm{canonicalDTree.go}\, f\, (\mathit{fuel}+1)\, \rho \) unfolds to \(\mathrm{termSubTree}\, t\, \rho \, \mathrm{cont}\), where \(\mathrm{cont}\, \rho '\) is \(\mathrm{leaf}\ \mathrm{true}\) if \(t\) is fixed by \(\rho '\) and otherwise \(\mathrm{canonicalDTree.go}\, f\, \mathit{fuel}\, \rho '\).

The top-level analogue of the previous lemma for \(\mathrm{canonicalDTree}\) itself: under the alive-branch hypotheses with first non-killed clause \(t\), \(\mathrm{canonicalDTree}\, f\, \rho \) equals \(\mathrm{termSubTree}\, t\, \rho \, \mathrm{cont}\) with the same fixed-or-recurse continuation running at fuel \(\rho .\mathrm{numFree}\).

If every literal in \(\mathit{prefix}\) has variable not free in \(\rho \), then \(\mathrm{termSubTree}\, (\mathit{prefix} \mathbin {+\! \! +} \mathit{rest})\, \rho \, \mathrm{cont} = \mathrm{termSubTree}\, \mathit{rest}\, \rho \, \mathrm{cont}\).

If \(l.\mathrm{var} = v\), then \(\mathrm{termSubTree}\, (l :: \mathit{rest})\, (\rho [v \mapsto b])\, \mathrm{cont} = \mathrm{termSubTree}\, \mathit{rest}\, (\rho [v \mapsto b])\, \mathrm{cont}\), since after the update \(v\) is no longer free and \(l\) is skipped.

If a decision tree \(T\) computes a function \(f\) (i.e. \(T.\mathrm{eval}\, x = f(x)\) for all \(x\)), then its depth is at least the decision-tree depth of \(f\): \(T.\mathrm{depth} \ge \mathrm{dtDepth}\, f\).

The depth of the canonical decision tree for \(f|_\rho \) is at least the decision-tree depth of the restricted function: \((\mathrm{canonicalDTree}\, f\, \rho ).\mathrm{depth} \ge \mathrm{dtDepth}\, (\mathrm{restrictFn}\, (f.\mathrm{eval})\, \rho )\).

For any function \(f\) and restriction \(\rho \), the decision-tree depth of the restricted function is at most the number of free variables: \(\mathrm{dtDepth}\, (\mathrm{restrictFn}\, f\, \rho ) \le \rho .\mathrm{numFree}\).