The proof of the theorem on definable construction sequences. Compute a chain at radius $5r + 1$ and accuracy $ε$ (the chain theorem), of length $m ≤ O(r/ε)$, and turn it into a construction sequence (the lemma turning chains into construction sequences). With $k_r ≤ c (n+1)^ε$ the radius-$(5r+1)$ width of the chain, $d$ a bound on the VC-dimension of the graphs of the class (the observation on bounded VC-dimension) and $π_G(k) ≤ (k+1)^d$ (the Sauer–Shelah lemma), $w_r ≤ (k_r + 1)^(d+1)$, so $a₀ = d + 1$. The length is $O(n w₁) ≤ O(n w_r)$, as the width of a chain grows with the radius. The number of predicates is $2m + 1 ≤ ⌈A r/ε⌉ + A$. On the word RAM, a first phase converts the compressed sparse row form of the graph into the word of the graph that the two cited programs read.

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 that program. The script of a graph is the one whose encoding the program outputs on the converted input.