The program is one pass over the tree followed by restoring canonical form, as in the proof of the merge lift lemma. The pass reads the tree and the colors $P$ and $Q$, 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 extensions. An atom is transformed by replacing the color $Q$ by $P$ in every atom $Y(x)$ and $dist(x, Y) < r$. The guards are kept, and the child of an extension is referred to by the indices of the jobs of the child. 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$), which merges atoms that become equal. This is the semantic core $mergeNode$, whose correctness is $mergeNode_node$. No tree grows, 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$.