An algorithm for the solution of tree equations

We consider the problem of solving equations over k-ary trees. Here an equation is a pair of labeled α-ary trees, where α is a function associating an arity to each label. A solution to an equation is a morphism from α-ary trees to k-ary trees that maps the left and right hand side of the equation to the same k-ary tree.