YES TRS: +(x,+(y,z)) -> +(+(x,y),z) +(*(x,y),+(x,z)) -> *(x,+(y,z)) +(*(x,y),+(*(x,z),u)) -> +(*(x,+(y,z)),u) linear polynomial interpretations on N: +_A(x1,x2) = x1 + x2 + 1 +#_A(x1,x2) = x2 *_A(x1,x2) = x1 + x2 + 1 *#_A(x1,x2) = 0 precedence: + > *