YES TRS: i(0()) -> 0() +(0(),y) -> y +(x,0()) -> x i(i(x)) -> x +(i(x),x) -> 0() +(x,i(x)) -> 0() i(+(x,y)) -> +(i(x),i(y)) +(x,+(y,z)) -> +(+(x,y),z) +(+(x,i(y)),y) -> x +(+(x,y),i(y)) -> x max/plus interpretations on N: i_A(x1) = max{1, 3 + x1} i#_A(x1) = max{5, 1 + x1} 0_A = 4 0#_A = 6 +_A(x1,x2) = max{8, x1, 11 + x2} +#_A(x1,x2) = max{0, 4, 7 + x2} precedence: i > + > 0