MAYBE MAYBE TRS: { natsFrom(N) -> cons(N), fst(pair(XS, YS)) -> XS, snd(pair(XS, YS)) -> YS, splitAt(0(), XS) -> pair(nil(), XS), splitAt(s(N), cons(X)) -> u(splitAt(N, XS)), u(pair(YS, ZS)) -> pair(cons(X), ZS), head(cons(N)) -> N, tail(cons(N)) -> XS, afterNth(N, XS) -> snd(splitAt(N, XS)), sel(N, XS) -> head(afterNth(N, XS)), take(N, XS) -> fst(splitAt(N, XS)) } DUP: We consider a duplicating system. Trs: { natsFrom(N) -> cons(N), fst(pair(XS, YS)) -> XS, snd(pair(XS, YS)) -> YS, splitAt(0(), XS) -> pair(nil(), XS), splitAt(s(N), cons(X)) -> u(splitAt(N, XS)), u(pair(YS, ZS)) -> pair(cons(X), ZS), head(cons(N)) -> N, tail(cons(N)) -> XS, afterNth(N, XS) -> snd(splitAt(N, XS)), sel(N, XS) -> head(afterNth(N, XS)), take(N, XS) -> fst(splitAt(N, XS)) } Fail