Fix an assignment \(\alpha \) and a list of literals \(\mathit{lits}\), and let \(j\) be an index with \(j + 2 \le |\mathit{lits}|\). Then the auxiliary variable valuation associated with \(\alpha \), \(\mathit{lits}\), and \(j\) holds if and only if every one of the first \(j + 2\) literals of \(\mathit{lits}\) evaluates to false under \(\alpha \).

Let \(\mathit{cs} = (c_0,\dots ,c_{m-1})\) be a list of clauses over a variable type \(V\), let \(\mathit{idx} \in \mathbb {N}\) be a starting index, and let \(c_3\) be a 3-clause over the auxiliary variable type \(\mathtt{AuxVar}\, V\). Encode \(\mathit{cs}\) into 3-clauses by transforming each clause \(c_i\) at the shifted index \(\mathit{idx}+i\) and concatenating the outputs in order of increasing \(i\). Then \(c_3\) occurs in the resulting encoding of \(\mathit{cs}\) if and only if there is a position \(i \lt m\) for which \(c_3\) occurs among the 3-clauses produced by transforming the clause \(c_i\) at index \(\mathit{idx}+i\).

Let \(f = (C_0, \dots , C_{m-1})\) be a CNF formula over a variable type \(V\), and write \(\mathrm{Aux}(V)\) for the auxiliary variable type built from \(V\). For each index \(i\) with \(0 \le i \lt m\), let \(T_i\) be the list of \(3\)-clauses obtained by encoding the single clause \(C_i\) at index \(i\), and take the SAT-to-3-SAT encoding of \(f\) to be the \(3\)-CNF formula over \(\mathrm{Aux}(V)\) formed by concatenating \(T_0, T_1, \dots , T_{m-1}\) in order. Then a \(3\)-clause \(c\) over \(\mathrm{Aux}(V)\) occurs in the SAT-to-3-SAT encoding of \(f\) if and only if there exists an index \(i \lt m\) such that \(c\) occurs in \(T_i\).

Let \(l\) be a list over a type \(\alpha \), let \(n\) be a natural number, and suppose that dropping the first \(n\) entries of \(l\) leaves a nonempty list whose head is \(a\) (so that \(l\) has more than \(n\) entries and its \((n+1)\)-st entry is \(a\)). Then the prefix consisting of the first \(n+1\) entries of \(l\) equals the prefix consisting of the first \(n\) entries with \(a\) appended: taking \(n+1\) entries of \(l\) gives (taking \(n\) entries of \(l\)) followed by \([a]\).

Fix a clause index \(i\) and a clause presented as a list of literals over a variable type \(V\), and let \(\alpha : V \to \mathrm{Prop}\) be an assignment that makes at least one literal of the clause true. Let \(ml\) be a map lifting each literal over \(V\) to a literal over the extended type \(\mathtt{AuxVar}\, V\), and let \(\alpha _3\) be an assignment on \(\mathtt{AuxVar}\, V\) such that: (i) for every \(k\) the auxiliary variable \(y_{i,k}\) is true under \(\alpha _3\) exactly when all of the first \(k+2\) literals of the clause are false under \(\alpha \); and (ii) for every literal \(\ell \), the lifted literal \(ml(\ell )\) is true under \(\alpha _3\) if and only if \(\ell \) is true under \(\alpha \). Then for every chain counter \(j \ge 1\), letting \(\mathit{lits}\) be the suffix of the clause obtained by dropping its first \(j+1\) literals, every 3-clause in the chain built for clause \(i\) from \(\mathit{lits}\) starting at counter \(j\) is satisfied by \(\alpha _3\).

