YES TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) max/plus interpretations on N: +_A(x1,x2) = max{0, x1, x2} +#_A(x1,x2) = max{0, x1, x2} a_A = 0 a#_A = 0 b_A = 0 b#_A = 0 f_A(x1,x2) = max{0, x1, x2} f#_A(x1,x2) = max{0, x1, x2} precedence: a > b > f > +