The program runs the glue program $ShiftRam.glue$ and the restriction program of the restriction lemma in the loop driver $loop_sound$. In its first round the glue program reads the tree, finds the first extension with guard $0$, which exists since $dist(a₁, a₁) = 0$, and asks for the restriction of its child to the first $ℓ$ positions. In its second round it outputs the answer. The child is tree_{k+1,q−1}(ā b) for a vertex $b$, so the answer is tree_{k+1,q−1}(ā), as in the proof of the rank shift 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, the run of the restriction program because its query is admissible at the word length of its region. The constant absorbs the constant of the restriction program at rank $(k + 1, q)$, and the degree is that of the restriction program plus two.

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