The proof of the few-types theorem. Run the algorithm of the theorem on definable construction sequences with radius $r + 7^q$, where $h = 7^q$ is the radius of the lemma passing from definability to few types. The output is radius-$(r + 7^q)$ definable with $⌈A(r + 7^q)/ε⌉ + A$ predicates and $s ≤ c₀ (n+1)^(a₀ε)$ parameters, so its radius-$r$ depth-$q$ width is at most $F (s+1)^D$, which is $O((n+1)^(a₀Dε))$. So $a = a₀D + a₀$ works for the width and the length, and $a ≥ 1$ since $a₀ ≥ 1$. The exponent $3 + η$ of the time is passed on to the theorem on definable construction sequences. The program is a simulation of the program of the theorem on definable construction sequences on the rewritten input, one word bit shorter, and the word-length exponent grows by one to pay for the larger first entry.

The proof is carried out for the input format with the graph in compressed sparse row form and the notion $Lax185574.Computing.Computes$. The algorithm converts the word of the graph into compressed sparse rows ($Interface.nbr_bridge$) and runs the program for that format. The script of a graph is the one whose encoding the program outputs on the converted input.