Initial configuration constraints

For every specification $S$, assignment $\tau:\mathbb N\to B$, and total function $T:\mathbb N\times\mathbb N\to\mathbb N$, assume the encoding condition described here. Under that hypothesis, every clause of the initial formula is true under $\tau$ if and only if $\forall c<W,\ T(0,c)\in I_c$. A missing required initial list is empty and makes the right-hand condition false; the theorem retains the encoding hypothesis in that case. Here $S=(s,i,r,I,A,H)$ has $s,i,r\in\mathbb N$, a list $I$ of lists of natural numbers, a list $A$ of natural numbers, and a list $H$ of lists of natural numbers, with no validity restrictions on these fields. Put $W=i+2\ge2$, $Q=r+1\ge1$, and $v(t,c,a)=(tW+c)Q+a$. The list $I_c$ is the zero-based $c$th list of $I$, or the empty list when that entry is missing. The encoding condition for $\tau:\mathbb N\to B$ and $T:\mathbb N\times\mathbb N\to\mathbb N$ is the conjunction of $\forall t\le s,\ \forall c<W,\ T(t,c)<Q$ and $\forall t\le s,\ \forall c<W,\ \forall a<Q,\ \tau(v(t,c,a))=\mathrm{true}\ \Longleftrightarrow\ T(t,c)=a$. Values of $T$ outside this rectangle and Boolean values not constrained by these displayed indices are unrestricted. The initial formula has, in increasing $c<W$ and then increasing $a<Q$, the negative unit clause $[(\mathrm{false},v(0,c,a))]$ exactly when $a\notin I_c$. A formula is a finite list of clauses, each clause a finite list of literals $(b,j)\in B\times\mathbb N$. Under an assignment $\tau:\mathbb N\to B$, the literal $(b,j)$ is true exactly when $\tau(j)=b$, a clause is true exactly when some literal in it is true, and a formula is true exactly when every clause is true. Thus an empty clause is false and an empty formula is true. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The supplied body is admitted with sorry; no proof of this assertion is supplied there.