Fix a list of literal–position pairs \(L\), a path \(P\) (a list of variable–direction pairs), and two restrictions \(\rho _0, \sigma \) on \(n\) variables. Running the clause-processing operation on these inputs yields a remaining path \(P'\) and an auxiliary list \(A\) of position–direction pairs (together with updated restrictions). Then

where \(\left\lvert \cdot \right\rvert \) denotes the number of entries of a list.

Run the clause-processing procedure on a nonempty list of free literals — each paired with its position index in the clause — and a nonempty canonical path, starting from restrictions \(\rho _0\) and \(\sigma \), and let its output consist of a remaining path and a list of accumulated auxiliary entries (among the updated restrictions). Writing \(a\) for the number of auxiliary entries produced, \(r\) for the length of the remaining path returned, and \(m\) for the length of the input path, we have

Consider the recursive encoding routine underlying Razborov’s proof of the switching lemma, which processes a DNF formula \(f\) on \(n\) variables against a width parameter \(w\) and a fuel bound, while carrying a path recorded as a list of variable–value pairs \((i,b) \in \mathrm{Fin}\, n \times \mathrm{Bool}\), two restrictions \(\rho _0, \sigma \) on \(n\) variables, and an accumulator \(\mathrm{acc}\) recorded as a list of index–value pairs in \(\mathbb {N}\times \mathrm{Bool}\); it returns a pair of lists. Then the second component of its output has length at most \(\left\lvert \mathrm{acc}\right\rvert + 2\, \left\lvert \mathrm{path}\right\rvert \), where \(\left\lvert \mathrm{acc}\right\rvert \) and \(\left\lvert \mathrm{path}\right\rvert \) denote the lengths of the accumulator and path lists.

Let \(f\) be a DNF formula on \(n\) Boolean variables, let \(w, d \in \mathbb {N}\), and let \(\rho \) be a restriction that is bad for \(f\) at depth \(d\); that is, the restriction of the Boolean function computed by \(f\) along \(\rho \) has decision-tree depth strictly greater than \(d\). Then the auxiliary component of the Razborov encoding of \(f\) and \(\rho \) with parameters \(w\) and \(d\) — the list of \((\mathbb {N}\times \mathrm{Bool})\) pairs returned as the second entry of the encoding — has length at most \(2d\).

Fix \(n\) and let \(\mathrm{lits}\) be a list of literals over \(\mathrm{Fin}\, n\), each paired with a position index, let \(\mathrm{path}\) be a list of variable–direction pairs, and let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables. Suppose \(v \in \mathrm{Fin}\, n\) is not the variable of any literal occurring in \(\mathrm{lits}\). Then the restriction \(\sigma '\) produced by processing \(\mathrm{lits}\) against \(\mathrm{path}\) starting from \(\rho _0\) and \(\sigma \) agrees with \(\sigma \) at \(v\), that is \(\sigma '(v) = \sigma (v)\).

Fix \(n\) and let \(\mathrm{lits}\) be a list of literals on \(n\) variables, each paired with a position index, and let \(\mathrm{path}\) be a list of variable–direction pairs. Given restrictions \(\rho _0,\sigma \) on \(n\) variables and a variable \(v\) such that \(v\) is not the variable of any literal occurring in \(\mathrm{lits}\), the updated restriction \(\rho _0'\) produced by processing the clause’s free literals of \(\mathrm{lits}\) against \(\mathrm{path}\) starting from \(\rho _0\) and \(\sigma \) agrees with \(\rho _0\) at \(v\); that is, \(\rho _0'(v) = \rho _0(v)\).

Fix \(n\), and let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables, let \(\ell \) be a list of literals each paired with its position index in a clause, and let a decision-tree path be given. Suppose the variable \(v\) is fixed under \(\rho _0\), i.e. \(\rho _0(v) \neq \mathrm{none}\). Then, after processing the clause’s free literals against the path — which returns updated versions of \(\rho _0\), \(\sigma \), together with the remaining path and the accumulated auxiliary data — the variable \(v\) remains fixed in the returned restriction \(\rho _0\): its value there is again not \(\mathrm{none}\). In other words, this process never frees a variable that was already fixed in \(\rho _0\).

Fix \(n\) and work with formulas on the variables \(\mathrm{Fin}\, n\). Let \(f\) be a DNF formula, \(w \in \mathbb {N}\) a width parameter, and \(\mathrm{fuel} \in \mathbb {N}\) a bound on the recursion depth; let \(\mathrm{path}\) be a list of variable–value pairs (elements of \(\mathrm{Fin}\, n \times \mathrm{Bool}\)), let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables, and let \(\mathrm{acc}\) be a list of index–value pairs holding the encoding accumulated so far. The recursive core of the Razborov encoder sends this data to a pair whose first component is again a restriction; write \(\gamma \) for that restriction. Then for every variable \(v\) that is fixed by \(\rho _0\) — that is, \(\rho _0(v) \neq \mathrm{none}\) — one has \(\gamma (v) = \sigma (v)\).

Fix a DNF formula \(f\) on \(n\) variables — a list of terms, each a conjunction of literals — together with a width parameter \(w \in \mathbb {N}\), a fuel bound \(\mathrm{fuel} \in \mathbb {N}\), a path \(P\) recording the variable–value pairs already committed (a list of elements of \(\mathrm{Fin}\, n \times \mathrm{Bool}\)), two restrictions \(\rho _0, \sigma : \mathrm{Fin}\, n \to \mathrm{Option}\, \mathrm{Bool}\), and an accumulator \(A\), a list of index–value pairs in \(\mathbb {N}\times \mathrm{Bool}\). The tail-recursive helper of Razborov’s encoding procedure, run from the initial accumulator \(A\) on these data, produces the same output as the corresponding run started from the empty accumulator, with the entries of \(A\) carried through unchanged; that is, the accumulator contributes to the result only additively and does not affect the encoding computed by the procedure itself.

Fix a DNF formula \(f\) on \(n\) variables, a width parameter \(w \in \mathbb {N}\), a fuel bound \(\in \mathbb {N}\), a partial path recorded as a list of variable–value pairs \((i,b) \in \mathrm{Fin}\, n \times \{ 0,1\} \), and two restrictions \(\rho _0, \sigma \) on the \(n\) variables. The auxiliary recursion underlying the Razborov encoding takes, in addition, a starting accumulator: a list of index–bit pairs in \(\mathbb {N}\times \{ 0,1\} \), and returns a pair. Then the first component of its output does not depend on that accumulator: running the recursion from an arbitrary accumulator yields the same first component as running it from the empty accumulator.

Fix \(n\) variables and consider the entry-processing step of the Razborov decoding procedure, which takes a term \(t\) (a conjunction of literals) over these variables, a natural number \(w\), two restrictions \(\sigma , \rho _0 \colon \mathrm{Fin}\, n \to \mathrm{Option}\, \mathrm{Bool}\), and a list \(\mathit{aux}\) of pairs \((\mathbb {N} \times \mathrm{Bool})\), and returns a restriction as the first component of its output. If \(\sigma \) leaves a variable \(v\) free (that is, \(\sigma (v) = \mathtt{none}\)), then the restriction produced by this step also leaves \(v\) free.

Fix a number of variables \(n\), and let \(D\) denote the recursive loop underlying Razborov’s decoder, which takes as input a DNF formula \(f\) on \(n\) variables, a width parameter \(w \in \mathbb {N}\), a fuel bound \(\mathrm{fuel} \in \mathbb {N}\), two restrictions \(\sigma \) and \(\rho _0\) on the \(n\) variables, and an auxiliary list of index–value pairs drawn from \(\mathbb {N}\times \mathrm{Bool}\), and returns a pair whose first component is again a restriction on the \(n\) variables. Then for every variable \(v\) with \(\sigma (v) = \mathrm{none}\), the first component of \(D(f, w, \mathrm{fuel}, \sigma , \rho _0, \mathrm{aux})\) also assigns \(\mathrm{none}\) to \(v\).

Fix a list of literals, each paired with its position index within a clause, a decision-tree path, a restriction \(\rho _0\), and two arbitrary restrictions \(\sigma _1\) and \(\sigma _2\) on \(n\) variables. Running the clause-processing procedure on this data with \(\sigma _1\) and with \(\sigma _2\) produces the same three outputs in each case: the same remaining path, the same updated restriction \(\rho _0\), and the same accumulated auxiliary list of (position index, path direction) pairs. In other words, of the procedure’s outputs only the returned \(\sigma \) can depend on the \(\sigma \) supplied as input; the path, the \(\rho _0\) component, and the auxiliary data are all unaffected by that choice.

Fix a DNF formula \(f\) on \(n\) variables, two natural-number parameters \(w\) and \(t\) (a fuel bound), a list of decisions pairing a variable with a Boolean value, and a restriction \(\rho _0\). Run the Razborov encoding loop on this data, started with empty auxiliary data, using a restriction \(\sigma \). Then the second component of the loop’s output is the same whether one supplies the restriction \(\sigma _1\) or the restriction \(\sigma _2\) in place of \(\sigma \); that is, this component does not depend on the \(\sigma \) argument.

Fix \(n\), and process the free literals of a clause against a decision-tree path: take a list \(\mathrm{lits}\) of literal–index pairs, a decision-tree path, and two restrictions \(\rho _0\) and \(\sigma \) on \(n\) variables, and write \(A\) for the accumulated list of index–direction pairs returned as auxiliary data. Then for every pair \((i, b) \in A\), the index \(i\) equals the index component \(j\) of some literal–index pair \((\ell , j) \in \mathrm{lits}\).

Let \(t\) be a term in \(n\) variables, let \(v \in \mathrm{Fin}\, n\) be a variable, and let \(\rho _0, \sigma \) be restrictions on \(n\) variables. Let \(\mathit{lits}\) be a list of literals each tagged with a natural-number position, and suppose that every tagged literal in \(\mathit{lits}\) occurs in the position-indexed enumeration of \(t\) (each literal of \(t\) paired with its index), and that no literal appearing in \(\mathit{lits}\) has variable \(v\). Consider the clause auxiliary data — the list of (position, direction) pairs — produced by processing \(\mathit{lits}\) against a path starting from \(\rho _0\) and \(\sigma \). Then for every pair \((i, b)\) in this auxiliary data, whenever the literals of \(t\) from position \(i\) onward form a nonempty list with leading literal \(\ell \), the variable of \(\ell \) is different from \(v\).

Let \(t\) be a term on \(n\) variables (a list of literals), let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables, let \(L\) be a list of literals each paired with a position index, and let \(P\) be a decision-tree path. Suppose that every pair \((\ell , i)\) in \(L\) occurs in the indexed enumeration of \(t\) — so that \(\ell \) is precisely the literal at position \(i\) of \(t\) — and that every literal appearing in \(L\) has its variable free under \(\rho _0\) (its value under \(\rho _0\) is \(\mathrm{none}\)). Then for each auxiliary entry \((i, b)\) produced by processing \(L\) against \(P\) starting from \(\rho _0\) and \(\sigma \), and for any literal \(\ell '\) and list \(r\) with \(t\) from position \(i\) onward equal to \(\ell ' :: r\) (i.e. discarding the first \(i\) literals of \(t\) leaves a nonempty list headed by \(\ell '\)), the variable of \(\ell '\) is free under \(\rho _0\).

Fix a term \(t\) over \(n\) variables (a list of literals), a restriction \(\sigma : \mathrm{Fin}\, n \to \mathrm{Option}\, \mathrm{Bool}\), a variable \(v\), and a finite list of entries, each a pair \((k, b)\) with \(k \in \mathbb {N}\) and \(b\) a Boolean. Process the entries left to right, starting from \(\sigma \): for an entry \((k, b)\), delete the first \(k\) literals of \(t\); if what remains is empty, leave the current restriction unchanged, and otherwise, writing \(l\) for the first remaining literal, reset the restriction to be free (unassigned) at the variable of \(l\). (The Boolean component \(b\) of each entry is never used.) Suppose that for every entry \((k, b)\) in the list, if deleting the first \(k\) literals of \(t\) leaves a nonempty list whose first literal is \(l\), then the variable of \(l\) is not \(v\). Then the restriction obtained after processing all the entries takes the same value at \(v\) as \(\sigma \) does.

Fix \(n\), and let \(t\) be a term over \(n\) variables, that is a list of literals, together with a restriction \(\rho _0 : \mathrm{Fin}\, n \to \mathrm{Option}\, \mathrm{Bool}\), a variable \(v \in \mathrm{Fin}\, n\), and a finite list of entries \((k_1, b_1), \dots , (k_m, b_m)\) with each \(k_i \in \mathbb {N}\) and each \(b_i\) a Boolean. Process these entries from left to right, starting from \(\rho _0\): for an entry \((k_i, b_i)\), delete the first \(k_i\) literals of \(t\); if what remains is nonempty with head literal \(l\), update the current restriction so that the variable of \(l\) is now assigned the fixed value \(b_i\), and otherwise leave the restriction unchanged. Suppose that for every entry \((k_i, b_i)\), whenever deleting the first \(k_i\) literals of \(t\) leaves a nonempty list with head literal \(l\), the variable of \(l\) is not \(v\). Then the restriction obtained after processing all the entries assigns \(v\) the same value as \(\rho _0\) does.

Let \(t\) be a term on \(n\) variables (a list of literals), let \((k_1,b_1),\dots ,(k_m,b_m)\) be a list of pairs in \(\mathbb {N}\times \mathrm{Bool}\), and let \(\rho \) be a restriction on \(n\) variables. Process the entries left to right, starting from \(\rho \): for the entry \((k_i,b_i)\), delete the first \(k_i\) literals of \(t\); if nothing remains, leave the current restriction unchanged, and otherwise reset the variable of the first surviving literal to free. Then for every variable \(v\) left free by \(\rho \), the restriction obtained at the end of this process still leaves \(v\) free.

Let \(t\) be a term on \(n\) variables — a list of literals, each carrying a variable and a negation flag — and refer to the position of a literal by its index in this list. Let \(\mathrm{lits}\) be a list of (literal, index) pairs, every one of which is the literal occurring at that index in \(t\); let \(\mathrm{path}\) be a list of (variable, Boolean) pairs; and let \(\rho _0\), \(\sigma \), and \(\sigma _{\mathrm{dec}}\) be restrictions on \(n\) variables, with \(v\) a distinguished variable. Feeding \(\mathrm{lits}\), \(\mathrm{path}\), \(\rho _0\), and \(\sigma \) to the clause-processing procedure returns an updated restriction \(\rho _0'\) together with an auxiliary list \(A\) of (index, direction) pairs. Suppose \(\rho _0(v)\) is free while \(\rho _0'(v)\) is fixed. Then processing \(A\) from left to right, starting from \(\sigma _{\mathrm{dec}}\) and, at each entry whose index component is \(i\), resetting to free the variable of the \(i\)-th literal of \(t\) whenever \(t\) has a literal at position \(i\) (and otherwise leaving the restriction unchanged), yields a restriction that is free at \(v\).

Let \(t\) be a term on \(n\) variables (a list of literals), and let \(\mathrm{lits}\) be a list of literal–index pairs, each of which is required to be a literal of \(t\) together with its position — that is, every pair in \(\mathrm{lits}\) occurs in the list obtained by pairing each literal of \(t\) with its index. Fix a path, restrictions \(\rho _0\), \(\sigma \), and \(\rho _0^{\mathrm{dec}}\) on the \(n\) variables, and a variable \(v\) with \(\rho _0(v) = \rho _0^{\mathrm{dec}}(v)\). Processing \(\mathrm{lits}\) against the path starting from \(\rho _0\) and \(\sigma \) yields an updated restriction \(\rho _0'\) together with an auxiliary list of pairs \((i, b)\). Now form a restriction by folding over this auxiliary list, left to right, starting from \(\rho _0^{\mathrm{dec}}\): an entry \((i, b)\) leaves the current restriction unchanged if \(t\) has no literal at position \(i\), and otherwise fixes the variable of the literal at position \(i\) to the Boolean value \(b\). Then the restriction so obtained and \(\rho _0'\) take the same value at \(v\).

Let \(t\) be a term on \(n\) variables, and let \(L\) be a list of literal–index pairs each of which occurs at its recorded position in \(t\) (that is, every pair in \(L\) lies in the enumeration of \(t\) that tags each literal with its index). Fix restrictions \(\rho _0\), \(\sigma \), and \(\rho _0^{\mathrm{dec}}\) on \(n\) variables, a decision-tree path \(P\), and a variable \(v\) that \(\rho _0\) leaves free. Running the clause-processing routine on \(L\), \(P\), \(\rho _0\), \(\sigma \) produces an updated restriction \(\rho _0'\) together with auxiliary data \(A\), a list of (position index, direction) pairs, and assume that \(\rho _0'\) assigns a value at \(v\). Consider the restriction obtained by folding \(A\) over the starting restriction \(\rho _0^{\mathrm{dec}}\), where each pair \((i, b)\) leaves the current restriction unchanged if \(t\) has no literal at position \(i\), and otherwise sets the variable of the \(i\)-th literal of \(t\) to the value \(b\). Then this folded restriction agrees with \(\rho _0'\) at \(v\); that is, its value at \(v\) equals \(\rho _0'(v)\).

Fix a number \(n\) of variables, and let \(\rho _0\) and \(\sigma \) be restrictions on them. Suppose the free literals of a clause are given as a list, each literal paired with its position index, and let a decision-tree path be a list of variable–direction pairs whose length is at least the number of literals. Running the clause-processing operation on this list, this path, \(\rho _0\), and \(\sigma \) returns an updated restriction \(\rho _0'\) in place of \(\rho _0\). If a variable \(v\) is free under \(\rho _0\) and remains free under \(\rho _0'\), then no literal on the list has \(v\) as its underlying variable.

Consider the routine that processes one clause’s free literals — a list of literals, each tagged with its position index in the clause — against a canonical decision-tree path, starting from a restriction \(\rho _0\) and a restriction \(\sigma \), and returning (among other data) an updated restriction \(\sigma '\). Fix the list of literals, the path, the restriction \(\rho _0\), and a variable \(v\). If two starting restrictions \(\sigma _1\) and \(\sigma _2\) agree at \(v\), that is \(\sigma _1(v) = \sigma _2(v)\), then the updated restrictions produced from \(\sigma _1\) and from \(\sigma _2\) also agree at \(v\); equivalently, the value at \(v\) of the updated \(\sigma \)-restriction depends only on the starting value \(\sigma (v)\).

Fix \(n\), and let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables. Run the clause-processing procedure on a list of literals (each paired with its position index) together with a decision-tree path, starting from \(\rho _0\) and \(\sigma \), and write \(\rho _0'\) and \(\sigma '\) for the two restrictions it returns. If a variable \(v\) is free under the input, \(\rho _0(v) = \mathrm{none}\), and remains free under the output, \(\rho _0'(v) = \mathrm{none}\), then the procedure has not altered \(\sigma \) at \(v\) either: \(\sigma '(v) = \sigma (v)\).

Fix a DNF formula \(f\) on \(n\) variables, a width \(w\), a fuel bound, a decision path (a list of variable–direction pairs), and a base restriction \(\rho _0\). The recursive worker of the Razborov encoding, run on these inputs together with a running restriction \(\sigma \) and empty auxiliary data, returns among its outputs a restriction; write \(R(\sigma )\) for this first output component. Let \(v\) be a variable that is left free by \(\rho _0\) and by two running restrictions \(\sigma _1\) and \(\sigma _2\), meaning \(\rho _0(v)\), \(\sigma _1(v)\), and \(\sigma _2(v)\) are all undefined. Then the two runs agree at \(v\): \(R(\sigma _1)(v) = R(\sigma _2)(v)\).

Work over \(n\) Boolean variables, where a *literal* is a variable together with a negation flag, a *term* is a list of literals (a conjunction), and a *restriction* \(\rho : \mathrm{Fin}\, n \to \mathrm{Option}\, \mathrm{Bool}\) fixes some variables and leaves the rest free. Let \(t\) be a term whose length is at most a bound \(w\), let \(\mathit{lits}\) be a list of literals each paired with a position index, every such pair occurring among the indexed entries of \(t\), and fix a canonical decision-tree path together with restrictions \(\rho _0^{\mathrm{enc}}, \sigma ^{\mathrm{enc}}, \sigma ^{\mathrm{dec}}, \rho _0^{\mathrm{dec}}\) and a remainder list. Then, running the decoder’s entry-processing routine on the auxiliary data emitted when this clause’s free literals are consumed against the path — followed by the termination marker \((w, \mathrm{false})\) and the remainder — yields the same \(\sigma \)- and \(\rho _0\)-restrictions as folding the corresponding per-entry updates directly over that auxiliary data, with the remainder left unconsumed.

Let \(\ell \) be a literal with variable \(v\) and negation flag \(b\), let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables, and let \(\mathit{lits}\) be a list of literals (each tagged with its position index in the clause) run against a decision-tree path. Suppose that every literal in \(\mathit{lits}\) whose variable is \(v\) is equal to \(\ell \), and that \(\sigma \) does not already assign \(v\) the fixed value \(b\), i.e. \(\sigma (v) \neq \mathrm{some}\, b\). Then the restriction \(\sigma '\) obtained as the \(\sigma \)-component of processing \(\mathit{lits}\) against the path starting from \(\rho _0\) and \(\sigma \) still does not assign \(v\) the value \(b\), i.e. \(\sigma '(v) \neq \mathrm{some}\, b\).

Fix \(n\), a list \(\mathit{lits}\) whose entries are literals paired with clause positions, a path \(\mathit{path}\) presented as a list of variable–direction pairs, and two restrictions \(\rho _0,\sigma \) on \(n\) variables. Suppose the pair \((l,\mathit{idx})\) occurs in \(\mathit{lits}\), that every entry of \(\mathit{lits}\) whose variable equals \(\mathrm{var}(l)\) is equal to \(l\) itself, and that \(\rho _0\) leaves \(\mathrm{var}(l)\) free. Processing \(\mathit{lits}\) against \(\mathit{path}\) from the starting restrictions \(\rho _0\) and \(\sigma \) yields an updated restriction \(\rho _0'\), an updated restriction \(\sigma '\), a remaining path, and accumulated auxiliary data. If \(\rho _0'\) still leaves \(\mathrm{var}(l)\) free, then the remaining path yielded is empty.

Let \(\rho _0\) and \(\sigma \) be restrictions on \(n\) variables, let a list of literals be given (each paired with its position index inside its clause), and let a decision-tree path be given as a list of variable–direction pairs, with at least as many path entries as literals in the list. Process the literals against the path starting from \(\rho _0\) and \(\sigma \), and let \(\rho _0'\) be the updated first restriction that this returns. If some literal in the list has underlying variable \(v\), then \(v\) is not free in \(\rho _0'\); that is, \(\rho _0'(v)\) is a fixed Boolean value rather than the free marker.

Fix \(n\), and let \(f\) be a DNF formula on \(n\) variables and \(w\) a natural number. Let \(\rho _0\), \(\sigma \), \(\sigma _{\mathrm{dec}}\), and \(\rho _0^{\mathrm{dec}}\) be restrictions on \(n\) variables (each variable either assigned a Boolean value or left free), and let \(d\) be a fuel bound. Suppose that \(\sigma \) leaves free every variable that \(\rho _0\) leaves free, and that \(\sigma _{\mathrm{dec}}\) agrees with \(\sigma \) on every variable — both those that \(\rho _0\) leaves free and those that \(\rho _0\) fixes. Then running the Razborov decoding loop on \(f\), with width \(w\), fuel \(d\), working restrictions \(\sigma _{\mathrm{dec}}\) and \(\rho _0^{\mathrm{dec}}\), and the empty list of emitted advice, yields an output whose first component is exactly \(\sigma \).

Let \(f\) be a DNF formula on \(n\) variables in which no term contains two distinct literals over the same variable, and let \(w\) be a natural-number width parameter. Fix two restrictions \(\rho _0\) and \(\sigma \) on the \(n\) variables such that \(\sigma \) leaves a variable free whenever \(\rho _0\) does (that is, \(\rho _0(v)\) undefined implies \(\sigma (v)\) undefined), and let \(t\) be the first term of \(f\), in list order, that is not killed by \(\rho _0\). Run the recursion at the heart of the Razborov encoding on \(f\) and \(w\) — with any fuel budget, any decision path, initial data \(\rho _0\) and \(\sigma \), and empty accumulated data — and write \(\rho \) for the restriction it returns as its first component. Then for every literal \(l\) of \(t\) whose variable is left free by \(\rho _0\), the output restriction \(\rho \) does not kill \(l\): it does not fix the variable of \(l\) to the value that would make \(l\) false.