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