The program runs the glue program $StpRam.glue$ and the program of the rank shift lemma in the loop driver $loop_sound$, as in the proof of the lemma on computing scatter types. The first round reads the graph, $k$ and $q$, skips the distance matrix $D_G$ and reads the family of type trees. For $q = 0$ it outputs the empty scatter type. Otherwise the rounds ask for the shifts of the entries of the list of the family trees followed by the answers, one by one, so that the answers are the trees $tree_{k+i,q−i}(v)$ for $1 ≤ i ≤ q$ and all vertices $v$, in this order. After a dummy call the final round reads the graph, $D_G$ and the answers and computes the scatter type ($StpRam.finalRound_run$). Its greedy scans test whether a vertex is within distance $r$ of a chosen vertex by one entry of the row of $D_G$ of the chosen vertex, in place of a breadth-first search. The script has $q · n + 1$ calls. Every run inside the driver is right at an admissible word length: the runs of the glue program because their values are below a constant in $k, q$ times the cube of $|x| + max x + 1$, the runs of the rank shift because their queries are admissible at the word lengths of their regions. The time is that of the first round, $O_{k,q}(n² + n · L)$, and of the final round, $O_{k,q}(n² · (L + 1))$, plus $q · n$ middle rounds of time $O_{k,q}(n · L)$ and $q · n + 1$ calls of time $O_{k,q}((L + 1)^a)$.

The proof is carried out for the notion $Lax185574.Computing.Computes$, and transferred to $Lax185574.Algorithms.Algorithm.Computes$ through $Lax185574Proofs.Interface$.