YES TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) f(0()) -> s(0()) f(s(x)) -> minus(s(x),g(f(x))) g(0()) -> 0() g(s(x)) -> minus(s(x),f(g(x))) max/plus interpretations on N: minus_A(x1,x2) = max{24, x1, 24} minus#_A(x1,x2) = max{22, 23, 10} 0_A = 1 0#_A = 0 s_A(x1) = max{19, 13 + x1} s#_A(x1) = max{9, 21 + x1} f_A(x1) = max{19, 10 + x1} f#_A(x1) = max{24, 7 + x1} g_A(x1) = max{17, 5 + x1} g#_A(x1) = max{25, x1} precedence: f > g > minus = 0 = s