fillList inserts the boxes with $e$ stars, with their values, into the trie of a tile (pruned encodings)

Let $P$ be a program of the light language whose procedure number $49$ is the body of fillList, and in which the routines nineFirst, nineNext, starFirst, horner, insert and sumTen meet their specifications for the limits $\mathrm{lim}$. Then fillList meets its specification for $\mathrm{lim}$:

consider a tile with encodings $\mathrm{enc}_A,\mathrm{enc}_B$ (functions on the leaves, strings of $L$ symbols) stored at $a_A,a_B$, a trie area of $\mathit{cap}$ cells at $\mathit{tr}$ holding the trie array $T$ whose length is in the cell $\mathit{fp}$, two scratch strings $\mathit{cur},\mathit{box}$ of $L$ cells, and a number of stars $e\le m-t$. Assume the surroundings of the tile are valid (in particular $t\le m\le L$, the products of the two encodings at the leaves with at most $m$ nines, multiplied by $10^m$, and $10^L$ fit in a word, and the areas lie in order in memory), the root of the tile's trie is nonzero, the trie array represents the tries in which the boxes with fewer than $e$ stars of this tile are already stored, and there is room for $11L$ cells per new box. Then for every depth $d$ with $d+2\le\mathrm{depth}$, $\mathrm{fillList}(e,\mathit{root},a_A,a_B,\mathit{tr},\mathit{fp},\mathit{cur},\mathit{box},L,m-t)$ ends within

steps, where $k$ is the number of boxes with $e$ stars; afterwards the trie area holds the array obtained by inserting each of these boxes with its value (for $e=0$ the product read from the two encodings; for $e\ge1$ the sum of the ten values of the boxes with one star fewer, by the recurrence of Lemma 29), and nothing changes outside the trie area, the cell $\mathit{fp}$ and the two scratch strings.

The only reads of the encodings are at leaves with at most $m$ nines, so the routine is correct for pruned encodings, which are wrong elsewhere.

“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.fillList]? = some fillListBody → NineFirstSpec lim P → NineNextSpec lim P → StarFirstSpec lim P → HornerSpec lim P → InsertSpec lim P → SumTenSpec lim P → FillListSpecP lim P.