Theorem 17 host: the residue classes and the chunks, followed by any statement (classes_then)

A sequencing lemma for the host program of Theorem 17 (the reduction of Exact Triangle to Lop-AE-SparseTri), about the two calls that sort the pairs by residue class and cut the classes into chunks.

Let $P$ be a program of the light language whose procedures $p_{\mathrm{classes}}$ and $p_{\mathrm{chunks}}$ are the bodies of classes and chunks. Let $x$ be an Exact Triangle instance with $n$ vertices per part and weight bound $U$, and $X$ the data of the host's run (the prime $p$, the capacity $\mathit{cap}\ge1$ of a chunk, the residues of the weights), and assume the host is ready at depth $d$ in memory $\mu$ with free pointer $f$: the three $n\times n$ weight matrices are stored below $f$ with entries of absolute value at most $U$, $1\le p$, $p\cdot2^{\mathrm{bitLen}(U)+1}$ and every address fit in a word, the arrays of the host fit in memory and $d+2\le\mathrm{depth}$. Let $\mu_1$ be a memory holding the residues $r_{AB}$ of the first matrix modulo $p$ at their array.

Suppose a statement $t$ satisfies: for every result $r'$ and every memory $\mu'$ that holds the pairs sorted class by class and the table of chunks (their residues, starts and lengths) and agrees with $\mu_1$ outside the area between the class array and the first instance matrix, $t$ run from the host's local frame (with the number of chunks set) ends within $T-(t_{\mathrm{classes}}(n,p)+t_{\mathrm{chunks}}(p,k)+17)$ steps with postcondition $Q$, where $k$ is the number of chunks. If moreover $t_{\mathrm{classes}}(n,p)+t_{\mathrm{chunks}}(p,k)+17\le T$, then the sequence

run from the host's local frame in memory $\mu_1$ ends within $T$ steps with postcondition $Q$.

The lemma lets the proofs of the host compose the classes-and-chunks phase with whatever follows it, here the loop over the instances of the all-edges host at the middle dimension.

Formalization Note This is the lemma Light.Sec3.Et17.classes_then of the unmodified library; it is a platform node because the all-edges host at the middle dimension reuses it. The local variable names (ResAB, Size, ThePrime, Cls, …) are the slots of the host's frame Et17.locals.