YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),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(1),O(n^1)) We add the 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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),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(1),O(n^1)) We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component: Problem (R): ------------ 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))) } Weak DPs: { 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) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# U51^# U61^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom s 0 nil Strategy: innermost Problem (S): ------------ Strict DPs: { U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) , U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) } Weak 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))) } Weak Trs: { activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# U51^# U61^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom s 0 nil Strategy: innermost Overall, the transformation results in the following sub-problem(s): Generated new problems: ----------------------- R) 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))) } Weak DPs: { 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) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# U51^# U61^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom s 0 nil Strategy: innermost This problem was proven YES(O(1),O(n^1)). S) Strict DPs: { U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) , U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) } Weak 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))) } Weak Trs: { activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(X) , natsFrom(N) -> cons(N, n__natsFrom(s(N))) , natsFrom(X) -> n__natsFrom(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# U51^# U61^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom s 0 nil Strategy: innermost This problem was proven YES(O(1),O(1)). Proofs for generated problems: ------------------------------ R) We are left with following problem, upon which TcT provides the certificate YES(O(1),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))) } Weak DPs: { 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(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) , 3: splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, activate(XS))) , 4: U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) } Sub-proof: ---------- 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 the following constructor-based matrix interpretation satisfying not(EDA). [U11](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [tt] = [0] [U12](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [activate](x1) = [1] x1 + [0] [snd](x1) = [7] x1 + [0] [splitAt](x1, x2) = [7] x1 + [7] x2 + [0] [U21](x1, x2) = [7] x1 + [7] x2 + [0] [U22](x1, x2) = [7] x1 + [7] x2 + [0] [U31](x1, x2) = [7] x1 + [7] x2 + [0] [U32](x1, x2) = [7] x1 + [7] x2 + [0] [U41](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U42](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [head](x1) = [7] x1 + [0] [afterNth](x1, x2) = [7] x1 + [7] x2 + [0] [U51](x1, x2) = [7] x1 + [7] x2 + [0] [U52](x1, x2) = [7] x1 + [7] x2 + [0] [U61](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U62](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U63](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U64](x1, x2) = [7] x1 + [7] x2 + [0] [pair](x1, x2) = [1] x1 + [1] x2 + [0] [cons](x1, x2) = [0] [U71](x1, x2) = [7] x1 + [7] x2 + [0] [U72](x1, x2) = [7] x1 + [7] x2 + [0] [U81](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U82](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [fst](x1) = [7] x1 + [0] [natsFrom](x1) = [0] [n__natsFrom](x1) = [0] [s](x1) = [1] x1 + [7] [sel](x1, x2) = [7] x1 + [7] x2 + [0] [0] = [0] [nil] = [0] [tail](x1) = [7] x1 + [0] [take](x1, x2) = [7] x1 + [7] x2 + [0] [U11^#](x1, x2, x3) = [4] x2 + [4] [c_1](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U12^#](x1, x2, x3) = [2] x2 + [1] [activate^#](x1) = [7] x1 + [0] [c_2](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [snd^#](x1) = [7] x1 + [0] [splitAt^#](x1, x2) = [1] x1 + [1] [c_3] = [0] [c_4](x1) = [7] x1 + [0] [natsFrom^#](x1) = [7] x1 + [0] [c_5](x1) = [7] x1 + [0] [U51^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_6](x1, x2) = [7] x1 + [7] x2 + [0] [U61^#](x1, x2, x3, x4) = [1] x2 + [4] [c_7] = [0] [U21^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_8](x1, x2) = [7] x1 + [7] x2 + [0] [U22^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_9](x1) = [7] x1 + [0] [U31^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [U32^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_11](x1) = [7] x1 + [0] [U41^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] [c_12](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U42^#](x1, x2, x3) = [4] x2 + [4] [c_13](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [head^#](x1) = [7] x1 + [0] [afterNth^#](x1, x2) = [4] x1 + [4] [c_14](x1) = [7] x1 + [0] [c_15](x1) = [7] x1 + [0] [c_16](x1, x2) = [7] x1 + [7] x2 + [0] [U52^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_17](x1) = [7] x1 + [0] [c_18](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U62^#](x1, x2, x3, x4) = [1] x2 + [1] [c_19](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U63^#](x1, x2, x3, x4) = [1] x2 + [1] [c_20](x1, x2, x3, x4, x5) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [7] x5 + [0] [U64^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_21](x1) = [7] x1 + [0] [U71^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_22](x1, x2) = [7] x1 + [7] x2 + [0] [U72^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_23](x1) = [7] x1 + [0] [U81^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] [c_24](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U82^#](x1, x2, x3) = [4] x2 + [4] [c_25](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [fst^#](x1) = [7] x1 + [0] [c_26](x1) = [7] x1 + [0] [c_27] = [0] [c_28] = [0] [sel^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_29](x1) = [7] x1 + [0] [tail^#](x1) = [7] x1 + [0] [c_30](x1, x2) = [7] x1 + [7] x2 + [0] [take^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_31](x1) = [7] x1 + [0] [c] = [0] [c_1](x1) = [1] x1 + [1] [c_2](x1) = [1] x1 + [0] [c_3](x1) = [1] x1 + [1] [c_4](x1) = [1] x1 + [1] [c_5](x1) = [1] x1 + [3] [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 + [3] [c_11](x1) = [4] x1 + [0] [c_12](x1) = [7] x1 + [0] [c_13](x1) = [7] x1 + [0] The following symbols are considered usable {activate, natsFrom, U11^#, U12^#, splitAt^#, U61^#, U41^#, U42^#, afterNth^#, U62^#, U63^#, U81^#, U82^#} The order satisfies the 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)] = [4] N + [4] > [2] N + [2] = [c_1(U12^#(tt(), activate(N), activate(XS)))] [U12^#(tt(), N, XS)] = [2] N + [1] >= [1] N + [1] = [c_2(splitAt^#(activate(N), activate(XS)))] [splitAt^#(s(N), cons(X, XS))] = [1] N + [8] > [1] N + [5] = [c_3(U61^#(tt(), N, X, activate(XS)))] [U61^#(tt(), N, X, XS)] = [1] N + [4] > [1] N + [2] = [c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))] [U41^#(tt(), N, XS)] = [7] N + [7] XS + [7] >= [4] N + [7] = [c_5(U42^#(tt(), activate(N), activate(XS)))] [U42^#(tt(), N, XS)] = [4] N + [4] >= [4] N + [4] = [c_6(afterNth^#(activate(N), activate(XS)))] [afterNth^#(N, XS)] = [4] N + [4] >= [4] N + [4] = [c_7(U11^#(tt(), N, XS))] [U62^#(tt(), N, X, XS)] = [1] N + [1] >= [1] N + [1] = [c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))] [U63^#(tt(), N, X, XS)] = [1] N + [1] >= [1] N + [1] = [c_9(splitAt^#(activate(N), activate(XS)))] [U81^#(tt(), N, XS)] = [7] N + [7] XS + [7] >= [4] N + [7] = [c_10(U82^#(tt(), activate(N), activate(XS)))] [U82^#(tt(), N, XS)] = [4] N + [4] >= [4] N + [4] = [c_11(splitAt^#(activate(N), activate(XS)))] We return to the main proof. Consider the set of all dependency pairs : { 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) , 2: U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) , 3: splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, activate(XS))) , 4: U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) , 5: U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) , 6: U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) , 7: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) , 8: U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) , 9: U63^#(tt(), N, X, XS) -> c_9(splitAt^#(activate(N), activate(XS))) , 10: U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) , 11: U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {1,3,4}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,6,7,8,9,10,11}, their number of application is equally bounded. The dependency pairs are shifted into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak 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(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { 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))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). 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(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded S) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) , U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) } Weak 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))) } 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(1),O(1)) We estimate the number of application of {2} by applications of Pre({2}) = {1}. Here rules are labeled as follows: DPs: { 1: U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) , 2: U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) , 3: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) , 4: U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) , 5: splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, activate(XS))) , 6: U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) , 7: U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) , 8: U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) , 9: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) , 10: U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) , 11: U63^#(tt(), N, X, XS) -> c_9(splitAt^#(activate(N), activate(XS))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) } Weak 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))) , 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(1),O(1)) We estimate the number of application of {1} by applications of Pre({1}) = {}. Here rules are labeled as follows: DPs: { 1: U81^#(tt(), N, XS) -> c_10(U82^#(tt(), activate(N), activate(XS))) , 2: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) , 3: U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) , 4: splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, activate(XS))) , 5: U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) , 6: U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) , 7: U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) , 8: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) , 9: U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) , 10: U63^#(tt(), N, X, XS) -> c_9(splitAt^#(activate(N), activate(XS))) , 11: U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak 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(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { 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))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). 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(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))