YES TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) max/plus interpretations on N: +_A(x1,x2) = max{0, x1, x2} +#_A(x1,x2) = max{0, x1, x2} 0_A = 0 0#_A = 0 s_A(x1) = max{0, x1} s#_A(x1) = max{0, x1} *_A(x1,x2) = max{0, x1, x2} *#_A(x1,x2) = max{0, x1, x2} sum_A(x1) = max{0, x1} sum#_A(x1) = max{0, x1} nil_A = 0 nil#_A = 0 cons_A(x1,x2) = max{0, x1, x2} cons#_A(x1,x2) = max{0, x1, x2} prod_A(x1) = max{0, x1} prod#_A(x1) = max{0, x1} precedence: nil > 0 = cons > prod > * = sum > + > s