The program runs a glue program and the three programs of the restriction lemma, the rank shift lemma and the canonical form observation in the loop driver. The glue program runs the recursion of the far composition with an explicit stack of frames: each round reads the stack and the answer to its last question, does one step of the recursion and asks the next question, a rank shift, a restriction or a canonical form, or writes the type tree of the concatenation. Before it halts, every round checks that the question is admissible for the program that answers it, that the round counter is small against the word length of its region, and that its output fits, so every halting run inside the driver is right.

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