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