We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , 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)) , s(X) -> n__s(X) , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , head(cons(N, XS)) -> N , tail(cons(N, XS)) -> activate(XS) , sel(N, XS) -> head(afterNth(N, XS)) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Arguments of following rules are not normal-forms: { splitAt(s(N), cons(X, XS)) -> u(splitAt(N, activate(XS)), N, X, activate(XS)) } All above mentioned rules can be savely removed. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , fst(pair(XS, YS)) -> XS , snd(pair(XS, YS)) -> YS , splitAt(0(), XS) -> pair(nil(), XS) , s(X) -> n__s(X) , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , head(cons(N, XS)) -> N , tail(cons(N, XS)) -> activate(XS) , sel(N, XS) -> head(afterNth(N, XS)) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. Trs: { natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , fst(pair(XS, YS)) -> XS , snd(pair(XS, YS)) -> YS , splitAt(0(), XS) -> pair(nil(), XS) , s(X) -> n__s(X) , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , head(cons(N, XS)) -> N , tail(cons(N, XS)) -> activate(XS) , sel(N, XS) -> head(afterNth(N, XS)) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(natsFrom) = {1}, safe(cons) = {1, 2}, safe(n__natsFrom) = {1}, safe(n__s) = {1}, safe(fst) = {1}, safe(pair) = {1, 2}, safe(snd) = {1}, safe(splitAt) = {1, 2}, safe(0) = {}, safe(nil) = {}, safe(s) = {1}, safe(u) = {1}, safe(activate) = {}, safe(head) = {1}, safe(tail) = {}, safe(sel) = {}, safe(afterNth) = {1, 2}, safe(take) = {} and precedence u > activate, activate > natsFrom, activate > s, tail > activate, sel > head, sel > afterNth, afterNth > snd, afterNth > splitAt, take > fst, take > splitAt . Following symbols are considered recursive: {activate} The recursion depth is 1. For your convenience, here are the satisfied ordering constraints: natsFrom(; N) > cons(; N, n__natsFrom(; n__s(; N))) natsFrom(; X) > n__natsFrom(; X) fst(; pair(; XS, YS)) > XS snd(; pair(; XS, YS)) > YS splitAt(; 0(), XS) > pair(; nil(), XS) s(; X) > n__s(; X) u(N, X, XS; pair(; YS, ZS)) > pair(; cons(; activate(X;), YS), ZS) activate(X;) > X activate(n__natsFrom(; X);) > natsFrom(; activate(X;)) activate(n__s(; X);) > s(; activate(X;)) head(; cons(; N, XS)) > N tail(cons(; N, XS);) > activate(XS;) sel(N, XS;) > head(; afterNth(; N, XS)) afterNth(; N, XS) > snd(; splitAt(; N, XS)) take(N, XS;) > fst(; splitAt(; N, XS)) We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , fst(pair(XS, YS)) -> XS , snd(pair(XS, YS)) -> YS , splitAt(0(), XS) -> pair(nil(), XS) , s(X) -> n__s(X) , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , head(cons(N, XS)) -> N , tail(cons(N, XS)) -> activate(XS) , sel(N, XS) -> head(afterNth(N, XS)) , afterNth(N, XS) -> snd(splitAt(N, XS)) , take(N, XS) -> fst(splitAt(N, XS)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))