YES TRS: natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) fst(pair(XS,YS)) -> XS snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) splitAt(s(N),cons(X,XS)) -> u(splitAt(N,activate(XS)),N,X,activate(XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) head(cons(N,XS)) -> N tail(cons(N,XS)) -> activate(XS) sel(N,XS) -> head(afterNth(N,XS)) take(N,XS) -> fst(splitAt(N,XS)) afterNth(N,XS) -> snd(splitAt(N,XS)) natsFrom(X) -> n__natsFrom(X) s(X) -> n__s(X) activate(n__natsFrom(X)) -> natsFrom(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X max/plus interpretations on N: natsFrom_A(x1) = max{13, 7 + x1} natsFrom#_A(x1) = max{13, 7 + x1} cons_A(x1,x2) = max{6, x1, x2} cons#_A(x1,x2) = max{6, x1, x2} n__natsFrom_A(x1) = max{13, 7 + x1} n__natsFrom#_A(x1) = max{13, 7 + x1} n__s_A(x1) = max{5, x1} n__s#_A(x1) = max{5, x1} fst_A(x1) = max{25, 1 + x1} fst#_A(x1) = max{25, 1 + x1} pair_A(x1,x2) = max{13, 7 + x1, 5 + x2} pair#_A(x1,x2) = max{13, 7 + x1, 5 + x2} snd_A(x1) = max{25, 1 + x1} snd#_A(x1) = max{25, 1 + x1} splitAt_A(x1,x2) = max{24, 19 + x1, 20 + x2} splitAt#_A(x1,x2) = max{24, 19 + x1, 20 + x2} 0_A = 26 0#_A = 26 nil_A = 25 nil#_A = 25 s_A(x1) = max{6, x1} s#_A(x1) = max{6, x1} u_A(x1,x2,x3,x4) = max{5, x1, 7 + x2, 12 + x3, 12 + x4} u#_A(x1,x2,x3,x4) = max{5, x1, 7 + x2, 12 + x3, 12 + x4} activate_A(x1) = max{6, x1} activate#_A(x1) = max{6, x1} head_A(x1) = max{26, 1 + x1} head#_A(x1) = max{26, 1 + x1} tail_A(x1) = max{7, 7 + x1} tail#_A(x1) = max{7, 7 + x1} sel_A(x1,x2) = max{24, 26 + x1, 24 + x2} sel#_A(x1,x2) = max{24, 26 + x1, 24 + x2} afterNth_A(x1,x2) = max{25, 23 + x1, 22 + x2} afterNth#_A(x1,x2) = max{25, 23 + x1, 22 + x2} take_A(x1,x2) = max{25, 21 + x1, 22 + x2} take#_A(x1,x2) = max{25, 21 + x1, 22 + x2} precedence: sel > head = afterNth = take > fst = snd = splitAt = 0 > nil = u = tail > pair = activate > s > n__s > natsFrom > cons = n__natsFrom