The program is one pass over the tree followed by restoring canonical form, as in the proof of the restriction lemma. The pass reads the tree and $J$, the latter into a table of the places of the positions, lists the nodes of the tree in breadth-first order, and writes for every node, from the last to the first, its transformed atoms and its transformed extensions. An atom is transformed by renaming its positions along $J$, and dropped if a position lies outside $J$. An extension is transformed by renaming its guard in the same way, and dropped if the guard lies outside $J$, and its child is referred to by the indices of the jobs of the child. Positions beyond the arity $ℓ$, the new positions of the nodes below the root, are moved down by $ℓ - |J|$. Nothing is sorted in the pass. The canonical form is then restored from the leaves up by the program of the canonical form observation, called once for every set of the result ($TreeCanon.treeCanon$). The result is the semantic core $restrictNode$ along the partial inverse of $J$, whose correctness is $restrictTree_tree$. The sets of the result are no larger than those of the input, so the time is polynomial in the length of the input.

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