YES TRS: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) +(x,+(y,z)) -> +(+(x,y),z) f(g(f(x))) -> f(h(s(0()),x)) f(g(h(x,y))) -> f(h(s(x),y)) f(h(x,h(y,z))) -> f(h(+(x,y),z)) linear polynomial interpretations on N: +_A(x1,x2) = x1 + x2 + 1 +#_A(x1,x2) = x2 + 8 0_A = 1 0#_A = 0 s_A(x1) = x1 + 1 s#_A(x1) = 0 f_A(x1) = x1 + 4 f#_A(x1) = x1 + 1 g_A(x1) = x1 + 3 g#_A(x1) = 8 h_A(x1,x2) = x1 + x2 + 4 h#_A(x1,x2) = 7 precedence: g > h > f > + = 0 > s