Input TRS: 1: first(0(),X) -> nil() 2: first(s(X),cons(Y)) -> cons(Y) 3: from(X) -> cons(X) Number of Rules: 3 Direct QWPOS(Sum) ... orients all. I(0) = 1 I(from) = x1 + 1 sigma(from) = [1] I(nil) = 0 I(s) = x1 sigma(s) = [1] I(cons) = x1 sigma(cons) = [1] I(first) = x1 + x2 sigma(first) = [1,2] PREC: 0 > from = nil = s > cons = first Number of Rules: 0