Let \(l\) be a circuit literal on \(n\) variables and let \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\) be an assignment of Boolean values to those variables. Then evaluating \(l\) as a circuit literal at \(x\) yields the same Boolean value as first converting \(l\) to the corresponding switching-lemma literal and evaluating that at \(x\).

Fix a number of variables \(n\) and a Boolean assignment \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\). For any finite list of circuit literals \(\ell _1, \ldots , \ell _k\) on \(n\) variables, the right fold of logical conjunction over their evaluations, taken with initial value \(\mathrm{true}\) — that is, \(\ell _1.\mathrm{eval}(x) \wedge \bigl(\ell _2.\mathrm{eval}(x) \wedge \cdots \wedge (\ell _k.\mathrm{eval}(x) \wedge \mathrm{true})\bigr)\) — equals the term evaluation, on \(x\), of the list obtained by converting each circuit literal to its corresponding switching-lemma literal.

Let \(\ell _1, \dots , \ell _k\) be a list of circuit literals on \(n\) variables and let \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\) be an assignment. Then the right fold of disjunction over the literal evaluations, starting from \(\mathrm{false}\),

equals the clause evaluation on \(x\) of the term obtained by converting each circuit literal to its switching-lemma literal; that is, both equal \(\mathrm{true}\) precisely when some literal in the list holds under \(x\).

Let \(cs\) be a list of normal-form AND circuits on \(n\) variables, and suppose each member of \(cs\) is a base AND-clause (a conjunction of literals with distinct variable indices) rather than an AND-node built from OR-subcircuits. Form the normal-form OR circuit whose children are exactly the circuits in \(cs\), so that it computes their disjunction. Then for every assignment \(x : \mathrm{Fin}\, n \to \mathrm{Bool}\), this OR circuit evaluates at \(x\) to the same Boolean value as the DNF formula obtained from it by converting each child AND-clause into a term.

Let \(cs\) be a list of normal-form OR circuits on \(n\) variables, and suppose that every entry of \(cs\) is an OR-clause — that is, a base clause given by a list of literals, rather than an internal OR node. Then for every assignment \(x : \mathrm{Fin}\, n \to \mathbb {F}_2\), evaluating the normal-form AND circuit that conjoins the circuits in \(cs\) agrees with evaluating the CNF formula built from it: the value at \(x\) of the AND-node over \(cs\) equals the value at \(x\) of the CNF whose clauses are obtained by converting each OR-clause of \(cs\) into a disjunction of literals.

Let \(lits\) be a list of Boolean-circuit literals over \(n\) variables, and suppose the list of variable indices \(\mathrm{idx}(l)\) taken over the literals \(l\) in \(lits\) has no repeated entry. Then the term obtained from the normal-form AND-clause on \(lits\) by mapping each circuit literal to its switching-lemma literal, viewed as a list of literals, has no repeated entry.

Let \(lits\) be a list of circuit literals on \(n\) variables whose variable indices are pairwise distinct, and let \(C\) be the AND-clause built from \(lits\). If \(\ell _1\) and \(\ell _2\) are any two literals occurring in the term obtained by converting \(C\), and \(\ell _1\) and \(\ell _2\) have the same variable, then \(\ell _1 = \ell _2\).

Let \(lits\) be a list of circuit literals in \(n\) variables whose underlying variable indices are pairwise distinct. Then the term obtained by converting the OR-clause on \(lits\) — the list of switching-lemma literals produced by sending each circuit literal to its counterpart — has no repeated entries.

Let \(n \ge 0\) and let \(lits\) be a list of circuit literals over \(n\) variables whose variable indices are pairwise distinct, and form the term obtained by converting each literal of \(lits\) to a switching-lemma literal (recording the same variable and polarity). Then any two literals of this term that share the same variable \(\mathtt{var} \in \mathrm{Fin}\, n\) are in fact equal.

Fix \(n\), and let \(lits\) be a list of circuit literals on \(n\) variables whose variable indices are pairwise distinct. Form the normal-form AND-clause on this list, and convert it into a term by replacing each circuit literal with the corresponding switching-lemma literal. Then the width of that term — its number of literals — equals the length of \(lits\).

Let \(\mathrm{lits}\) be a list of circuit literals over \(n\) variables whose variable indices are pairwise distinct. Then the width of the term obtained from the OR-clause on \(\mathrm{lits}\) — that is, the term formed by converting each circuit literal to its corresponding literal — equals the number of literals in \(\mathrm{lits}\).

Let \(cs\) be a finite list of normal-form AND circuits on \(n\) variables, and let \(w \in \mathbb {N}\). Suppose every circuit in \(cs\) is a base clause — a list of literals whose variable indices are pairwise distinct — and that each such clause contains at most \(w\) literals. Then the DNF obtained from the normal-form OR circuit whose disjuncts are the circuits in \(cs\), by converting each AND-clause into a term, has width at most \(w\); that is, every term in it has at most \(w\) literals.

Fix \(n \in \mathbb {N}\), let \(cs\) be a list of normal-form OR circuits on \(n\) variables, and let \(w \in \mathbb {N}\). Suppose every circuit in \(cs\) is an OR-clause on some list of literals whose variable indices are pairwise distinct and whose length is at most \(w\). Form the normal-form AND circuit that conjoins all the members of \(cs\), and convert that circuit to a CNF formula by turning each OR-clause into a clause (a disjunction of its literals). Then this CNF formula has width at most \(w\); equivalently, each of its clauses contains at most \(w\) literals.

Let \(cs\) be a list of normal-form AND circuits on \(n\) variables, and suppose every element of \(cs\) is a clause — that is, each is given by a list of circuit literals whose variable indices are pairwise distinct. Consider the normal-form OR circuit that combines the members of \(cs\), and let its associated DNF formula be the list of terms obtained by converting each clause into a term (mapping every circuit literal to the corresponding switching-lemma literal with the same variable and polarity). Then every term of this DNF is duplicate-free: no term contains the same literal twice.

Fix \(n \in \mathbb {N}\) and a list \(c_1, \dots , c_m\) of normal-form AND circuits on \(n\) variables, and suppose each \(c_i\) is a base AND-clause — that is, \(c_i = \mathrm{clause}(\ell _1, \dots , \ell _{k_i})\) for some list of circuit literals whose variable indices are pairwise distinct. Let \(F\) be the DNF formula obtained from the OR circuit \(\mathrm{node}(c_1, \dots , c_m)\) by converting each clause \(c_i\) into the term formed by its literals. Then in every term of \(F\), any two literals that share the same variable are identical.

Let \(cs\) be a list of normal-form OR circuits on \(n\) variables, and suppose every member of \(cs\) is an OR-clause \(\mathrm{clause}\, (lits)\) whose literals have pairwise distinct variable indices. Form the depth-2 AND circuit that conjoins the circuits in \(cs\), and pass to the CNF formula obtained by turning each of these OR-clauses into a clause (a disjunction of literals). Then every clause of this CNF is a list of literals with no repeated entry.

Let \(cs\) be a list of normal-form OR circuits on \(n\) variables, and suppose every member of \(cs\) is a base OR-clause: for each \(c \in cs\) there is a list of circuit literals \(lits\), whose variable indices are pairwise distinct, with \(c = \mathrm{clause}\, lits\). Form the CNF formula of the AND-node over \(cs\) by converting each of these OR-clauses into a term. Then within any single clause of this CNF, any two literals that share the same variable are identical — in particular they carry the same negation flag.