YES(O(1),POLY) We are left with following problem, upon which TcT provides the certificate YES(O(1),POLY). 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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(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(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , s(X) -> n__s(X) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(O(1),POLY) Arguments of following rules are not normal-forms: { splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) } All above mentioned rules can be savely removed. We are left with following problem, upon which TcT provides the certificate YES(O(1),POLY). 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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , 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(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , s(X) -> n__s(X) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(O(1),POLY) 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^#(activate(X)), activate^#(X)) , activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X)) , snd^#(pair(X, Y)) -> c_6(U51^#(tt(), Y)) , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() , s^#(X) -> c_30() , 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)) , 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)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), 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)) , 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_31(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_32(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),POLY). 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^#(activate(X)), activate^#(X)) , activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X)) , snd^#(pair(X, Y)) -> c_6(U51^#(tt(), Y)) , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() , s^#(X) -> c_30() , 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)) , 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)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), 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)) , 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_31(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_32(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , 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(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , s(X) -> n__s(X) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(O(1),POLY) We estimate the number of application of {3,7,8,9,10} by applications of Pre({3,7,8,9,10}) = {1,2,4,5,11,12,13,14,15,16,17,20,21,22,23,24,25,26,27,28,31}. 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^#(activate(X)), activate^#(X)) , 5: activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X)) , 6: snd^#(pair(X, Y)) -> c_6(U51^#(tt(), Y)) , 7: splitAt^#(0(), XS) -> c_7() , 8: natsFrom^#(N) -> c_27() , 9: natsFrom^#(X) -> c_28() , 10: s^#(X) -> c_30() , 11: U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) , 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: U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 22: U62^#(tt(), N, X, XS) -> c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 23: 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)) , 24: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) , 25: U71^#(tt(), XS) -> c_22(U72^#(tt(), activate(XS)), activate^#(XS)) , 26: U72^#(tt(), XS) -> c_23(activate^#(XS)) , 27: U81^#(tt(), N, XS) -> c_24(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 28: U82^#(tt(), N, XS) -> c_25(fst^#(splitAt(activate(N), activate(XS))), splitAt^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 29: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) , 30: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) , 31: tail^#(cons(N, XS)) -> c_31(U71^#(tt(), activate(XS)), activate^#(XS)) , 32: take^#(N, XS) -> c_32(U81^#(tt(), N, XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),POLY). 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^#(activate(X)), activate^#(X)) , activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X)) , snd^#(pair(X, Y)) -> c_6(U51^#(tt(), Y)) , 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)) , 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)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), 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)) , 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_31(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_32(U81^#(tt(), N, XS)) } Weak DPs: { activate^#(X) -> c_3() , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() , s^#(X) -> c_30() } 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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , 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(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , s(X) -> n__s(X) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(O(1),POLY) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { activate^#(X) -> c_3() , splitAt^#(0(), XS) -> c_7() , natsFrom^#(N) -> c_27() , natsFrom^#(X) -> c_28() , s^#(X) -> c_30() } We are left with following problem, upon which TcT provides the certificate YES(O(1),POLY). 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^#(activate(X)), activate^#(X)) , activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X)) , snd^#(pair(X, Y)) -> c_6(U51^#(tt(), Y)) , 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)) , 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)) , U61^#(tt(), N, X, XS) -> c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), 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)) , 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_31(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_32(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , 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(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , s(X) -> n__s(X) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(O(1),POLY) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { 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^#(activate(X)), activate^#(X)) , activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X)) , 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)) , 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),POLY). 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))), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , sel^#(N, XS) -> c_25(U41^#(tt(), N, XS)) , tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_27(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , 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(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U41(tt(), N, XS) , s(X) -> n__s(X) , tail(cons(N, XS)) -> U71(tt(), activate(XS)) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: YES(O(1),POLY) We replace rewrite rules by usable rules: Weak Usable Rules: { 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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } We are left with following problem, upon which TcT provides the certificate YES(O(1),POLY). 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))), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , sel^#(N, XS) -> c_25(U41^#(tt(), N, XS)) , tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) , take^#(N, XS) -> c_27(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),POLY) Consider the dependency graph 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) -->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_1 U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) :2 2: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) -->_1 snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) :5 -->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 3: activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) -->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 4: activate^#(n__s(X)) -> c_4(activate^#(X)) -->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 5: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) -->_1 U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) :6 6: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) -->_1 U52^#(tt(), Y) -> c_15(activate^#(Y)) :15 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 7: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) -->_1 U22^#(tt(), X) -> c_8(activate^#(X)) :8 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 8: U22^#(tt(), X) -> c_8(activate^#(X)) -->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 9: U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) -->_1 U32^#(tt(), N) -> c_10(activate^#(N)) :10 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 10: U32^#(tt(), N) -> c_10(activate^#(N)) -->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 11: U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) -->_1 U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) :12 -->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 12: U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) -->_2 afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) :14 -->_1 head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) :13 -->_4 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_4 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 13: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) -->_1 U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) :9 14: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) -->_1 U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) :1 15: U52^#(tt(), Y) -> c_15(activate^#(Y)) -->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 16: U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) -->_1 U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) :17 -->_4 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_4 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 17: U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) -->_1 U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) :18 -->_4 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_4 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 18: U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) -->_1 U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) :19 -->_4 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_4 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 19: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) -->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 20: U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) -->_1 U72^#(tt(), XS) -> c_21(activate^#(XS)) :21 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 21: U72^#(tt(), XS) -> c_21(activate^#(XS)) -->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 22: U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) -->_1 U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) :23 -->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 23: U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) -->_1 fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) :24 -->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 24: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) -->_1 U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) :7 25: sel^#(N, XS) -> c_25(U41^#(tt(), N, XS)) -->_1 U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) :11 26: tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) -->_1 U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) :20 -->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4 -->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3 27: take^#(N, XS) -> c_27(U81^#(tt(), N, XS)) -->_1 U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) :22 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_25(U41^#(tt(), N, XS)) , take^#(N, XS) -> c_27(U81^#(tt(), N, XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),POLY). 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))), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),POLY) 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)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) } Weak DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__s 0 nil Strategy: innermost Problem (S): ------------ Strict DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) } Weak DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__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)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) } Weak DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__s 0 nil Strategy: innermost This problem was proven YES(O(1),POLY). S) Strict DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) } Weak DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__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),POLY). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) } Weak DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),POLY) 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: { activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) } Weak 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))), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__s 0 nil Strategy: innermost Problem (S): ------------ Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) } Weak DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__s 0 nil Strategy: innermost Overall, the transformation results in the following sub-problem(s): Generated new problems: ----------------------- R) Strict DPs: { activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) } Weak 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))), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__s 0 nil Strategy: innermost This problem was proven YES(?,POLY). S) Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) } Weak DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__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(?,POLY). Strict DPs: { activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) } Weak 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))), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(?,POLY) The input was oriented with the instance of 'Polynomial Path Order (PS)' as induced by the safe mapping safe(U11) = {}, safe(tt) = {}, safe(U12) = {}, safe(activate) = {}, safe(snd) = {}, safe(splitAt) = {}, safe(U21) = {}, safe(U22) = {}, safe(U31) = {}, safe(U32) = {}, safe(U41) = {}, safe(U42) = {}, safe(head) = {}, safe(afterNth) = {}, safe(U51) = {}, safe(U52) = {}, safe(U61) = {}, safe(U62) = {}, safe(U63) = {}, safe(U64) = {}, safe(pair) = {1, 2}, safe(cons) = {1, 2}, safe(U71) = {}, safe(U72) = {}, safe(U81) = {}, safe(U82) = {}, safe(fst) = {}, safe(natsFrom) = {1}, safe(n__natsFrom) = {1}, safe(n__s) = {1}, safe(sel) = {}, safe(0) = {}, safe(nil) = {}, safe(s) = {1}, safe(tail) = {}, safe(take) = {}, safe(U11^#) = {}, safe(c_1) = {}, safe(U12^#) = {}, safe(activate^#) = {}, safe(c_2) = {}, safe(snd^#) = {}, safe(splitAt^#) = {}, safe(c_3) = {}, safe(c_4) = {}, safe(natsFrom^#) = {}, safe(c_5) = {}, safe(s^#) = {}, safe(c_6) = {}, safe(U51^#) = {}, safe(c_7) = {}, safe(U21^#) = {}, safe(c_8) = {}, safe(U22^#) = {}, safe(c_9) = {}, safe(U31^#) = {1}, safe(c_10) = {}, safe(U32^#) = {1}, safe(c_11) = {}, safe(U41^#) = {}, safe(c_12) = {}, safe(U42^#) = {}, safe(c_13) = {}, safe(head^#) = {}, safe(afterNth^#) = {}, safe(c_14) = {}, safe(c_15) = {}, safe(c_16) = {}, safe(U52^#) = {1}, safe(c_17) = {}, safe(U61^#) = {}, safe(c_18) = {}, safe(U62^#) = {}, safe(c_19) = {}, safe(U63^#) = {}, safe(c_20) = {}, safe(U64^#) = {}, safe(c_21) = {}, safe(U71^#) = {1}, safe(c_22) = {}, safe(U72^#) = {1}, safe(c_23) = {}, safe(U81^#) = {}, safe(c_24) = {}, safe(U82^#) = {}, safe(c_25) = {}, safe(fst^#) = {}, safe(c_26) = {}, safe(c_27) = {}, safe(c_28) = {}, safe(sel^#) = {}, safe(c_29) = {}, safe(c_30) = {}, safe(tail^#) = {}, safe(c_31) = {}, safe(take^#) = {}, safe(c_32) = {}, safe(c) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(c_6) = {}, safe(c_7) = {}, safe(c_8) = {}, safe(c_9) = {}, safe(c_10) = {}, safe(c_11) = {}, safe(c_12) = {}, safe(c_13) = {}, safe(c_14) = {}, safe(c_15) = {}, safe(c_16) = {}, safe(c_17) = {}, safe(c_18) = {}, safe(c_19) = {}, safe(c_20) = {}, safe(c_21) = {}, safe(c_22) = {}, safe(c_23) = {}, safe(c_24) = {}, safe(c_25) = {}, safe(c_26) = {}, safe(c_27) = {} and precedence U11 > U12, U11 > activate, U11 > snd, U11 > splitAt, U11 > U51, U11 > U52, U11 > natsFrom, U11 > s, U11 > activate^#, U11 > U22^#, U11 > U32^#, U11 > U64^#, U12 > activate, U12 > snd, U12 > splitAt, U12 > U51, U12 > U52, U12 > natsFrom, U12 > s, U12 > activate^#, U12 > U22^#, U12 > U32^#, U12 > U64^#, activate > splitAt, activate > natsFrom, activate > s, activate > activate^#, activate > U64^#, snd > activate, snd > splitAt, snd > U51, snd > U52, snd > natsFrom, snd > s, snd > activate^#, snd > U22^#, snd > U32^#, snd > U64^#, afterNth > U12, afterNth > activate, afterNth > snd, afterNth > splitAt, afterNth > U51, afterNth > U52, afterNth > natsFrom, afterNth > s, afterNth > activate^#, afterNth > U22^#, afterNth > U32^#, afterNth > U64^#, U51 > activate, U51 > splitAt, U51 > U52, U51 > natsFrom, U51 > s, U51 > activate^#, U51 > U22^#, U51 > U32^#, U51 > U64^#, U52 > activate, U52 > splitAt, U52 > natsFrom, U52 > s, U52 > activate^#, U52 > U22^#, U52 > U32^#, U52 > U64^#, natsFrom > splitAt, natsFrom > activate^#, natsFrom > U64^#, s > splitAt, s > activate^#, s > U64^#, U11^# > U11, U11^# > U12, U11^# > activate, U11^# > snd, U11^# > splitAt, U11^# > afterNth, U11^# > U51, U11^# > U52, U11^# > natsFrom, U11^# > s, U11^# > U12^#, U11^# > activate^#, U11^# > snd^#, U11^# > U51^#, U11^# > U21^#, U11^# > U22^#, U11^# > U31^#, U11^# > U32^#, U11^# > head^#, U11^# > U52^#, U11^# > U61^#, U11^# > U62^#, U11^# > U63^#, U11^# > U64^#, U11^# > U71^#, U11^# > U72^#, U11^# > U81^#, U11^# > U82^#, U11^# > fst^#, U12^# > U11, U12^# > U12, U12^# > activate, U12^# > snd, U12^# > splitAt, U12^# > afterNth, U12^# > U51, U12^# > U52, U12^# > natsFrom, U12^# > s, U12^# > activate^#, U12^# > snd^#, U12^# > U51^#, U12^# > U21^#, U12^# > U22^#, U12^# > U31^#, U12^# > U32^#, U12^# > head^#, U12^# > U52^#, U12^# > U61^#, U12^# > U62^#, U12^# > U63^#, U12^# > U64^#, U12^# > U71^#, U12^# > U72^#, U12^# > U81^#, U12^# > U82^#, U12^# > fst^#, snd^# > U11, snd^# > U12, snd^# > activate, snd^# > snd, snd^# > splitAt, snd^# > afterNth, snd^# > U51, snd^# > U52, snd^# > natsFrom, snd^# > s, snd^# > activate^#, snd^# > U21^#, snd^# > U22^#, snd^# > U31^#, snd^# > U32^#, snd^# > head^#, snd^# > U52^#, snd^# > U61^#, snd^# > U62^#, snd^# > U63^#, snd^# > U64^#, snd^# > U72^#, snd^# > U82^#, snd^# > fst^#, U51^# > U11, U51^# > U12, U51^# > activate, U51^# > snd, U51^# > splitAt, U51^# > afterNth, U51^# > U51, U51^# > U52, U51^# > natsFrom, U51^# > s, U51^# > activate^#, U51^# > U21^#, U51^# > U22^#, U51^# > U31^#, U51^# > U32^#, U51^# > head^#, U51^# > U52^#, U51^# > U61^#, U51^# > U62^#, U51^# > U63^#, U51^# > U64^#, U51^# > U72^#, U51^# > U82^#, U51^# > fst^#, U21^# > U11, U21^# > U12, U21^# > activate, U21^# > snd, U21^# > splitAt, U21^# > afterNth, U21^# > U51, U21^# > U52, U21^# > natsFrom, U21^# > s, U21^# > activate^#, U21^# > U22^#, U21^# > U32^#, U21^# > U64^#, U22^# > splitAt, U22^# > natsFrom, U22^# > s, U22^# > activate^#, U22^# > U64^#, U31^# > U11, U31^# > U12, U31^# > activate, U31^# > snd, U31^# > splitAt, U31^# > afterNth, U31^# > U51, U31^# > U52, U31^# > natsFrom, U31^# > s, U31^# > activate^#, U31^# > U22^#, U31^# > U32^#, U31^# > U64^#, U32^# > splitAt, U32^# > natsFrom, U32^# > s, U32^# > activate^#, U32^# > U64^#, U41^# > U11, U41^# > U12, U41^# > activate, U41^# > snd, U41^# > splitAt, U41^# > afterNth, U41^# > U51, U41^# > U52, U41^# > natsFrom, U41^# > s, U41^# > U11^#, U41^# > U12^#, U41^# > activate^#, U41^# > snd^#, U41^# > U51^#, U41^# > U21^#, U41^# > U22^#, U41^# > U31^#, U41^# > U32^#, U41^# > U42^#, U41^# > head^#, U41^# > afterNth^#, U41^# > U52^#, U41^# > U61^#, U41^# > U62^#, U41^# > U63^#, U41^# > U64^#, U41^# > U71^#, U41^# > U72^#, U41^# > U81^#, U41^# > U82^#, U41^# > fst^#, U42^# > U11, U42^# > U12, U42^# > activate, U42^# > snd, U42^# > splitAt, U42^# > afterNth, U42^# > U51, U42^# > U52, U42^# > natsFrom, U42^# > s, U42^# > U11^#, U42^# > U12^#, U42^# > activate^#, U42^# > snd^#, U42^# > U51^#, U42^# > U21^#, U42^# > U22^#, U42^# > U31^#, U42^# > U32^#, U42^# > head^#, U42^# > afterNth^#, U42^# > U52^#, U42^# > U61^#, U42^# > U62^#, U42^# > U63^#, U42^# > U64^#, U42^# > U71^#, U42^# > U72^#, U42^# > U81^#, U42^# > U82^#, U42^# > fst^#, head^# > U11, head^# > U12, head^# > activate, head^# > snd, head^# > splitAt, head^# > afterNth, head^# > U51, head^# > U52, head^# > natsFrom, head^# > s, head^# > activate^#, head^# > U22^#, head^# > U32^#, head^# > U64^#, afterNth^# > U11, afterNth^# > U12, afterNth^# > activate, afterNth^# > snd, afterNth^# > splitAt, afterNth^# > afterNth, afterNth^# > U51, afterNth^# > U52, afterNth^# > natsFrom, afterNth^# > s, afterNth^# > U11^#, afterNth^# > U12^#, afterNth^# > activate^#, afterNth^# > snd^#, afterNth^# > U51^#, afterNth^# > U21^#, afterNth^# > U22^#, afterNth^# > U31^#, afterNth^# > U32^#, afterNth^# > head^#, afterNth^# > U52^#, afterNth^# > U61^#, afterNth^# > U62^#, afterNth^# > U63^#, afterNth^# > U64^#, afterNth^# > U71^#, afterNth^# > U72^#, afterNth^# > U81^#, afterNth^# > U82^#, afterNth^# > fst^#, U52^# > U11, U52^# > U12, U52^# > activate, U52^# > snd, U52^# > splitAt, U52^# > afterNth, U52^# > U51, U52^# > U52, U52^# > natsFrom, U52^# > s, U52^# > activate^#, U52^# > U22^#, U52^# > U32^#, U52^# > U64^#, U61^# > U11, U61^# > U12, U61^# > activate, U61^# > snd, U61^# > splitAt, U61^# > afterNth, U61^# > U51, U61^# > U52, U61^# > natsFrom, U61^# > s, U61^# > activate^#, U61^# > U21^#, U61^# > U22^#, U61^# > U31^#, U61^# > U32^#, U61^# > head^#, U61^# > U52^#, U61^# > U62^#, U61^# > U63^#, U61^# > U64^#, U61^# > U72^#, U61^# > U82^#, U61^# > fst^#, U62^# > U11, U62^# > U12, U62^# > activate, U62^# > snd, U62^# > splitAt, U62^# > afterNth, U62^# > U51, U62^# > U52, U62^# > natsFrom, U62^# > s, U62^# > activate^#, U62^# > U21^#, U62^# > U22^#, U62^# > U31^#, U62^# > U32^#, U62^# > head^#, U62^# > U52^#, U62^# > U63^#, U62^# > U64^#, U62^# > U72^#, U62^# > fst^#, U63^# > U11, U63^# > U12, U63^# > activate, U63^# > snd, U63^# > splitAt, U63^# > afterNth, U63^# > U51, U63^# > U52, U63^# > natsFrom, U63^# > s, U63^# > activate^#, U63^# > U22^#, U63^# > U32^#, U63^# > U64^#, U71^# > U11, U71^# > U12, U71^# > activate, U71^# > snd, U71^# > splitAt, U71^# > afterNth, U71^# > U51, U71^# > U52, U71^# > natsFrom, U71^# > s, U71^# > activate^#, U71^# > U21^#, U71^# > U22^#, U71^# > U31^#, U71^# > U32^#, U71^# > head^#, U71^# > U52^#, U71^# > U61^#, U71^# > U62^#, U71^# > U63^#, U71^# > U64^#, U71^# > U72^#, U71^# > U82^#, U71^# > fst^#, U72^# > U11, U72^# > U12, U72^# > activate, U72^# > snd, U72^# > splitAt, U72^# > afterNth, U72^# > U51, U72^# > U52, U72^# > natsFrom, U72^# > s, U72^# > activate^#, U72^# > U22^#, U72^# > U32^#, U72^# > U64^#, U81^# > U11, U81^# > U12, U81^# > activate, U81^# > snd, U81^# > splitAt, U81^# > afterNth, U81^# > U51, U81^# > U52, U81^# > natsFrom, U81^# > s, U81^# > activate^#, U81^# > U21^#, U81^# > U22^#, U81^# > U31^#, U81^# > U32^#, U81^# > head^#, U81^# > U52^#, U81^# > U61^#, U81^# > U62^#, U81^# > U63^#, U81^# > U64^#, U81^# > U72^#, U81^# > U82^#, U81^# > fst^#, U82^# > U11, U82^# > U12, U82^# > activate, U82^# > snd, U82^# > splitAt, U82^# > afterNth, U82^# > U51, U82^# > U52, U82^# > natsFrom, U82^# > s, U82^# > activate^#, U82^# > U21^#, U82^# > U22^#, U82^# > U31^#, U82^# > U32^#, U82^# > head^#, U82^# > U52^#, U82^# > U63^#, U82^# > U64^#, U82^# > U72^#, U82^# > fst^#, fst^# > U11, fst^# > U12, fst^# > activate, fst^# > snd, fst^# > splitAt, fst^# > afterNth, fst^# > U51, fst^# > U52, fst^# > natsFrom, fst^# > s, fst^# > activate^#, fst^# > U22^#, fst^# > U32^#, fst^# > U64^#, tail^# > U11, tail^# > U12, tail^# > activate, tail^# > snd, tail^# > splitAt, tail^# > afterNth, tail^# > U51, tail^# > U52, tail^# > natsFrom, tail^# > s, tail^# > U11^#, tail^# > U12^#, tail^# > activate^#, tail^# > snd^#, tail^# > U51^#, tail^# > U21^#, tail^# > U22^#, tail^# > U31^#, tail^# > U32^#, tail^# > U42^#, tail^# > head^#, tail^# > afterNth^#, tail^# > U52^#, tail^# > U61^#, tail^# > U62^#, tail^# > U63^#, tail^# > U64^#, tail^# > U71^#, tail^# > U72^#, tail^# > U81^#, tail^# > U82^#, tail^# > fst^#, U11 ~ afterNth, activate ~ U22^#, activate ~ U32^#, splitAt ~ activate^#, splitAt ~ U64^#, natsFrom ~ s, activate^# ~ U64^#, snd^# ~ U51^#, snd^# ~ U71^#, snd^# ~ U81^#, U51^# ~ U71^#, U51^# ~ U81^#, U21^# ~ U31^#, U21^# ~ head^#, U21^# ~ U52^#, U21^# ~ U63^#, U21^# ~ U72^#, U21^# ~ fst^#, U22^# ~ U32^#, U31^# ~ head^#, U31^# ~ U52^#, U31^# ~ U63^#, U31^# ~ U72^#, U31^# ~ fst^#, U41^# ~ tail^#, head^# ~ U52^#, head^# ~ U63^#, head^# ~ U72^#, head^# ~ fst^#, U52^# ~ U63^#, U52^# ~ U72^#, U52^# ~ fst^#, U62^# ~ U82^#, U63^# ~ U72^#, U63^# ~ fst^#, U71^# ~ U81^#, U72^# ~ fst^# . Following symbols are considered recursive: {activate, U51, U52, natsFrom, s, U11^#, activate^#, snd^#, U51^#, U21^#, U22^#, U31^#, U32^#, U41^#, head^#, afterNth^#, U52^#, U61^#, U62^#, U64^#, U71^#, U72^#, U81^#, fst^#} The recursion depth is 12. Further, following argument filtering is employed: pi(U11) = [3], pi(tt) = [], pi(U12) = [3], pi(activate) = [1], pi(snd) = [1], pi(splitAt) = [2], pi(U21) = [], pi(U22) = [], pi(U31) = [], pi(U32) = [], pi(U41) = [], pi(U42) = [], pi(head) = [], pi(afterNth) = [2], pi(U51) = [2], pi(U52) = [2], pi(U61) = [], pi(U62) = [], pi(U63) = [], pi(U64) = [], pi(pair) = [1, 2], pi(cons) = [1, 2], pi(U71) = [], pi(U72) = [], pi(U81) = [], pi(U82) = [], pi(fst) = [], pi(natsFrom) = [1], pi(n__natsFrom) = [1], pi(n__s) = [1], pi(sel) = [], pi(0) = [], pi(nil) = [], pi(s) = [1], pi(tail) = [], pi(take) = [], pi(U11^#) = [2, 3], pi(c_1) = [], pi(U12^#) = [2, 3], pi(activate^#) = [1], pi(c_2) = [], pi(snd^#) = [1], pi(splitAt^#) = [], pi(c_3) = [], pi(c_4) = [], pi(natsFrom^#) = [], pi(c_5) = [], pi(s^#) = [], pi(c_6) = [], pi(U51^#) = [2], pi(c_7) = [], pi(U21^#) = [2], pi(c_8) = [], pi(U22^#) = [2], pi(c_9) = [], pi(U31^#) = [2], pi(c_10) = [], pi(U32^#) = [1, 2], pi(c_11) = [], pi(U41^#) = [2, 3], pi(c_12) = [], pi(U42^#) = [1, 2, 3], pi(c_13) = [], pi(head^#) = [1], pi(afterNth^#) = [1, 2], pi(c_14) = [], pi(c_15) = [], pi(c_16) = [], pi(U52^#) = [1, 2], pi(c_17) = [], pi(U61^#) = [2, 3, 4], pi(c_18) = [], pi(U62^#) = [2, 3, 4], pi(c_19) = [], pi(U63^#) = [2, 3, 4], pi(c_20) = [], pi(U64^#) = [1, 2], pi(c_21) = [], pi(U71^#) = [2], pi(c_22) = [], pi(U72^#) = [1, 2], pi(c_23) = [], pi(U81^#) = [2, 3], pi(c_24) = [], pi(U82^#) = [2, 3], pi(c_25) = [], pi(fst^#) = [1], pi(c_26) = [], pi(c_27) = [], pi(c_28) = [], pi(sel^#) = [], pi(c_29) = [], pi(c_30) = [], pi(tail^#) = [1], pi(c_31) = [], pi(take^#) = [], pi(c_32) = [], pi(c) = [], pi(c_1) = [1, 2, 3], pi(c_2) = [1, 2, 3], pi(c_3) = [1], pi(c_4) = [1], pi(c_5) = [1], pi(c_6) = [1, 2], pi(c_7) = [1, 2], pi(c_8) = [1], pi(c_9) = [1, 2], pi(c_10) = [1], pi(c_11) = [1, 2, 3], pi(c_12) = [1, 2, 3, 4], pi(c_13) = [1], pi(c_14) = [1], pi(c_15) = [1], pi(c_16) = [1, 2, 3, 4], pi(c_17) = [1, 2, 3, 4], pi(c_18) = [1, 2, 3, 4], pi(c_19) = [1], pi(c_20) = [1, 2], pi(c_21) = [1], pi(c_22) = [1, 2, 3], pi(c_23) = [1, 2, 3], pi(c_24) = [1], pi(c_25) = [], pi(c_26) = [1, 2], pi(c_27) = [] Usable defined function symbols are a subset of: {U11, U12, activate, snd, splitAt, afterNth, U51, U52, natsFrom, s, U11^#, U12^#, activate^#, snd^#, splitAt^#, natsFrom^#, s^#, U51^#, U21^#, U22^#, U31^#, U32^#, U41^#, U42^#, head^#, afterNth^#, U52^#, U61^#, U62^#, U63^#, U64^#, U71^#, U72^#, U81^#, U82^#, fst^#, sel^#, tail^#, take^#} For your convenience, here are the satisfied ordering constraints: pi(U11^#(tt(), N, XS)) = U11^#(N, XS;) > c_1(U12^#(activate(N;), activate(XS;);), activate^#(N;), activate^#(XS;);) = pi(c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS))) pi(U12^#(tt(), N, XS)) = U12^#(N, XS;) > c_2(snd^#(splitAt(activate(XS;););), activate^#(N;), activate^#(XS;);) = pi(c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS))) pi(activate^#(n__natsFrom(X))) = activate^#(n__natsFrom(; X);) > c_3(activate^#(X;);) = pi(c_3(activate^#(X))) pi(activate^#(n__s(X))) = activate^#(n__s(; X);) > c_4(activate^#(X;);) = pi(c_4(activate^#(X))) pi(snd^#(pair(X, Y))) = snd^#(pair(; X, Y);) > c_5(U51^#(Y;);) = pi(c_5(U51^#(tt(), Y))) pi(U51^#(tt(), Y)) = U51^#(Y;) > c_6(U52^#(activate(Y;); tt()), activate^#(Y;);) = pi(c_6(U52^#(tt(), activate(Y)), activate^#(Y))) pi(U21^#(tt(), X)) = U21^#(X;) > c_7(U22^#(activate(X;);), activate^#(X;);) = pi(c_7(U22^#(tt(), activate(X)), activate^#(X))) pi(U22^#(tt(), X)) = U22^#(X;) > c_8(activate^#(X;);) = pi(c_8(activate^#(X))) pi(U31^#(tt(), N)) = U31^#(N;) > c_9(U32^#(activate(N;); tt()), activate^#(N;);) = pi(c_9(U32^#(tt(), activate(N)), activate^#(N))) pi(U32^#(tt(), N)) = U32^#(N; tt()) > c_10(activate^#(N;);) = pi(c_10(activate^#(N))) pi(U41^#(tt(), N, XS)) = U41^#(N, XS;) > c_11(U42^#(tt(), activate(N;), activate(XS;);), activate^#(N;), activate^#(XS;);) = pi(c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS))) pi(U42^#(tt(), N, XS)) = U42^#(tt(), N, XS;) > c_12(head^#(afterNth(activate(XS;););), afterNth^#(activate(N;), activate(XS;);), activate^#(N;), activate^#(XS;);) = pi(c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS))) pi(head^#(cons(N, XS))) = head^#(cons(; N, XS);) > c_13(U31^#(N;);) = pi(c_13(U31^#(tt(), N))) pi(afterNth^#(N, XS)) = afterNth^#(N, XS;) > c_14(U11^#(N, XS;);) = pi(c_14(U11^#(tt(), N, XS))) pi(U52^#(tt(), Y)) = U52^#(Y; tt()) > c_15(activate^#(Y;);) = pi(c_15(activate^#(Y))) pi(U61^#(tt(), N, X, XS)) = U61^#(N, X, XS;) > c_16(U62^#(activate(N;), activate(X;), activate(XS;);), activate^#(N;), activate^#(X;), activate^#(XS;);) = pi(c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS))) pi(U62^#(tt(), N, X, XS)) = U62^#(N, X, XS;) > c_17(U63^#(activate(N;), activate(X;), activate(XS;);), activate^#(N;), activate^#(X;), activate^#(XS;);) = pi(c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS))) pi(U63^#(tt(), N, X, XS)) = U63^#(N, X, XS;) > c_18(U64^#(splitAt(activate(XS;);), activate(X;);), activate^#(N;), activate^#(XS;), activate^#(X;);) = pi(c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X))) pi(U64^#(pair(YS, ZS), X)) = U64^#(pair(; YS, ZS), X;) > c_19(activate^#(X;);) = pi(c_19(activate^#(X))) pi(U71^#(tt(), XS)) = U71^#(XS;) > c_20(U72^#(activate(XS;); tt()), activate^#(XS;);) = pi(c_20(U72^#(tt(), activate(XS)), activate^#(XS))) pi(U72^#(tt(), XS)) = U72^#(XS; tt()) > c_21(activate^#(XS;);) = pi(c_21(activate^#(XS))) pi(U81^#(tt(), N, XS)) = U81^#(N, XS;) > c_22(U82^#(activate(N;), activate(XS;);), activate^#(N;), activate^#(XS;);) = pi(c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS))) pi(U82^#(tt(), N, XS)) = U82^#(N, XS;) > c_23(fst^#(splitAt(activate(XS;););), activate^#(N;), activate^#(XS;);) = pi(c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS))) pi(fst^#(pair(X, Y))) = fst^#(pair(; X, Y);) > c_24(U21^#(X;);) = pi(c_24(U21^#(tt(), X))) pi(tail^#(cons(N, XS))) = tail^#(cons(; N, XS);) > c_26(U71^#(activate(XS;);), activate^#(XS;);) = pi(c_26(U71^#(tt(), activate(XS)), activate^#(XS))) pi(U11(tt(), N, XS)) = U11(XS;) > U12(activate(XS;);) = pi(U12(tt(), activate(N), activate(XS))) pi(U12(tt(), N, XS)) = U12(XS;) > snd(splitAt(activate(XS;););) = pi(snd(splitAt(activate(N), activate(XS)))) pi(activate(X)) = activate(X;) > X = pi(X) pi(activate(n__natsFrom(X))) = activate(n__natsFrom(; X);) > natsFrom(; activate(X;)) = pi(natsFrom(activate(X))) pi(activate(n__s(X))) = activate(n__s(; X);) > s(; activate(X;)) = pi(s(activate(X))) pi(snd(pair(X, Y))) = snd(pair(; X, Y);) > U51(Y;) = pi(U51(tt(), Y)) pi(splitAt(0(), XS)) = splitAt(XS;) > pair(; nil(), XS) = pi(pair(nil(), XS)) pi(afterNth(N, XS)) = afterNth(XS;) >= U11(XS;) = pi(U11(tt(), N, XS)) pi(U51(tt(), Y)) = U51(Y;) > U52(activate(Y;);) = pi(U52(tt(), activate(Y))) pi(U52(tt(), Y)) = U52(Y;) > activate(Y;) = pi(activate(Y)) pi(natsFrom(N)) = natsFrom(; N) > cons(; N, n__natsFrom(; n__s(; N))) = pi(cons(N, n__natsFrom(n__s(N)))) pi(natsFrom(X)) = natsFrom(; X) > n__natsFrom(; X) = pi(n__natsFrom(X)) pi(s(X)) = s(; X) > n__s(; X) = pi(n__s(X)) S) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) } Weak DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {1} by applications of Pre({1}) = {2}. 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: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , 3: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 4: activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , 5: activate^#(n__s(X)) -> c_4(activate^#(X)) , 6: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , 7: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , 8: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , 9: U22^#(tt(), X) -> c_8(activate^#(X)) , 10: U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , 11: U32^#(tt(), N) -> c_10(activate^#(N)) , 12: U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 13: U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 14: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , 15: U52^#(tt(), Y) -> c_15(activate^#(Y)) , 16: U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 17: U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 18: U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , 19: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , 20: U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , 21: U72^#(tt(), XS) -> c_21(activate^#(XS)) , 22: U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 23: U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 24: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , 25: tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) } Weak 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))), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(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)), activate^#(N), activate^#(XS)) , U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) } Weak DPs: { U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), 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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { afterNth^#(N, XS) -> c_1() } Weak DPs: { U41^#(tt(), N, XS) -> c_2(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_3(afterNth^#(activate(N), 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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We replace rewrite rules by usable rules: Weak Usable Rules: { activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { afterNth^#(N, XS) -> c_1() } Weak DPs: { U41^#(tt(), N, XS) -> c_2(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_3(afterNth^#(activate(N), activate(XS))) } Weak Trs: { activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The dependency graph contains no loops, we remove all dependency pairs. 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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(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: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) } Weak DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {5,7,9,13,15} by applications of Pre({5,7,9,13,15}) = {3,4,6,12,14}. Here rules are labeled as follows: DPs: { 1: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 2: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , 3: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , 4: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , 5: U22^#(tt(), X) -> c_8(activate^#(X)) , 6: U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , 7: U32^#(tt(), N) -> c_10(activate^#(N)) , 8: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , 9: U52^#(tt(), Y) -> c_15(activate^#(Y)) , 10: U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 11: U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 12: U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , 13: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , 14: U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , 15: U72^#(tt(), XS) -> c_21(activate^#(XS)) , 16: U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 17: U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 18: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , 19: tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) , 20: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 21: activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , 22: activate^#(n__s(X)) -> c_4(activate^#(X)) , 23: U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 24: U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 25: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) } Weak DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U72^#(tt(), XS) -> c_21(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {3,4,5,9,10} by applications of Pre({3,4,5,9,10}) = {2,6,8,13,14}. Here rules are labeled as follows: DPs: { 1: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 2: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , 3: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , 4: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , 5: U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , 6: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , 7: U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 8: U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 9: U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , 10: U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , 11: U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 12: U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 13: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , 14: tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) , 15: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 16: activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , 17: activate^#(n__s(X)) -> c_4(activate^#(X)) , 18: U22^#(tt(), X) -> c_8(activate^#(X)) , 19: U32^#(tt(), N) -> c_10(activate^#(N)) , 20: U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 21: U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 22: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , 23: U52^#(tt(), Y) -> c_15(activate^#(Y)) , 24: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , 25: U72^#(tt(), XS) -> c_21(activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) } Weak DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {2,5,8,9} by applications of Pre({2,5,8,9}) = {1,4,7}. Here rules are labeled as follows: DPs: { 1: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 2: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , 3: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , 4: U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 5: U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 6: U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 7: U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 8: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , 9: tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) , 10: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 11: activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , 12: activate^#(n__s(X)) -> c_4(activate^#(X)) , 13: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , 14: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , 15: U22^#(tt(), X) -> c_8(activate^#(X)) , 16: U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , 17: U32^#(tt(), N) -> c_10(activate^#(N)) , 18: U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 19: U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 20: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , 21: U52^#(tt(), Y) -> c_15(activate^#(Y)) , 22: U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , 23: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , 24: U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , 25: U72^#(tt(), XS) -> c_21(activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) } Weak DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {3,5} by applications of Pre({3,5}) = {4}. Here rules are labeled as follows: DPs: { 1: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 2: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , 3: U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 4: U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 5: U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 6: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 7: activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , 8: activate^#(n__s(X)) -> c_4(activate^#(X)) , 9: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , 10: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , 11: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , 12: U22^#(tt(), X) -> c_8(activate^#(X)) , 13: U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , 14: U32^#(tt(), N) -> c_10(activate^#(N)) , 15: U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 16: U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 17: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , 18: U52^#(tt(), Y) -> c_15(activate^#(Y)) , 19: U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 20: U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , 21: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , 22: U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , 23: U72^#(tt(), XS) -> c_21(activate^#(XS)) , 24: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , 25: tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) } Weak DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We estimate the number of application of {3} by applications of Pre({3}) = {}. Here rules are labeled as follows: DPs: { 1: U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 2: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) , 3: U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 4: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 5: activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , 6: activate^#(n__s(X)) -> c_4(activate^#(X)) , 7: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , 8: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , 9: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , 10: U22^#(tt(), X) -> c_8(activate^#(X)) , 11: U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , 12: U32^#(tt(), N) -> c_10(activate^#(N)) , 13: U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 14: U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , 15: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , 16: U52^#(tt(), Y) -> c_15(activate^#(Y)) , 17: U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 18: U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , 19: U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , 20: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , 21: U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , 22: U72^#(tt(), XS) -> c_21(activate^#(XS)) , 23: U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , 24: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , 25: tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) } Weak DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(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. { activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) , activate^#(n__s(X)) -> c_4(activate^#(X)) , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) , U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y)) , U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X)) , U22^#(tt(), X) -> c_8(activate^#(X)) , U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N)) , U32^#(tt(), N) -> c_10(activate^#(N)) , U52^#(tt(), Y) -> c_15(activate^#(Y)) , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), activate(N), activate(X), activate(XS)), activate^#(N), activate^#(X), activate^#(XS)) , U63^#(tt(), N, X, XS) -> c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)), activate^#(N), activate^#(XS), activate^#(X)) , U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) , U71^#(tt(), XS) -> c_20(U72^#(tt(), activate(XS)), activate^#(XS)) , U72^#(tt(), XS) -> c_21(activate^#(XS)) , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U82^#(tt(), N, XS) -> c_23(fst^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) , tail^#(cons(N, XS)) -> c_26(U71^#(tt(), activate(XS)), activate^#(XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U12^#(tt(), N, XS) -> c_2(snd^#(splitAt(activate(N), activate(XS))), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) } Weak DPs: { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , afterNth^#(N, XS) -> c_14(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(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))), activate^#(N), activate^#(XS)) , U41^#(tt(), N, XS) -> c_11(U42^#(tt(), activate(N), activate(XS)), activate^#(N), activate^#(XS)) , U42^#(tt(), N, XS) -> c_12(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS)), activate^#(N), activate^#(XS)) , head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U12^#(tt(), N, XS) -> c_1() , head^#(cons(N, XS)) -> c_2() } Weak DPs: { U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS))) , U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_5(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS))) , afterNth^#(N, XS) -> c_6(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(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: { U12^#(tt(), N, XS) -> c_1() } Weak DPs: { U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS))) , U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_5(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS))) , head^#(cons(N, XS)) -> c_2() , afterNth^#(N, XS) -> c_6(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__s 0 nil Strategy: innermost Problem (S): ------------ Strict DPs: { head^#(cons(N, XS)) -> c_2() } Weak DPs: { U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_1() , U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_5(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS))) , afterNth^#(N, XS) -> c_6(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__s 0 nil Strategy: innermost Overall, the transformation results in the following sub-problem(s): Generated new problems: ----------------------- R) Strict DPs: { U12^#(tt(), N, XS) -> c_1() } Weak DPs: { U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS))) , U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_5(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS))) , head^#(cons(N, XS)) -> c_2() , afterNth^#(N, XS) -> c_6(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__s 0 nil Strategy: innermost This problem was proven YES(O(1),O(1)). S) Strict DPs: { head^#(cons(N, XS)) -> c_2() } Weak DPs: { U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_1() , U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_5(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS))) , afterNth^#(N, XS) -> c_6(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } StartTerms: basic terms Defined Symbols: U11^# U12^# activate^# snd^# splitAt^# natsFrom^# s^# U51^# U21^# U22^# U31^# U32^# U41^# U42^# head^# afterNth^# U52^# U61^# U62^# U63^# U64^# U71^# U72^# U81^# U82^# fst^# sel^# tail^# take^# Constructors: tt pair cons n__natsFrom n__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(1)). Strict DPs: { U12^#(tt(), N, XS) -> c_1() } Weak DPs: { U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS))) , U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_5(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS))) , head^#(cons(N, XS)) -> c_2() , afterNth^#(N, XS) -> c_6(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(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. { head^#(cons(N, XS)) -> c_2() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U12^#(tt(), N, XS) -> c_1() } Weak DPs: { U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS))) , U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_5(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS))) , afterNth^#(N, XS) -> c_6(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { U42^#(tt(), N, XS) -> c_5(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U12^#(tt(), N, XS) -> c_1() } Weak DPs: { U11^#(tt(), N, XS) -> c_2(U12^#(tt(), activate(N), activate(XS))) , U41^#(tt(), N, XS) -> c_3(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_4(afterNth^#(activate(N), activate(XS))) , afterNth^#(N, XS) -> c_5(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) We replace rewrite rules by usable rules: Weak Usable Rules: { activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { U12^#(tt(), N, XS) -> c_1() } Weak DPs: { U11^#(tt(), N, XS) -> c_2(U12^#(tt(), activate(N), activate(XS))) , U41^#(tt(), N, XS) -> c_3(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_4(afterNth^#(activate(N), activate(XS))) , afterNth^#(N, XS) -> c_5(U11^#(tt(), N, XS)) } Weak Trs: { activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The dependency graph contains no loops, we remove all dependency pairs. 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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(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: { head^#(cons(N, XS)) -> c_2() } Weak DPs: { U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_1() , U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_5(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS))) , afterNth^#(N, XS) -> c_6(U11^#(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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(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_3(U12^#(tt(), activate(N), activate(XS))) , U12^#(tt(), N, XS) -> c_1() , afterNth^#(N, XS) -> c_6(U11^#(tt(), N, XS)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { head^#(cons(N, XS)) -> c_2() } Weak DPs: { U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_5(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), 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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { U42^#(tt(), N, XS) -> c_5(head^#(afterNth(activate(N), activate(XS))), afterNth^#(activate(N), activate(XS))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Strict DPs: { head^#(cons(N, XS)) -> c_1() } Weak DPs: { U41^#(tt(), N, XS) -> c_2(U42^#(tt(), activate(N), activate(XS))) , U42^#(tt(), N, XS) -> c_3(head^#(afterNth(activate(N), 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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(X) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The dependency graph contains no loops, we remove all dependency pairs. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). 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(activate(X)) , activate(n__s(X)) -> s(activate(X)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(0(), XS) -> pair(nil(), XS) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), activate(Y)) , U52(tt(), Y) -> activate(Y) , natsFrom(N) -> cons(N, n__natsFrom(n__s(N))) , natsFrom(X) -> n__natsFrom(X) , s(X) -> n__s(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),POLY)