YES TRS: from(X) -> cons(X,n__from(s(X))) head(cons(X,XS)) -> X 2nd(cons(X,XS)) -> head(activate(XS)) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) from(X) -> n__from(X) take(X1,X2) -> n__take(X1,X2) activate(n__from(X)) -> from(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(X) -> X linear polynomial interpretations on N: from_A(x1) = x1 + 2 from#_A(x1) = x1 + 1 cons_A(x1,x2) = x1 + x2 + 1 cons#_A(x1,x2) = 0 n__from_A(x1) = x1 + 1 n__from#_A(x1) = 0 s_A(x1) = 0 s#_A(x1) = x1 head_A(x1) = x1 head#_A(x1) = 1 2nd_A(x1) = x1 2nd#_A(x1) = x1 + 1 activate_A(x1) = x1 + 1 activate#_A(x1) = x1 + 1 take_A(x1,x2) = x2 + 2 take#_A(x1,x2) = x2 + 1 0_A = 0 0#_A = 1 nil_A = 0 nil#_A = 0 n__take_A(x1,x2) = x2 + 1 n__take#_A(x1,x2) = 0 sel_A(x1,x2) = x2 sel#_A(x1,x2) = x2 + 1 precedence: n__take > 2nd = take > activate = sel > from = 0 > cons = n__from = s = nil > head