YES TRS: +(x,0()) -> x +(minus(x),x) -> 0() minus(0()) -> 0() minus(minus(x)) -> x minus(+(x,y)) -> +(minus(y),minus(x)) *(x,1()) -> x *(x,0()) -> 0() *(x,+(y,z)) -> +(*(x,y),*(x,z)) *(x,minus(y)) -> minus(*(x,y)) max/plus interpretations on N: +_A(x1,x2) = max{3, x1, x2} +#_A(x1,x2) = max{0, -2, -1} 0_A = 4 0#_A = 3 minus_A(x1) = max{4, x1} minus#_A(x1) = max{4, 1} *_A(x1,x2) = max{4, 1 + x1, 2} *#_A(x1,x2) = max{2, 4, 4} 1_A = 0 1#_A = 0 precedence: * > minus > 0 > + = 1