Polynomial-time construction of tableau CNF

There exists one total function $f:B^*\to B^*$ satisfying $F(f)$ such that, for every specification $S$, $f(J(S))=E(F_S)$, where $F_S$ is the full tableau formula described here. This single polynomial-time function must obey the equation on encodings of all specifications, including ones with malformed allowed-window lists or zero fields; its values on words that encode no specification are unrestricted apart from total polynomial-time computability. Its polynomial running-time bound is measured against $|J(S)|$ on these encoded inputs. Here $B=\{\mathrm{false},\mathrm{true}\}$, $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. Write $F(f)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for every $w\in B^*$, compute output list $f(w)$ from input list $w$ in at most $p(|w|)$ steps. Different existential computation witnesses may use different machines and polynomials. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations. 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 specification encoding $J(S)$ is $E(G_S)$, where $G_S$ is the following clause list: first a clause of $s$ copies of $(\mathrm{true},0)$, then a clause of $i$ copies, then a clause of $r$ copies, then a clause of $|I|$ copies; next, for each list $x$ in $I$ in order, the clause $[(\mathrm{true},a):a\text{ runs through }x]$; next one clause formed in the same way from $A$; finally one such clause for each list in $H$ in order. These are raw formula encodings: no satisfiability condition is part of $J$. Empty lists and zero replication counts give empty clauses, which still have their clause delimiters. Write $E(F)$ for this Boolean-list encoding of a formula $F$: for each literal $(b,j)$, take $[b]$ followed by the little-endian canonical binary digits of $j$ (the digits of $0$ form the empty list), replace each bit $d$ by $[\mathrm{false},d]$, and append $[\mathrm{true},\mathrm{false}]$; concatenate these literal encodings within each clause and append $[\mathrm{true},\mathrm{true}]$; then concatenate the clause encodings in formula order. In particular $E([])=[]$. 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. 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. The supplied body is admitted with sorry; no proof of this assertion is supplied there.