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{0, x1} natsFrom#_A(x1) = max{0, x1} cons_A(x1,x2) = max{0, x1, x2} cons#_A(x1,x2) = max{0, x1, x2} n__natsFrom_A(x1) = max{0, x1} n__natsFrom#_A(x1) = max{0, x1} n__s_A(x1) = max{0, x1} n__s#_A(x1) = max{0, x1} fst_A(x1) = max{0, x1} fst#_A(x1) = max{0, x1} pair_A(x1,x2) = max{0, x1, x2} pair#_A(x1,x2) = max{0, x1, x2} snd_A(x1) = max{0, x1} snd#_A(x1) = max{0, x1} splitAt_A(x1,x2) = max{0, x1, x2} splitAt#_A(x1,x2) = max{0, x1, x2} 0_A = 0 0#_A = 0 nil_A = 0 nil#_A = 0 s_A(x1) = max{0, x1} s#_A(x1) = max{0, x1} u_A(x1,x2,x3,x4) = max{0, x1, x2, x3, x4} u#_A(x1,x2,x3,x4) = max{0, x1, x2, x3, x4} activate_A(x1) = max{0, x1} activate#_A(x1) = max{0, x1} head_A(x1) = max{0, x1} head#_A(x1) = max{0, x1} tail_A(x1) = max{0, x1} tail#_A(x1) = max{0, x1} sel_A(x1,x2) = max{0, x1, x2} sel#_A(x1,x2) = max{0, x1, x2} afterNth_A(x1,x2) = max{0, x1, x2} afterNth#_A(x1,x2) = max{0, x1, x2} take_A(x1,x2) = max{0, x1, x2} take#_A(x1,x2) = max{0, x1, x2} precedence: sel > 0 = nil = head = afterNth = take > fst = snd = splitAt > u = tail > pair = activate > natsFrom = s > cons = n__natsFrom = n__s