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)) f_6(x) -> g_6(x,x) g_6(s(x),y) -> b(f_5(y),g_6(x,y)) f_7(x) -> g_7(x,x) g_7(s(x),y) -> b(f_6(y),g_7(x,y)) f_8(x) -> g_8(x,x) g_8(s(x),y) -> b(f_7(y),g_8(x,y)) f_9(x) -> g_9(x,x) g_9(s(x),y) -> b(f_8(y),g_9(x,y)) f_10(x) -> g_10(x,x) g_10(s(x),y) -> b(f_9(y),g_10(x,y)) linear polynomial interpretations on N: f_0_A(x1) = 1 f_0#_A(x1) = 1 a_A = 0 a#_A = 0 f_1_A(x1) = 1 f_1#_A(x1) = 3 g_1_A(x1,x2) = 1 g_1#_A(x1,x2) = 2 s_A(x1) = x1 + 1 s#_A(x1) = 0 b_A(x1,x2) = x1 b#_A(x1,x2) = x2 f_2_A(x1) = 1 f_2#_A(x1) = 5 g_2_A(x1,x2) = 1 g_2#_A(x1,x2) = 4 f_3_A(x1) = 1 f_3#_A(x1) = 7 g_3_A(x1,x2) = 1 g_3#_A(x1,x2) = 6 f_4_A(x1) = 1 f_4#_A(x1) = x1 + 8 g_4_A(x1,x2) = 1 g_4#_A(x1,x2) = x1 + 7 f_5_A(x1) = 1 f_5#_A(x1) = x1 + 10 g_5_A(x1,x2) = 1 g_5#_A(x1,x2) = x2 + 9 f_6_A(x1) = x1 + 1 f_6#_A(x1) = x1 + 12 g_6_A(x1,x2) = x2 + 1 g_6#_A(x1,x2) = x2 + 11 f_7_A(x1) = x1 + 1 f_7#_A(x1) = x1 + 14 g_7_A(x1,x2) = x2 + 1 g_7#_A(x1,x2) = x2 + 13 f_8_A(x1) = x1 + 1 f_8#_A(x1) = x1 + 16 g_8_A(x1,x2) = x2 + 1 g_8#_A(x1,x2) = x2 + 15 f_9_A(x1) = x1 + 1 f_9#_A(x1) = x1 + 18 g_9_A(x1,x2) = x2 + 1 g_9#_A(x1,x2) = x2 + 17 f_10_A(x1) = x1 + 1 f_10#_A(x1) = x1 + 20 g_10_A(x1,x2) = x2 + 1 g_10#_A(x1,x2) = x2 + 19 precedence: f_10 = g_10 > f_9 > g_9 > f_8 > s = g_8 > f_7 > g_7 > f_6 > g_6 > f_5 > g_5 > f_4 > g_4 > f_3 > g_3 > f_2 > g_2 > f_1 > g_1 > f_0 = b > a