Input TRS: 1: a__zeros() -> cons(0(),zeros()) 2: a__tail(cons(X,XS)) -> mark(XS) 3: mark(zeros()) -> a__zeros() 4: mark(tail(X)) -> a__tail(mark(X)) 5: mark(cons(X1,X2)) -> cons(mark(X1),X2) 6: mark(0()) -> 0() 7: a__zeros() -> zeros() 8: a__tail(X) -> tail(X) Number of Rules: 8 Direct POLO(Sum) ... removes: 7 6 3 2 1 I(mark) = x1 + 2 I(0) = 0 I(a__tail) = x1 + 3 I(a__zeros) = 1 I(zeros) = 0 I(cons) = x1 + x2 I(tail) = x1 + 3 Number of Rules: 3 Direct POLO(Sum) ...Direct QLPOS ... removes: 8 5 4 sigma(mark) = [1] sigma(a__tail) = [1] sigma(cons) = [2,1] sigma(tail) = [1] PREC: mark > a__tail > cons = tail Number of Rules: 0