The program runs the glue program $FarRam.glue$ and the restriction program of the restriction lemma in the loop driver $loop_sound$. Round $j$ of the glue program reads the tree, the scatter type and the answers so far, and asks for the restriction $μ ↾ (ℓ+1)$ of the child of extension $j$ to its last position, one call per extension. The last round reads the radius and the blocks off the root, the met and far bits off the roots of the children, scans the scatter type and writes the selected trees, as in the proof of the far tree lemma. Its output is the far tree by $farTree_tree$, which applies the clustering lemma. Every run inside the driver is right at an admissible word length: the runs of the glue program because their values are polynomial in the input with a factor depending on the rank, the runs of the restriction program because their queries are admissible at the word lengths of their regions.

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