allTiles builds the tries of all tiles of the Theorem 30 data structure (pruned encodings)

Let $P$ be a program of the light language whose procedure number $51$ is the body of allTiles, and in which the routine tile meets its specification for the limits $\mathrm{lim}$. Then allTiles meets its specification for $\mathrm{lim}$:

consider $n_B$ row bands and $n_B$ column bands whose encodings $\mathrm{enc}_A(\beta),\mathrm{enc}_B(\beta)$ are stored at $a_{\mathrm{ENCA}}+\beta\,10^L$ and $a_{\mathrm{ENCB}}+\beta\,10^L$, a table of $n_B^2$ root cells from $a_R$, a trie area of $\mathit{cap}$ cells from $\mathit{tr}$ that holds the trie array $[0]$ (its length in the cell $\mathit{fp}$), and scratch strings $\mathit{cur},\mathit{box}$. Assume the standing assumptions on the limits, $t\le m\le L$, that some bounds $A,B$ on the encodings at the leaves with at most $m$ nines satisfy $10^m AB\le\mathrm{word}$, that $10^L\le\mathrm{word}$, that $1+n_B^2\cdot11\,(1+L\,|\mathcal B|)\le\mathit{cap}$ where $|\mathcal B|$ is the number of boxes of a tile, and that the areas lie in this order without overlap below the end of memory. Then for every depth $d$ with $d+4\le\mathrm{depth}$, the call $\mathrm{allTiles}(a_{\mathrm{ENCA}},a_{\mathrm{ENCB}},n_B,10^L,a_R,\mathit{tr},\mathit{fp},\mathit{cur},\mathit{box},L,m-t)$ ends within

steps; afterwards the trie area holds the tries of all $n_B^2$ tiles (tile $(\beta,\beta')$ built from row band $\beta$ and column band $\beta'$, each holding the values of all its boxes), the root cells hold their roots, and no cell below $\mathit{cur}$ or behind the trie area has changed.

Only the leaves with at most $m$ nines of the encodings are read, so the routine works with the pruned encodings left by the shared stage.

“Procedure $p$ meets its specification within $T$ steps” means: called at any depth $d$ allowed by the hypothesis, with the given argument values and a memory $\mu$ satisfying the precondition, the body of $p$ terminates within $T$ steps without violating the limits, and the returned value and final memory satisfy the postcondition.

Formalization Note The statement is P[Proc.allTiles]? = some allTilesBody → TileSpecP lim P → AllTilesSpecP lim P.