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{2, -5, 4} +#_A(x1,x2) = max{3, 9, 13} a_A = 5 a#_A = 1 b_A = 6 b#_A = 0 f_A(x1,x2) = max{4, 1 + x1, 1} f#_A(x1,x2) = max{8, 13, 2} precedence: f > + = a > b