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{5, x1, x2} minus#_A(x1,x2) = max{5, x1, x2} 0_A = 5 0#_A = 5 s_A(x1) = max{14, 8 + x1} s#_A(x1) = max{14, 8 + x1} f_A(x1) = max{17, 7 + x1} f#_A(x1) = max{17, 7 + x1} g_A(x1) = max{6, 4 + x1} g#_A(x1) = max{6, 4 + x1} precedence: f > 0 = s > g > minus