Let $q'$ be the rank of $LocalToGlobal$ for $q$-tuples, rank $q$ and arity 2, and let $a$ and $F$ be the exponent and factor of $TypeBound$ for $q$-tuples and rank $q' + q₀$. Fix a step $t$ and a vertex $v$, and let $B$ and $W$ be the balls of radius $r$ and $r + 7^q$ around $v$ in the next partial graph. A step keeps resolved pairs, so the radius-$7^q$ ball in the current partial graph of a tuple from $B$ lies in $W$. By $LocalToGlobal$, the type of such a tuple is determined by its type of rank $q'$ in the induced partial graph on $W$. This partial graph is definable in an expansion of the graph by $c$ predicates with at most $s$ parameters, so the type over the parameters of rank $q' + q₀$ determines the latter. $TypeBound$ bounds the number of these types by $F · (s + 1)^a$.

The argument is carried out for the graph classes of the archive and their monadic dependence, and transferred to the graph classes used here.