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