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