Polynomial bound on encoded tableau formula size

For every specification $S$, if $F_S$ is the full tableau formula described here, then $|E(F_S)|\le100(s+1)^2(i+2)^2(r+1)^8$. The inequality is non-strict, applies to every specification without any length or well-formedness assumptions on its lists, and counts bits of the encoded formula rather than clauses, literals, or numeric variable magnitudes. It includes zero values of $s,i,r$. 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. 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([])=[]$. 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.