The program is the loop driver of the glue program of the resolve lift with the switch of its five callees: the rank shift (the rank shift lemma), the far tree (the far tree lemma), the far composition (the far composition lemma), the canonical form (the canonical form observation) and the scatter type (the lemma on computing scatter types). The glue program first computes the scatter type of the input, then walks down the levels of the items, asking for the shift, the far tree and the compositions of each item, and walks up again, asking for the canonical forms of the atoms and of the children of each item. Its last round builds the resolved graph and its distance matrix, by the formula for distances after a resolve, and writes the output. Every round runs within a constant times $(n + 1) Y^a$ steps, with $Y = M + T + 1$, except the first two and the last round, which read the input or write the output and run within a constant times $(n + 1)² Y^a$ steps. With at most a constant times $(n + 1)(T + 1)^(q + 1)$ rounds, the total time of the glue program is within the bound. The sizes of the output trees are those of the type trees of the resolved graph.

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