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 QKBOS(Sum) ... orients all. I(mark) = x1 + 3 sigma(mark) = [1] I(0) = 1 I(a__tail) = x1 + 4 sigma(a__tail) = [1] I(a__zeros) = 3 I(zeros) = 1 I(cons) = x1 + x2 sigma(cons) = [2,1] I(tail) = x1 + 4 sigma(tail) = [1] PREC: mark > a__tail > tail > 0 = a__zeros > zeros = cons Number of Rules: 0