Tableau formula correctness

For every specification $S$, there exists a Boolean assignment $\tau:\mathbb N\to B$ making every clause of the full tableau formula true if and only if there exists a total natural-valued two-argument function $T$ satisfying the validity condition described here. Neither side additionally assumes the stricter specification predicate; all specifications, including those with zero fields, missing lists, and empty accepting lists, are quantified over. 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 full tableau formula is the concatenation, in order, of the cell, initial, boundary, accepting, and transition formulas described here. The cell formula consists, in increasing $t=0,\ldots,s$ and then increasing $c=0,\ldots,W-1$, of the clause of all positive literals $(\mathrm{true},v(t,c,a))$ for $a=0,\ldots,Q-1$, followed by every two-literal clause $[(\mathrm{false},v(t,c,a)),(\mathrm{false},v(t,c,b))]$ with $0\le a<b<Q$, ordered first by $a$ and then by $b$. 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$. The boundary formula has, for each $t=0,\ldots,s$ in order, the two positive unit clauses at $v(t,0,0)$ and $v(t,i+1,0)$, in that order. The accepting formula is a list containing one clause; its literals are $(\mathrm{true},v(s,c,a))$ for every $0\le c<W$ and $0\le a<Q$ with $a\in A$, ordered first by $c$ and then by $a$. If no such $a$ exists, this is an empty clause rather than an empty formula. The transition formula ranges in increasing order over $0\le t<s$, $0\le c<i$, and lexicographically over all six-tuples $u\in\{0,\ldots,Q-1\}^6$ absent from the list $H$. For each such tuple it has the clause of the six negative literals at positions $(t,c),(t,c+1),(t,c+2),(t+1,c),(t+1,c+1),(t+1,c+2)$ with symbol indices given by the corresponding entries of $u$, in that order. If $s=0$ or $i=0$, the transition formula is empty. The validity condition for $T:\mathbb N\times\mathbb N\to\mathbb N$ is the conjunction of: $\forall t\le s,\ \forall c<W,\ T(t,c)<Q$; $\forall c<W,\ T(0,c)\in I_c$; $\forall t\le s,\ T(t,0)=0\land T(t,i+1)=0$; $\exists c<W,\ T(s,c)\in A$; and $\forall t<s,\ \forall c<i,\ [T(t,c),T(t,c+1),T(t,c+2),T(t+1,c),T(t+1,c+1),T(t+1,c+2)]\in H$. Values outside the rectangle are unrestricted; the last condition is vacuous for $s=0$ or $i=0$, and a missing required $I_c$ or an empty $A$ makes the condition unsatisfiable. 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.