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 max/plus interpretations on N: from_A(x1) = max{2, 6 + x1} from#_A(x1) = max{2, 6 + x1} cons_A(x1,x2) = max{6, 5 + x1, 5 + x2} cons#_A(x1,x2) = max{6, 5 + x1, 5 + x2} n__from_A(x1) = max{1, 1 + x1} n__from#_A(x1) = max{1, 1 + x1} s_A(x1) = max{0, x1} s#_A(x1) = max{0, x1} head_A(x1) = max{8, 1 + x1} head#_A(x1) = max{8, 1 + x1} 2nd_A(x1) = max{5, 2 + x1} 2nd#_A(x1) = max{5, 2 + x1} activate_A(x1) = max{3, 5 + x1} activate#_A(x1) = max{3, 5 + x1} take_A(x1,x2) = max{2, 5 + x1, 5 + x2} take#_A(x1,x2) = max{2, 5 + x1, 5 + x2} 0_A = 1 0#_A = 1 nil_A = 0 nil#_A = 0 n__take_A(x1,x2) = max{1, x1, x2} n__take#_A(x1,x2) = max{1, x1, x2} sel_A(x1,x2) = max{7, 5 + x1, 1 + x2} sel#_A(x1,x2) = max{7, 5 + x1, 1 + x2} precedence: 2nd = 0 = sel > n__from = activate = nil > from = take > cons = s = n__take > head