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(Sum) ... orients all. I(0) = 1 I(len) = x1 + 2 sigma(len) = [1] I(from) = x1 + 1 sigma(from) = [1] I(nil) = 2 I(s) = 2 I(add) = x1 + x2 sigma(add) = [1,2] I(cons) = x1 sigma(cons) = [1] I(fst) = x1 + x2 + 1 sigma(fst) = [1,2] PREC: from = s = add > cons > nil = fst > 0 > len Number of Rules: 0