YES TRS: f(s(X),Y) -> h(s(f(h(Y),X))) max/plus interpretations on N: f_A(x1,x2) = max{1, -9 + x1, -1 + x2} f#_A(x1,x2) = max{0, -12 + x1, -4 + x2} s_A(x1) = max{15, 14 + x1} s#_A(x1) = max{3, -2 + x1} h_A(x1) = max{6, -9 + x1} h#_A(x1) = max{1, 3} precedence: f > s = h