YES(?,O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) , splitAt(0(), XS) -> pair(nil(), XS) , U21(tt(), X) -> U22(tt(), activate(X)) , U22(tt(), X) -> activate(X) , U31(tt(), N) -> U32(tt(), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(cons(N, XS)) -> U31(tt(), N) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , U61(tt(), N, X, XS) -> U62(tt(), activate(N), activate(X), activate(XS)) , U62(tt(), N, X, XS) -> U63(tt(), activate(N), activate(X), activate(XS)) , U63(tt(), N, X, XS) -> U64(splitAt(activate(N), activate(XS)), activate(X)) , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U71(tt(), XS) -> U72(tt(), activate(XS)) , U72(tt(), XS) -> activate(XS) , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(pair(X, Y)) -> U21(tt(), X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) We add following dependency tuples: Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(X) -> c_3() , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_9(activate^#(X)) , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_11(activate^#(N)) , U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_17(activate^#(Y)) , U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_23(activate^#(XS)) , U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(X) -> c_3() , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_9(activate^#(X)) , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_11(activate^#(N)) , U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_17(activate^#(Y)) , U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_23(activate^#(XS)) , U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } Weak Trs: { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) , splitAt(0(), XS) -> pair(nil(), XS) , U21(tt(), X) -> U22(tt(), activate(X)) , U22(tt(), X) -> activate(X) , U31(tt(), N) -> U32(tt(), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(cons(N, XS)) -> U31(tt(), N) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , U61(tt(), N, X, XS) -> U62(tt(), activate(N), activate(X), activate(XS)) , U62(tt(), N, X, XS) -> U63(tt(), activate(N), activate(X), activate(XS)) , U63(tt(), N, X, XS) -> U64(splitAt(activate(N), activate(XS)), activate(X)) , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U71(tt(), XS) -> U72(tt(), activate(XS)) , U72(tt(), XS) -> activate(XS) , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(pair(X, Y)) -> U21(tt(), X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) We estimate the number of application of {3,7,8,9} by applications of Pre({3,7,8,9}) = {1,2,4,6,10,11,12,13,14,15,16,17,20,21,22,23,24,25,26,27,30}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 2: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 3: activate^#(X) -> c_3() , 4: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , 5: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , 6: splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , 7: splitAt^#(0(), XS) -> c_7() , 8: natsFrom^#(N) -> c_27() , 9: natsFrom^#(X) -> c_28() , 10: U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , 11: U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 12: U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , 13: U22^#(tt(), X) -> c_9(activate^#(X)) , 14: U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , 15: U32^#(tt(), N) -> c_11(activate^#(N)) , 16: U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 17: U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 18: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , 19: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , 20: U52^#(tt(), Y) -> c_17(activate^#(Y)) , 21: U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 22: U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , 23: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , 24: U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , 25: U72^#(tt(), XS) -> c_23(activate^#(XS)) , 26: U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 27: U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 28: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , 29: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , 30: tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) , 31: take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_9(activate^#(X)) , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_11(activate^#(N)) , U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_17(activate^#(Y)) , U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_23(activate^#(XS)) , U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } Weak DPs: { activate^#(X) -> c_3() , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() } Weak Trs: { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) , splitAt(0(), XS) -> pair(nil(), XS) , U21(tt(), X) -> U22(tt(), activate(X)) , U22(tt(), X) -> activate(X) , U31(tt(), N) -> U32(tt(), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(cons(N, XS)) -> U31(tt(), N) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , U61(tt(), N, X, XS) -> U62(tt(), activate(N), activate(X), activate(XS)) , U62(tt(), N, X, XS) -> U63(tt(), activate(N), activate(X), activate(XS)) , U63(tt(), N, X, XS) -> U64(splitAt(activate(N), activate(XS)), activate(X)) , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U71(tt(), XS) -> U72(tt(), activate(XS)) , U72(tt(), XS) -> activate(XS) , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(pair(X, Y)) -> U21(tt(), X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) We estimate the number of application of {3} by applications of Pre({3}) = {1,2,5,6,7,8,9,10,11,12,13,16,17,18,19,20,21,22,23,26}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 2: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 3: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , 4: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , 5: splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , 6: U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , 7: U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 8: U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , 9: U22^#(tt(), X) -> c_9(activate^#(X)) , 10: U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , 11: U32^#(tt(), N) -> c_11(activate^#(N)) , 12: U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 13: U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 14: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , 15: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , 16: U52^#(tt(), Y) -> c_17(activate^#(Y)) , 17: U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 18: U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , 19: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , 20: U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , 21: U72^#(tt(), XS) -> c_23(activate^#(XS)) , 22: U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 23: U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 24: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , 25: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , 26: tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) , 27: take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) , 28: activate^#(X) -> c_3() , 29: splitAt^#(0(), XS) -> c_7() , 30: natsFrom^#(N) -> c_27() , 31: natsFrom^#(X) -> c_28() } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_9(activate^#(X)) , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_11(activate^#(N)) , U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_17(activate^#(Y)) , U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_23(activate^#(XS)) , U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } Weak DPs: { activate^#(X) -> c_3() , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() } Weak Trs: { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) , splitAt(0(), XS) -> pair(nil(), XS) , U21(tt(), X) -> U22(tt(), activate(X)) , U22(tt(), X) -> activate(X) , U31(tt(), N) -> U32(tt(), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(cons(N, XS)) -> U31(tt(), N) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , U61(tt(), N, X, XS) -> U62(tt(), activate(N), activate(X), activate(XS)) , U62(tt(), N, X, XS) -> U63(tt(), activate(N), activate(X), activate(XS)) , U63(tt(), N, X, XS) -> U64(splitAt(activate(N), activate(XS)), activate(X)) , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U71(tt(), XS) -> U72(tt(), activate(XS)) , U72(tt(), XS) -> activate(XS) , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(pair(X, Y)) -> U21(tt(), X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) We estimate the number of application of {8,10,15,18,20} by applications of Pre({8,10,15,18,20}) = {5,7,9,17,19}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 2: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 3: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , 4: splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , 5: U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , 6: U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 7: U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , 8: U22^#(tt(), X) -> c_9(activate^#(X)) , 9: U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , 10: U32^#(tt(), N) -> c_11(activate^#(N)) , 11: U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 12: U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 13: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , 14: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , 15: U52^#(tt(), Y) -> c_17(activate^#(Y)) , 16: U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 17: U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , 18: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , 19: U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , 20: U72^#(tt(), XS) -> c_23(activate^#(XS)) , 21: U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 22: U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 23: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , 24: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , 25: tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) , 26: take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) , 27: activate^#(X) -> c_3() , 28: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , 29: splitAt^#(0(), XS) -> c_7() , 30: natsFrom^#(N) -> c_27() , 31: natsFrom^#(X) -> c_28() } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } Weak DPs: { activate^#(X) -> c_3() , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() , U22^#(tt(), X) -> c_9(activate^#(X)) , U32^#(tt(), N) -> c_11(activate^#(N)) , U52^#(tt(), Y) -> c_17(activate^#(Y)) , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , U72^#(tt(), XS) -> c_23(activate^#(XS)) } Weak Trs: { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) , splitAt(0(), XS) -> pair(nil(), XS) , U21(tt(), X) -> U22(tt(), activate(X)) , U22(tt(), X) -> activate(X) , U31(tt(), N) -> U32(tt(), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(cons(N, XS)) -> U31(tt(), N) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , U61(tt(), N, X, XS) -> U62(tt(), activate(N), activate(X), activate(XS)) , U62(tt(), N, X, XS) -> U63(tt(), activate(N), activate(X), activate(XS)) , U63(tt(), N, X, XS) -> U64(splitAt(activate(N), activate(XS)), activate(X)) , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U71(tt(), XS) -> U72(tt(), activate(XS)) , U72(tt(), XS) -> activate(XS) , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(pair(X, Y)) -> U21(tt(), X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) We estimate the number of application of {5,7,8,15} by applications of Pre({5,7,8,15}) = {3,11,18,20}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 2: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 3: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , 4: splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , 5: U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , 6: U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 7: U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , 8: U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , 9: U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 10: U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 11: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , 12: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , 13: U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 14: U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , 15: U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , 16: U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 17: U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 18: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , 19: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , 20: tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) , 21: take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) , 22: activate^#(X) -> c_3() , 23: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , 24: splitAt^#(0(), XS) -> c_7() , 25: natsFrom^#(N) -> c_27() , 26: natsFrom^#(X) -> c_28() , 27: U22^#(tt(), X) -> c_9(activate^#(X)) , 28: U32^#(tt(), N) -> c_11(activate^#(N)) , 29: U52^#(tt(), Y) -> c_17(activate^#(Y)) , 30: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , 31: U72^#(tt(), XS) -> c_23(activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } Weak DPs: { activate^#(X) -> c_3() , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_9(activate^#(X)) , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_11(activate^#(N)) , U52^#(tt(), Y) -> c_17(activate^#(Y)) , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_23(activate^#(XS)) } Weak Trs: { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) , splitAt(0(), XS) -> pair(nil(), XS) , U21(tt(), X) -> U22(tt(), activate(X)) , U22(tt(), X) -> activate(X) , U31(tt(), N) -> U32(tt(), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(cons(N, XS)) -> U31(tt(), N) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , U61(tt(), N, X, XS) -> U62(tt(), activate(N), activate(X), activate(XS)) , U62(tt(), N, X, XS) -> U63(tt(), activate(N), activate(X), activate(XS)) , U63(tt(), N, X, XS) -> U64(splitAt(activate(N), activate(XS)), activate(X)) , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U71(tt(), XS) -> U72(tt(), activate(XS)) , U72(tt(), XS) -> activate(XS) , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(pair(X, Y)) -> U21(tt(), X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) We estimate the number of application of {3,8,14,16} by applications of Pre({3,8,14,16}) = {2,7,13}. Here rules are labeled as follows: DPs: { 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 2: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 3: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , 4: splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , 5: U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 6: U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 7: U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 8: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , 9: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , 10: U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 11: U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , 12: U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 13: U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 14: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , 15: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , 16: tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) , 17: take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) , 18: activate^#(X) -> c_3() , 19: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , 20: splitAt^#(0(), XS) -> c_7() , 21: natsFrom^#(N) -> c_27() , 22: natsFrom^#(X) -> c_28() , 23: U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , 24: U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , 25: U22^#(tt(), X) -> c_9(activate^#(X)) , 26: U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , 27: U32^#(tt(), N) -> c_11(activate^#(N)) , 28: U52^#(tt(), Y) -> c_17(activate^#(Y)) , 29: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , 30: U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , 31: U72^#(tt(), XS) -> c_23(activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } Weak DPs: { activate^#(X) -> c_3() , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_9(activate^#(X)) , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_11(activate^#(N)) , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_17(activate^#(Y)) , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_23(activate^#(XS)) , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) } Weak Trs: { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) , splitAt(0(), XS) -> pair(nil(), XS) , U21(tt(), X) -> U22(tt(), activate(X)) , U22(tt(), X) -> activate(X) , U31(tt(), N) -> U32(tt(), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(cons(N, XS)) -> U31(tt(), N) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , U61(tt(), N, X, XS) -> U62(tt(), activate(N), activate(X), activate(XS)) , U62(tt(), N, X, XS) -> U63(tt(), activate(N), activate(X), activate(XS)) , U63(tt(), N, X, XS) -> U64(splitAt(activate(N), activate(XS)), activate(X)) , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U71(tt(), XS) -> U72(tt(), activate(XS)) , U72(tt(), XS) -> activate(XS) , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(pair(X, Y)) -> U21(tt(), X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { activate^#(X) -> c_3() , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_9(activate^#(X)) , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_11(activate^#(N)) , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_17(activate^#(Y)) , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_23(activate^#(XS)) , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_30(U71^#(tt(), activate(XS)), activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) , U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } Weak Trs: { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) , splitAt(0(), XS) -> pair(nil(), XS) , U21(tt(), X) -> U22(tt(), activate(X)) , U22(tt(), X) -> activate(X) , U31(tt(), N) -> U32(tt(), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(cons(N, XS)) -> U31(tt(), N) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , U61(tt(), N, X, XS) -> U62(tt(), activate(N), activate(X), activate(XS)) , U62(tt(), N, X, XS) -> U63(tt(), activate(N), activate(X), activate(XS)) , U63(tt(), N, X, XS) -> U64(splitAt(activate(N), activate(XS)), activate(X)) , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U71(tt(), XS) -> U72(tt(), activate(XS)) , U72(tt(), XS) -> activate(XS) , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(pair(X, Y)) -> U21(tt(), X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U41^#(tt(), N, XS) -> c_12(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_13(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS), activate^#(X)) , U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) , splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, activate(XS))) , U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) , U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) , U63^#(tt(), N, X, XS) -> c_9(splitAt^#(activate(N), activate(XS))) , U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) , U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) , sel^#(N, XS) -> c_12(U41^#(tt(), N, XS)) , take^#(N, XS) -> c_13(U81^#(tt(), N, XS)) } Weak Trs: { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) , splitAt(0(), XS) -> pair(nil(), XS) , U21(tt(), X) -> U22(tt(), activate(X)) , U22(tt(), X) -> activate(X) , U31(tt(), N) -> U32(tt(), activate(N)) , U32(tt(), N) -> activate(N) , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(cons(N, XS)) -> U31(tt(), N) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , U61(tt(), N, X, XS) -> U62(tt(), activate(N), activate(X), activate(XS)) , U62(tt(), N, X, XS) -> U63(tt(), activate(N), activate(X), activate(XS)) , U63(tt(), N, X, XS) -> U64(splitAt(activate(N), activate(XS)), activate(X)) , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U71(tt(), XS) -> U72(tt(), activate(XS)) , U72(tt(), XS) -> activate(XS) , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(pair(X, Y)) -> U21(tt(), X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) We replace rewrite rules by usable rules: Weak Usable Rules: { activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) , splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, activate(XS))) , U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) , U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) , U63^#(tt(), N, X, XS) -> c_9(splitAt^#(activate(N), activate(XS))) , U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) , U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) , sel^#(N, XS) -> c_12(U41^#(tt(), N, XS)) , take^#(N, XS) -> c_13(U81^#(tt(), N, XS)) } Weak Trs: { activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) Consider the dependency graph 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) -->_1 U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) :2 2: U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, activate(XS))) :3 3: splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, activate(XS))) -->_1 U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) :4 4: U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) -->_1 U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) :8 5: U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) -->_1 U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) :6 6: U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) -->_1 afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) :7 7: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) -->_1 U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) :1 8: U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) -->_1 U63^#(tt(), N, X, XS) -> c_9(splitAt^#(activate(N), activate(XS))) :9 9: U63^#(tt(), N, X, XS) -> c_9(splitAt^#(activate(N), activate(XS))) -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, activate(XS))) :3 10: U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) -->_1 U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) :11 11: U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, activate(XS))) :3 12: sel^#(N, XS) -> c_12(U41^#(tt(), N, XS)) -->_1 U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) :5 13: take^#(N, XS) -> c_13(U81^#(tt(), N, XS)) -->_1 U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) :10 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { sel^#(N, XS) -> c_12(U41^#(tt(), N, XS)) , take^#(N, XS) -> c_13(U81^#(tt(), N, XS)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) , splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, activate(XS))) , U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) , U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) , U63^#(tt(), N, X, XS) -> c_9(splitAt^#(activate(N), activate(XS))) , U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) , U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) } Weak Trs: { activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1}, Uargs(c_11) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [tt] = [2] [activate](x1) = [1] x1 + [0] [cons](x1, x2) = [0] [natsFrom](x1) = [0] [n__natsFrom](x1) = [0] [s](x1) = [1] x1 + [3] [U11^#](x1, x2, x3) = [2] x2 + [2] [U12^#](x1, x2, x3) = [2] x2 + [1] [splitAt^#](x1, x2) = [2] x1 + [0] [U61^#](x1, x2, x3, x4) = [2] x1 + [2] x2 + [0] [U41^#](x1, x2, x3) = [1] x1 + [3] x2 + [3] x3 + [3] [U42^#](x1, x2, x3) = [2] x1 + [2] x2 + [0] [afterNth^#](x1, x2) = [2] x1 + [3] [U62^#](x1, x2, x3, x4) = [2] x2 + [2] [U63^#](x1, x2, x3, x4) = [2] x2 + [1] [U81^#](x1, x2, x3) = [1] x1 + [3] x2 + [3] x3 + [3] [U82^#](x1, x2, x3) = [2] x2 + [2] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] [c_3](x1) = [1] x1 + [1] [c_4](x1) = [1] x1 + [1] [c_5](x1) = [1] x1 + [0] [c_6](x1) = [1] x1 + [0] [c_7](x1) = [1] x1 + [0] [c_8](x1) = [1] x1 + [0] [c_9](x1) = [1] x1 + [0] [c_10](x1) = [1] x1 + [1] [c_11](x1) = [1] x1 + [1] This order satisfies following ordering constraints: [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__natsFrom(X))] = [0] >= [0] = [natsFrom(X)] [natsFrom(N)] = [0] >= [0] = [cons(N, n__natsFrom(s(N)))] [natsFrom(X)] = [0] >= [0] = [n__natsFrom(X)] [U11^#(tt(), N, XS)] = [2] N + [2] > [2] N + [1] = [c_1(U12^#(tt(), activate(N), activate(XS)))] [U12^#(tt(), N, XS)] = [2] N + [1] > [2] N + [0] = [c_2(splitAt^#(activate(N), activate(XS)))] [splitAt^#(s(N), cons(X, XS))] = [2] N + [6] > [2] N + [5] = [c_3(U61^#(tt(), N, X, activate(XS)))] [U61^#(tt(), N, X, XS)] = [2] N + [4] > [2] N + [3] = [c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))] [U41^#(tt(), N, XS)] = [3] N + [3] XS + [5] > [2] N + [4] = [c_5(U42^#(tt(), activate(N), activate(XS)))] [U42^#(tt(), N, XS)] = [2] N + [4] > [2] N + [3] = [c_6(afterNth^#(activate(N), activate(XS)))] [afterNth^#(N, XS)] = [2] N + [3] > [2] N + [2] = [c_7(U11^#(tt(), N, XS))] [U62^#(tt(), N, X, XS)] = [2] N + [2] > [2] N + [1] = [c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))] [U63^#(tt(), N, X, XS)] = [2] N + [1] > [2] N + [0] = [c_9(splitAt^#(activate(N), activate(XS)))] [U81^#(tt(), N, XS)] = [3] N + [3] XS + [5] > [2] N + [3] = [c_10(U82^#(tt(), activate(N), activate(XS)))] [U82^#(tt(), N, XS)] = [2] N + [2] > [2] N + [1] = [c_11(splitAt^#(activate(N), activate(XS)))] Hurray, we answered YES(?,O(n^1))