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{3, x1, x2} +#_A(x1,x2) = max{3, x1, x2} 0_A = 5 0#_A = 5 s_A(x1) = max{1, x1} s#_A(x1) = max{1, x1} *_A(x1,x2) = max{3, 1 + x1, x2} *#_A(x1,x2) = max{3, 1 + x1, x2} sum_A(x1) = max{6, 2 + x1} sum#_A(x1) = max{6, 2 + x1} nil_A = 5 nil#_A = 5 cons_A(x1,x2) = max{7, 5 + x1, 5 + x2} cons#_A(x1,x2) = max{7, 5 + x1, 5 + x2} prod_A(x1) = max{4, x1} prod#_A(x1) = max{4, x1} precedence: cons > * = sum = nil > + > s > prod > 0