YES TRS: f_0(x) -> a() f_1(x) -> g_1(x,x) g_1(s(x),y) -> b(f_0(y),g_1(x,y)) f_2(x) -> g_2(x,x) g_2(s(x),y) -> b(f_1(y),g_2(x,y)) f_3(x) -> g_3(x,x) g_3(s(x),y) -> b(f_2(y),g_3(x,y)) f_4(x) -> g_4(x,x) g_4(s(x),y) -> b(f_3(y),g_4(x,y)) f_5(x) -> g_5(x,x) g_5(s(x),y) -> b(f_4(y),g_5(x,y)) max/plus interpretations on N: f_0_A(x1) = max{0, x1} f_0#_A(x1) = max{0, x1} a_A = 0 a#_A = 0 f_1_A(x1) = max{0, x1} f_1#_A(x1) = max{0, x1} g_1_A(x1,x2) = max{0, x1, x2} g_1#_A(x1,x2) = max{0, x1, x2} s_A(x1) = max{0, x1} s#_A(x1) = max{0, x1} b_A(x1,x2) = max{0, x1, x2} b#_A(x1,x2) = max{0, x1, x2} f_2_A(x1) = max{0, x1} f_2#_A(x1) = max{0, x1} g_2_A(x1,x2) = max{0, x1, x2} g_2#_A(x1,x2) = max{0, x1, x2} f_3_A(x1) = max{0, x1} f_3#_A(x1) = max{0, x1} g_3_A(x1,x2) = max{0, x1, x2} g_3#_A(x1,x2) = max{0, x1, x2} f_4_A(x1) = max{0, x1} f_4#_A(x1) = max{0, x1} g_4_A(x1,x2) = max{0, x1, x2} g_4#_A(x1,x2) = max{0, x1, x2} f_5_A(x1) = max{0, x1} f_5#_A(x1) = max{0, x1} g_5_A(x1,x2) = max{0, x1, x2} g_5#_A(x1,x2) = max{0, x1, x2} precedence: f_5 > g_5 > f_4 > g_4 > f_3 > g_3 > f_2 > g_2 > f_1 > g_1 > f_0 = s = b > a