Input TRS: 1: fst(0(),Z) -> nil() 2: fst(s(),cons(Y)) -> cons(Y) 3: from(X) -> cons(X) 4: add(0(),X) -> X 5: add(s(),Y) -> s() 6: len(nil()) -> 0() 7: len(cons(X)) -> s() Number of Rules: 7 Direct QWPOS(Pol) ... orients all. I(0) = 3 I(len) = 3 * x1 sigma(len) = [1] I(from) = 3 * x1 + 3 sigma(from) = [1] I(nil) = 3 I(s) = 2 I(add) = 3 * x1 + 2 * x2 + 2 sigma(add) = [1,2] I(cons) = x1 + 3 sigma(cons) = [1] I(fst) = 2 * x1 + 3 * x2 + 2 sigma(fst) = [1,2] PREC: len = nil > 0 > from > cons > s = add = fst Number of Rules: 0