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{20, -2 + x1} from#_A(x1) = max{23, 7 + x1} cons_A(x1,x2) = max{0, -9 + x1, x2} cons#_A(x1,x2) = max{23, 23, 3 + x2} n__from_A(x1) = max{20, -2 + x1} n__from#_A(x1) = max{8, 7 + x1} s_A(x1) = max{1, -1 + x1} s#_A(x1) = max{8, 7 + x1} head_A(x1) = max{9, 9 + x1} head#_A(x1) = max{33, 22} 2nd_A(x1) = max{8, 9 + x1} 2nd#_A(x1) = max{34, 32 + x1} activate_A(x1) = max{0, x1} activate#_A(x1) = max{2, 10 + x1} take_A(x1,x2) = max{16, 0, 17 + x2} take#_A(x1,x2) = max{22, 24, 20 + x2} 0_A = 1 0#_A = 24 nil_A = 17 nil#_A = 23 n__take_A(x1,x2) = max{15, -1, 17 + x2} n__take#_A(x1,x2) = max{0, 21, 21} sel_A(x1,x2) = max{0, 0, 9 + x2} sel#_A(x1,x2) = max{0, 10, 10 + x2} precedence: 2nd = take = sel > activate > from = 0 > cons = n__from = s = nil = n__take > head