The batched band-array procedure fills the left input array of a band

In every program $P$ whose procedure number pBandArray is bandArrayBBody, under the standard limits (Std lim), the procedure meets BandArrayBLSpec lim P cBandArray: for parameters $p$ of Theorem 30 (with $m\le L$), a source matrix $X\in\mathbb Z^{K_0N\times D}$ stored at aX, a band $\beta<n_B$, the digit tables of the band (BandTables) and enough space, the call with the arguments of bandArray (Section 2.3.4) returns within the cost bound with constant cBandArray and writes at arr the left input array of the band $\beta$ in the batched layout, keeping the rest of the memory.

The batched layout (Batch/Tiling): the source of the left side is a $K_0N\times D$ matrix $X$ (row by row), that of the right side a $D\times K_0N$ matrix $Y$ (stored transposed); the slot $(g,h)$ of the band $\beta$ holds the row block number $(\beta K_0+g)K_0+h$ of the source, so one run of Theorem 30's data structure computes $K_0^2$ independent block products.

Meets lim P p d args μ T Q means: the call of procedure $p$ of $P$ at depth $d$ with the arguments args on memory $\mu$ returns within $T$ steps, under the limits lim, with a result $r$ and memory $\mu'$ satisfying $Q\,r\,\mu'$.