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{5, 1 + x1, 2 + x2} *#_A(x1,x2) = max{0, -5, -6} +_A(x1,x2) = max{4, 3, 5} +#_A(x1,x2) = max{0, -7, 0} 1_A = 0 1#_A = 0 precedence: * > + = 1