YES TRS: a__zeros() -> cons(0(),zeros()) a__tail(cons(X,XS)) -> mark(XS) mark(zeros()) -> a__zeros() mark(tail(X)) -> a__tail(mark(X)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(0()) -> 0() a__zeros() -> zeros() a__tail(X) -> tail(X) max/plus interpretations on N: a__zeros_A = 21 a__zeros#_A = 13 cons_A(x1,x2) = max{13, x1, 6 + x2} cons#_A(x1,x2) = max{0, 1, 12} 0_A = 5 0#_A = 3 zeros_A = 15 zeros#_A = 0 a__tail_A(x1) = max{5, 12 + x1} a__tail#_A(x1) = max{1, 4 + x1} mark_A(x1) = max{5, 6 + x1} mark#_A(x1) = max{2, -1 + x1} tail_A(x1) = max{0, 12 + x1} tail#_A(x1) = max{3, 0} precedence: tail > mark > 0 = a__tail > a__zeros > cons = zeros