If the restriction component \((\mathrm{processClauseLits}\ \mathit{lits}\ \mathit{path}\ \rho _0\ \sigma ).2.1\) is unset at a variable \(v\) (equal to none), then \(\rho _0\) is already unset at \(v\), i.e. \(\rho _0\, v = \texttt{none}\).

For a DNF \(f\) with no two literals in a term sharing a variable, suppose the encoder finds \(t_{\mathrm{clause}}\) as the first term not killed by \(\rho _0\). Under the agreement hypotheses relating \(\rho _0\), \(\sigma \), and the decoder restriction \(\rho _{0,\mathrm{dec}}\) (agreeing with the encoder output on free variables and with \(\rho _0\) on set variables), the decoder restriction also finds \(t_{\mathrm{clause}}\) as its first non-killed clause.

If a pair \(p\) lies in the list obtained by filtering the indexed literals of \(t_{\mathrm{clause}}\) (its zipIdx) to those whose variable is free under \(\rho _0\), then \(p\) is a member of \(t_{\mathrm{clause}}.\mathrm{zipIdx}\) and its variable is free, i.e. \(\rho _0\, (p.1.\mathrm{var}) = \texttt{none}\).

Assuming every literal in \(\mathit{lits}\) is an indexed literal of the term \(t\), if the restriction component \((\mathrm{processClauseLits}\ \mathit{lits}\ \mathit{path}\ \rho _0\ \sigma ).2.1\) is unset at \(v\), then no auxiliary entry produced by the fold targets \(v\): for every aux entry \(e\), dropping \(e.1\) literals of \(t\) to a head literal \(l\) gives \(l.\mathrm{var} \neq v\).

When the encoder finds \(t_{\mathrm{clause}}\) as the first clause not killed by \(\rho _0\) and its filtered free-variable literals form a nonempty list \(\mathit{fl}::\mathit{fls}\), the first component of the encoder run with fuel \(\mathrm{fuel}+1\) on path \(\mathit{step}::\mathit{rest}\) equals the first component of the recursive encoder run with fuel \(\mathrm{fuel}\) on the processed state \(\mathrm{pcl} = \mathrm{processClauseLits}\, (\mathit{fl}::\mathit{fls})\, (\mathit{step}::\mathit{rest})\, \rho _0\, \sigma \).

Under the freeness and membership hypotheses on \(\mathit{lits}\) and the agreement of \(\sigma _{\mathrm{dec}}\) with \(\sigma \) on variables set by \(\rho _0\), the \(\sigma \)-fold over the aux entries (which clears \(l.\mathrm{var}\) for each dropped head literal \(l\)) applied to \(\sigma _{\mathrm{dec}}\) agrees with \(\sigma \) at every variable \(v\) where the processed restriction \((\mathrm{processClauseLits}\ \mathit{lits}\ \mathit{path}\ \rho _0\ \sigma ).2.1\) is set.

Under the freeness and membership hypotheses on \(\mathit{lits}\) and the agreement of \(\rho _{0,\mathrm{dec}}\) with \(\rho _0\) on variables set by \(\rho _0\), the \(\rho _0\)-fold over the aux entries (which sets \(l.\mathrm{var}\) to \(e.2\) for each dropped head literal \(l\)) applied to \(\rho _{0,\mathrm{dec}}\) agrees with the processed restriction \((\mathrm{processClauseLits}\ \mathit{lits}\ \mathit{path}\ \rho _0\ \sigma ).2.1\) at every variable \(v\) where that restriction is set.

The generalized round-trip statement: for a DNF \(f\) of width at most \(w\) with distinct variables per term, given decoder states \(\sigma _{\mathrm{dec}}\) and \(\rho _{0,\mathrm{dec}}\) that satisfy the round-trip invariants relative to the encoder output and enough decoder fuel, the first component of the decoder run on the encoder’s output list equals the original \(\sigma \). This is the inductive core from which the closed round trip follows.

Specializing the generalized round trip to \(\sigma = \rho _0 = \rho \): for a width-\(w\) DNF \(f\) with distinct variables per term, running the encoder on \(\rho \) and then running the decoder (with one more than the encoded list length as fuel) on the encoder output recovers \(\rho \).

For a width-\(w\) DNF \(f\) with distinct variables per term and a bad restriction \(\rho \) for \(f.\mathrm{eval}\) at depth \(d\), decoding the Razborov encoding of \(\rho \) returns \(\rho \): \(\mathrm{razborovDecode}\ f\ w\ (\mathrm{razborovEncode}\ f\ w\ d\ \rho ) = \rho \).