Let \(\alpha \) be a truth assignment of the variables \(V\), and let \(f\) be a CNF formula over \(V\) with clauses \(C_0, \dots , C_{m-1}\). Fix an index \(i\) with \(0 \le i \lt m\) and write \(C_i\) for the \(i\)-th clause. Let \(l\) be a literal over the auxiliary variable type \(\mathtt{AuxVar}\, V\) that is local to \(i\), meaning that every auxiliary variable \(y_{i',j}\) occurring in \(l\) satisfies \(i' = i\). Write \(\hat\alpha \) for the global assignment determined by \(\alpha \) and \(f\), which sends each original variable to its value under \(\alpha \) and each auxiliary variable \(y_{i',j}\) to the truth of the assertion that the first \(j+2\) literals of clause \(C_{i'}\) are all false under \(\alpha \); and write \(\alpha _i\) for the corresponding local assignment, built from clause \(C_i\) alone. Then \(l\) takes the same truth value under \(\hat\alpha \) as under \(\alpha _i\).

Let \(i\) be a natural number and let \(ml\) be a lifting map sending each literal over a variable type \(V\) to a literal over \(\mathtt{AuxVar}\, V\), and suppose that \(ml(l)\) is local to index \(i\) for every literal \(l\). Then, for every list of literals \(\mathit{lits}\) over \(V\) and every chain counter \(j\), each \(3\)-clause occurring in the chain of clauses built from \(\mathit{lits}\) (with clause index \(i\), lifting map \(ml\), and counter \(j\)) has all three of its literals local to index \(i\).

Fix a clause index \(i\) and let \(C\) be a clause over a variable type \(V\). If a 3-clause occurs in the list produced by encoding \(C\) at index \(i\), then each of its three literals is local to \(i\); that is, every auxiliary variable appearing in the 3-clause carries the index \(i\), while literals over original variables of \(V\) are local automatically.

Fix an assignment \(\alpha \) of truth values to the variables of a type \(V\), a CNF formula \(f\), and an index \(i\) with \(i \lt \mathrm{length}(f)\); let \(C\) be the \(i\)-th clause of \(f\), and let \(c_3\) be any of the 3-clauses produced by encoding \(C\) as clause number \(i\). Consider the global lifted assignment on \(\mathtt{AuxVar}\, V\), which sends each original variable \(v\) to \(\alpha (v)\) and each auxiliary chain variable \(y_{i',j}\) to the truth value of the assertion “the first \(j+2\) literals of the \(i'\)-th clause of \(f\) are all false under \(\alpha \)”, together with the local assignment that agrees with \(\alpha \) on original variables and sends \(y_{i,j}\) to the truth value of “the first \(j+2\) literals of \(C\) are all false under \(\alpha \)”. Then \(c_3\) is satisfied by the global assignment if and only if it is satisfied by the local assignment.

Let \(\alpha \) be a truth assignment on a variable set \(V\), and let \(C\) be a clause over \(V\) — a finite list of literals read as their disjunction — carrying the index \(i\). Assume \(\alpha \) satisfies \(C\), meaning at least one literal of \(C\) is true under \(\alpha \). Extend \(\alpha \) to an assignment \(\alpha _3\) on the enlarged variable set consisting of the original variables of \(V\) together with the auxiliary chain variables \(y_{i,j}\): leave each original variable at its value under \(\alpha \), and set \(y_{i,j}\) to true exactly when the first \(j+2\) literals of \(C\) are all false under \(\alpha \). Then every \(3\)-clause in the list obtained by encoding \(C\) at index \(i\) as \(3\)-clauses is satisfied by \(\alpha _3\).

Fix a clause index \(i\) and an assignment \(\alpha \) of truth values to the auxiliary variables. Let \(\ell \mapsto \widehat{\ell }\) be a map lifting each literal over the base variable type to a literal over the auxiliary-variable type, let \(j \ge 1\), and let \(L\) be a list of at least two literals over the base type such that the lifted literal \(\widehat{\ell }\) evaluates to false under \(\alpha \) for every \(\ell \) in \(L\). If every 3-clause of the chain encoding built from clause index \(i\), the lifting \(\ell \mapsto \widehat{\ell }\), the list \(L\), and the counter \(j\) is satisfied by \(\alpha \), then \(\alpha \) cannot also make the entry variable \(y_{i,\, j-1}\) true; these hypotheses taken together are contradictory.

Fix a variable type \(V\), a clause index \(c \in \mathbb {N}\), and a clause \(C\) over \(V\) — a finite list of literals read as their disjunction. Let \(\alpha \) be a truth assignment to the auxiliary variables (the original variables of \(V\) together with the fresh chain variables), and suppose that every \(3\)-clause produced by encoding \(C\) at index \(c\) is satisfied by \(\alpha \). Then \(C\) has at least one literal that is true under the assignment obtained by reading each original variable \(v\) through its copy among the auxiliary variables, i.e. \(v \mapsto \alpha (\mathrm{orig}\, v)\).