YES TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) 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{41, x1, 13 + x2} +#_A(x1,x2) = max{35, 36, 36} 0_A = 29 0#_A = 32 s_A(x1) = max{1, x1} s#_A(x1) = max{36, 36} *_A(x1,x2) = max{54, 28 + x1, 26 + x2} *#_A(x1,x2) = max{34, 37, 40 + x2} sum_A(x1) = max{28, 1 + x1} sum#_A(x1) = max{37, 38} nil_A = 30 nil#_A = 37 cons_A(x1,x2) = max{55, 37 + x1, 39 + x2} cons#_A(x1,x2) = max{0, 0, 0} prod_A(x1) = max{13, -1 + x1} prod#_A(x1) = max{33, 1 + x1} precedence: cons > prod > * = sum = nil > + = 0 > s