Fix a number \(n\) of variables. Let \(\mathrm{lits}\) be a list of literals, each paired with its position index in a clause; let \(\mathrm{path}\) be a decision-tree path; let \(\rho _0\) and \(\sigma \) be restrictions on the \(n\) variables; and let \(v\) be a variable. Let \(\rho _0'\) denote the updated restriction produced in place of \(\rho _0\) by the clause-processing procedure applied to \(\mathrm{lits}\), \(\mathrm{path}\), \(\rho _0\), and \(\sigma \). If \(\rho _0'\) leaves \(v\) free, then \(\rho _0\) already leaves \(v\) free.

Let \(f\) be a DNF formula on \(n\) variables, viewed as an ordered list of terms, in which no term contains two distinct literals on the same variable. Fix restrictions \(\rho _0\) and \(\sigma \) such that \(\sigma \) leaves free every variable that \(\rho _0\) leaves free, and suppose that \(t_{\mathrm{clause}}\) is the first term of \(f\), in list order, that is not killed by \(\rho _0\). Let \(\rho _{\mathrm{enc}}\) be the restriction obtained as the first component of the output of the Razborov encoding procedure applied to \(f\) — with width parameter \(w\) and the given fuel and path arguments — started from \(\rho _0\) and \(\sigma \), and let \(\rho _{\mathrm{dec}}\) be any restriction that agrees with \(\rho _0\) on every variable that \(\rho _0\) fixes and with \(\rho _{\mathrm{enc}}\) on every variable that \(\rho _0\) leaves free. Then \(t_{\mathrm{clause}}\) is also the first term of \(f\), in list order, that is not killed by \(\rho _{\mathrm{dec}}\).

Fix a natural number \(n\), a restriction \(\rho _0\) on \(n\) variables, and a list \(t\) of literals. Enumerate \(t\) as the list of pairs \((\ell , i)\), where \(\ell \) ranges over the literals of \(t\) and \(i\) is the position of \(\ell \) in \(t\), and keep only those pairs whose literal’s variable is a free variable of \(\rho _0\). Then every pair \((\ell , i)\) surviving this filter is itself one of the enumerated pairs of \(t\), and its literal’s variable \(v\) is free under \(\rho _0\), meaning \(\rho _0\) leaves \(v\) unset.

Let \(t\) be a term on \(n\) variables (a list of literals), let \(L\) be a list of literals each paired with a natural-number position, let \(\pi \) be a path (a list of variable–direction pairs), and let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables. Suppose every pair in \(L\) occurs in the indexed enumeration of \(t\), so that each \((l,i)\in L\) records a literal \(l\) sitting at position \(i\) of \(t\). Run the clause-processing procedure that consumes the free literals of \(L\) against \(\pi \) starting from \(\rho _0\) and \(\sigma \), and let \(\rho _0'\) denote its updated \(\rho _0\)-restriction and \(A\) its list of clause auxiliary entries. If \(\rho _0'\) leaves the variable \(v\) free, then for every entry \((i,d)\in A\) and every literal \(l\) such that deleting the first \(i\) literals of \(t\) leaves a nonempty list with head \(l\), the variable of \(l\) is not \(v\).

Fix a DNF formula \(f\) on \(n\) variables, two restrictions \(\rho _0\) and \(\sigma \), a fuel budget, and a path \(\mathrm{step} :: \mathrm{rest}\) consisting of a first variable–direction pair \(\mathrm{step}\) followed by a list \(\mathrm{rest}\) of further such pairs. Suppose \(t_{\mathrm{clause}}\) is the first term of \(f\) that is not killed by \(\rho _0\), and that, listing the literals of \(t_{\mathrm{clause}}\) each tagged with its position in the term and keeping only those whose variable is free under \(\rho _0\), this filtered list is nonempty, of the form \(\mathit{fl} :: \mathit{fls}\). Then the first component of the encoder run at fuel one greater on the whole path \(\mathrm{step} :: \mathrm{rest}\) coincides with the first component of the encoder run at the smaller fuel started from the state obtained by processing the clause’s free literals \(\mathit{fl} :: \mathit{fls}\) against that same path from \(\rho _0\) and \(\sigma \).

