Hi, have you ever tried assigning a total order to your syntax tree? Very much like problems occurring in Buchberger's algorithm and its generalized form Knuth-Bendix completion; they have a very sophisticated way of recursively assigning weights to each term (which there can be infinitely many).