(VAR U V W X Y Z ) (RULES concat(leaf, Y) -> Y concat(cons(U, V), Y) -> cons(U, concat(V, Y)) lessleaves(X, leaf) -> false lessleaves(leaf, cons(W, Z)) -> true lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z)) )