Let \(t\) be a term on \(n\) variables, let \(\mathit{lits}\) be a list of literals each tagged with a position index, and let \(\mathit{path}\) be a list of variable–direction pairs. Let \(\rho _0\), \(\sigma \), and \(\sigma _{\mathrm{dec}}\) be restrictions on \(n\) variables, and suppose that every variable occurring in a literal of \(\mathit{lits}\) is free under \(\rho _0\); that every tagged literal in \(\mathit{lits}\) occurs at its recorded position in \(t\); that \(\sigma \) is free at every variable that is free under \(\rho _0\); and that \(\sigma _{\mathrm{dec}}\) agrees with \(\sigma \) at every variable that \(\rho _0\) fixes. Write \((\mathit{path}', \rho _0', \sigma ', a)\) for the result of processing \(\mathit{lits}\) along \(\mathit{path}\) starting from \(\rho _0\) and \(\sigma \), where \(a\) is the accumulated list of (position, direction) pairs. Then for every variable \(v\) that \(\rho _0'\) fixes, the restriction obtained by folding over \(a\) — starting from \(\sigma _{\mathrm{dec}}\) and, for each recorded pair with position \(i\), freeing the variable of the literal at position \(i\) in \(t\) (and leaving the restriction unchanged when \(i\) lies beyond the end of \(t\)) — agrees with \(\sigma \) at \(v\).

Let \(t\) be a term on \(n\) variables (a list of literals), let \(\mathit{lits}\) be a list of literals each paired with a position index, let a decision-tree path be given, and let \(\rho _0\), \(\sigma \), and \(\rho _{0,\mathrm{dec}}\) be restrictions on the \(n\) variables. Assume that every literal in \(\mathit{lits}\) has its variable left free by \(\rho _0\), that every pair in \(\mathit{lits}\) occurs in the indexed enumeration of \(t\) (each literal of \(t\) paired with its position), and that \(\rho _{0,\mathrm{dec}}\) agrees with \(\rho _0\) at every variable that \(\rho _0\) fixes. Write \(\rho _0^{\ast }\) for the restriction and \(A\) for the auxiliary list of index–direction pairs produced by processing \(\mathit{lits}\) against the path starting from \(\rho _0\) and \(\sigma \). Reconstruct a restriction from \(\rho _{0,\mathrm{dec}}\) by folding over \(A\): for each pair \((i,b)\), if deleting the first \(i\) literals of \(t\) leaves a nonempty list, set the variable of that list’s head literal to \(b\), and otherwise leave the restriction unchanged. Then at every variable \(v\) at which \(\rho _0^{\ast }\) is defined, this reconstructed restriction and \(\rho _0^{\ast }\) take the same value.

Fix a DNF formula \(f\) on \(n\) variables whose width is at most \(w\) and in which no term repeats a variable (within a single term, any two literals on the same variable are equal). Given a fuel budget, a partial decision path, and restrictions \(\rho _0\) and \(\sigma \), let the encoding procedure, started with empty auxiliary data, return a restriction \(\rho ^\ast \) together with an output list \(c\); let \(D\) denote the decoding procedure run on \(c\) with a fuel budget \(m\) and starting restrictions \(\sigma _{\mathrm{dec}}\) and \(\rho _{0,\mathrm{dec}}\). Suppose that \(\sigma \) is free wherever \(\rho _0\) is free; that on every variable left free by \(\rho _0\) both \(\sigma _{\mathrm{dec}}\) and \(\rho _{0,\mathrm{dec}}\) agree with \(\rho ^\ast \); that on every variable fixed by \(\rho _0\) one has \(\sigma _{\mathrm{dec}} = \sigma \) and \(\rho _{0,\mathrm{dec}} = \rho _0\); and that \(m\) is at least one more than the length of \(c\). Then the restriction returned by \(D\) equals \(\sigma \).

Let \(f\) be a DNF formula on \(n\) variables whose width is at most \(w\), and suppose that within every term of \(f\) any two literals naming the same variable are in fact equal. Given a natural number serving as a step budget for the encoder, a finite list of variable–value pairs, and a restriction \(\rho \) on the \(n\) variables, encoding \(\rho \) relative to \(f\) produces a list from which the decoder — run with a step budget one larger than that list’s length — recovers \(\rho \) exactly.

Let \(f\) be a DNF formula on \(n\) variables whose width is at most \(w\), and suppose that no term of \(f\) contains two distinct literals on the same variable (within each term, any two literals sharing a variable coincide). Let \(\rho \) be a restriction that is bad for \(f\) at depth \(d\), meaning the restriction of the Boolean function computed by \(f\) along \(\rho \) has decision-tree depth strictly greater than \(d\). Writing \((\gamma , \mathrm{aux})\) for the pair produced by the Razborov encoding of \(f\), \(w\), \(d\), \(\rho \), the Razborov decoding of \((\gamma , \mathrm{aux})\) with parameters \(f\) and \(w\) returns the original restriction \(\rho \).