YES TRS: times(x,0()) -> 0() times(x,s(y)) -> plus(times(x,y),x) plus(x,0()) -> x plus(0(),x) -> x plus(x,s(y)) -> s(plus(x,y)) plus(s(x),y) -> s(plus(x,y)) max/plus interpretations on N: times_A(x1,x2) = max{2, 1 + x1, 1 + x2} times#_A(x1,x2) = max{2, 1 + x1, 1 + x2} 0_A = 0 0#_A = 0 s_A(x1) = max{0, x1} s#_A(x1) = max{0, x1} plus_A(x1,x2) = max{2, x1, x2} plus#_A(x1,x2) = max{2, x1, x2} precedence: 0 > times > plus > s