YES(O(1),O(n^1)) 566.23/149.18 YES(O(1),O(n^1)) 566.23/149.18 566.23/149.18 We are left with following problem, upon which TcT provides the 566.23/149.18 certificate YES(O(1),O(n^1)). 566.23/149.18 566.23/149.18 Strict Trs: 566.23/149.18 { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) 566.23/149.18 , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 566.23/149.18 , activate(X) -> X 566.23/149.18 , activate(n__natsFrom(X)) -> natsFrom(X) 566.23/149.18 , snd(pair(X, Y)) -> U51(tt(), Y) 566.23/149.18 , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) 566.23/149.18 , splitAt(0(), XS) -> pair(nil(), XS) 566.23/149.18 , U21(tt(), X) -> U22(tt(), activate(X)) 566.23/149.18 , U22(tt(), X) -> activate(X) 566.23/149.18 , U31(tt(), N) -> U32(tt(), activate(N)) 566.23/149.18 , U32(tt(), N) -> activate(N) 566.23/149.18 , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) 566.23/149.18 , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 566.23/149.18 , head(cons(N, XS)) -> U31(tt(), N) 566.23/149.18 , afterNth(N, XS) -> U11(tt(), N, XS) 566.23/149.18 , U51(tt(), Y) -> U52(tt(), activate(Y)) 566.23/149.18 , U52(tt(), Y) -> activate(Y) 566.23/149.18 , U61(tt(), N, X, XS) -> 566.23/149.18 U62(tt(), activate(N), activate(X), activate(XS)) 566.23/149.18 , U62(tt(), N, X, XS) -> 566.23/149.18 U63(tt(), activate(N), activate(X), activate(XS)) 566.23/149.18 , U63(tt(), N, X, XS) -> 566.23/149.18 U64(splitAt(activate(N), activate(XS)), activate(X)) 566.23/149.18 , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 566.23/149.18 , U71(tt(), XS) -> U72(tt(), activate(XS)) 566.23/149.18 , U72(tt(), XS) -> activate(XS) 566.23/149.18 , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) 566.23/149.18 , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 566.23/149.18 , fst(pair(X, Y)) -> U21(tt(), X) 566.23/149.18 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.23/149.18 , natsFrom(X) -> n__natsFrom(X) 566.23/149.18 , sel(N, XS) -> U41(tt(), N, XS) 566.23/149.18 , tail(cons(N, XS)) -> U71(tt(), activate(XS)) 566.23/149.18 , take(N, XS) -> U81(tt(), N, XS) } 566.23/149.18 Obligation: 566.23/149.18 innermost runtime complexity 566.23/149.18 Answer: 566.23/149.18 YES(O(1),O(n^1)) 566.23/149.18 566.23/149.18 We add the following dependency tuples: 566.23/149.18 566.23/149.18 Strict DPs: 566.23/149.18 { U11^#(tt(), N, XS) -> 566.23/149.18 c_1(U12^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U12^#(tt(), N, XS) -> 566.23/149.18 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , activate^#(X) -> c_3() 566.23/149.18 , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.23/149.18 , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.23/149.18 , splitAt^#(s(N), cons(X, XS)) -> 566.23/149.18 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.23/149.18 , splitAt^#(0(), XS) -> c_7() 566.23/149.18 , natsFrom^#(N) -> c_27() 566.23/149.18 , natsFrom^#(X) -> c_28() 566.23/149.18 , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.23/149.18 , U61^#(tt(), N, X, XS) -> 566.23/149.18 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(X), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.23/149.18 , U22^#(tt(), X) -> c_9(activate^#(X)) 566.23/149.18 , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.23/149.18 , U32^#(tt(), N) -> c_11(activate^#(N)) 566.23/149.18 , U41^#(tt(), N, XS) -> 566.23/149.18 c_12(U42^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U42^#(tt(), N, XS) -> 566.23/149.18 c_13(head^#(afterNth(activate(N), activate(XS))), 566.23/149.18 afterNth^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.23/149.18 , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.23/149.18 , U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.23/149.18 , U62^#(tt(), N, X, XS) -> 566.23/149.18 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(X), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U63^#(tt(), N, X, XS) -> 566.23/149.18 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS), 566.23/149.18 activate^#(X)) 566.23/149.18 , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.23/149.18 , U71^#(tt(), XS) -> 566.23/149.18 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.18 , U72^#(tt(), XS) -> c_23(activate^#(XS)) 566.23/149.18 , U81^#(tt(), N, XS) -> 566.23/149.18 c_24(U82^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U82^#(tt(), N, XS) -> 566.23/149.18 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.23/149.18 , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.23/149.18 , tail^#(cons(N, XS)) -> 566.23/149.18 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.18 , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } 566.23/149.18 566.23/149.18 and mark the set of starting terms. 566.23/149.18 566.23/149.18 We are left with following problem, upon which TcT provides the 566.23/149.18 certificate YES(O(1),O(n^1)). 566.23/149.18 566.23/149.18 Strict DPs: 566.23/149.18 { U11^#(tt(), N, XS) -> 566.23/149.18 c_1(U12^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U12^#(tt(), N, XS) -> 566.23/149.18 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , activate^#(X) -> c_3() 566.23/149.18 , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.23/149.18 , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.23/149.18 , splitAt^#(s(N), cons(X, XS)) -> 566.23/149.18 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.23/149.18 , splitAt^#(0(), XS) -> c_7() 566.23/149.18 , natsFrom^#(N) -> c_27() 566.23/149.18 , natsFrom^#(X) -> c_28() 566.23/149.18 , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.23/149.18 , U61^#(tt(), N, X, XS) -> 566.23/149.18 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(X), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.23/149.18 , U22^#(tt(), X) -> c_9(activate^#(X)) 566.23/149.18 , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.23/149.18 , U32^#(tt(), N) -> c_11(activate^#(N)) 566.23/149.18 , U41^#(tt(), N, XS) -> 566.23/149.18 c_12(U42^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U42^#(tt(), N, XS) -> 566.23/149.18 c_13(head^#(afterNth(activate(N), activate(XS))), 566.23/149.18 afterNth^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.23/149.18 , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.23/149.18 , U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.23/149.18 , U62^#(tt(), N, X, XS) -> 566.23/149.18 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(X), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U63^#(tt(), N, X, XS) -> 566.23/149.18 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS), 566.23/149.18 activate^#(X)) 566.23/149.18 , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.23/149.18 , U71^#(tt(), XS) -> 566.23/149.18 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.18 , U72^#(tt(), XS) -> c_23(activate^#(XS)) 566.23/149.18 , U81^#(tt(), N, XS) -> 566.23/149.18 c_24(U82^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U82^#(tt(), N, XS) -> 566.23/149.18 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.23/149.18 , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.23/149.18 , tail^#(cons(N, XS)) -> 566.23/149.18 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.18 , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } 566.23/149.18 Weak Trs: 566.23/149.18 { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) 566.23/149.18 , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 566.23/149.18 , activate(X) -> X 566.23/149.18 , activate(n__natsFrom(X)) -> natsFrom(X) 566.23/149.18 , snd(pair(X, Y)) -> U51(tt(), Y) 566.23/149.18 , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) 566.23/149.18 , splitAt(0(), XS) -> pair(nil(), XS) 566.23/149.18 , U21(tt(), X) -> U22(tt(), activate(X)) 566.23/149.18 , U22(tt(), X) -> activate(X) 566.23/149.18 , U31(tt(), N) -> U32(tt(), activate(N)) 566.23/149.18 , U32(tt(), N) -> activate(N) 566.23/149.18 , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) 566.23/149.18 , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 566.23/149.18 , head(cons(N, XS)) -> U31(tt(), N) 566.23/149.18 , afterNth(N, XS) -> U11(tt(), N, XS) 566.23/149.18 , U51(tt(), Y) -> U52(tt(), activate(Y)) 566.23/149.18 , U52(tt(), Y) -> activate(Y) 566.23/149.18 , U61(tt(), N, X, XS) -> 566.23/149.18 U62(tt(), activate(N), activate(X), activate(XS)) 566.23/149.18 , U62(tt(), N, X, XS) -> 566.23/149.18 U63(tt(), activate(N), activate(X), activate(XS)) 566.23/149.18 , U63(tt(), N, X, XS) -> 566.23/149.18 U64(splitAt(activate(N), activate(XS)), activate(X)) 566.23/149.18 , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 566.23/149.18 , U71(tt(), XS) -> U72(tt(), activate(XS)) 566.23/149.18 , U72(tt(), XS) -> activate(XS) 566.23/149.18 , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) 566.23/149.18 , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 566.23/149.18 , fst(pair(X, Y)) -> U21(tt(), X) 566.23/149.18 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.23/149.18 , natsFrom(X) -> n__natsFrom(X) 566.23/149.18 , sel(N, XS) -> U41(tt(), N, XS) 566.23/149.18 , tail(cons(N, XS)) -> U71(tt(), activate(XS)) 566.23/149.18 , take(N, XS) -> U81(tt(), N, XS) } 566.23/149.18 Obligation: 566.23/149.18 innermost runtime complexity 566.23/149.18 Answer: 566.23/149.18 YES(O(1),O(n^1)) 566.23/149.18 566.23/149.18 We estimate the number of application of {3,7,8,9} by applications 566.23/149.18 of Pre({3,7,8,9}) = 566.23/149.18 {1,2,4,6,10,11,12,13,14,15,16,17,20,21,22,23,24,25,26,27,30}. Here 566.23/149.18 rules are labeled as follows: 566.23/149.18 566.23/149.18 DPs: 566.23/149.18 { 1: U11^#(tt(), N, XS) -> 566.23/149.18 c_1(U12^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , 2: U12^#(tt(), N, XS) -> 566.23/149.18 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , 3: activate^#(X) -> c_3() 566.23/149.18 , 4: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.23/149.18 , 5: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.23/149.18 , 6: splitAt^#(s(N), cons(X, XS)) -> 566.23/149.18 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.23/149.18 , 7: splitAt^#(0(), XS) -> c_7() 566.23/149.18 , 8: natsFrom^#(N) -> c_27() 566.23/149.18 , 9: natsFrom^#(X) -> c_28() 566.23/149.18 , 10: U51^#(tt(), Y) -> 566.23/149.18 c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.23/149.18 , 11: U61^#(tt(), N, X, XS) -> 566.23/149.18 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(X), 566.23/149.18 activate^#(XS)) 566.23/149.18 , 12: U21^#(tt(), X) -> 566.23/149.18 c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.23/149.18 , 13: U22^#(tt(), X) -> c_9(activate^#(X)) 566.23/149.18 , 14: U31^#(tt(), N) -> 566.23/149.18 c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.23/149.18 , 15: U32^#(tt(), N) -> c_11(activate^#(N)) 566.23/149.18 , 16: U41^#(tt(), N, XS) -> 566.23/149.18 c_12(U42^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , 17: U42^#(tt(), N, XS) -> 566.23/149.18 c_13(head^#(afterNth(activate(N), activate(XS))), 566.23/149.18 afterNth^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , 18: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.23/149.18 , 19: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.23/149.18 , 20: U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.23/149.18 , 21: U62^#(tt(), N, X, XS) -> 566.23/149.18 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(X), 566.23/149.18 activate^#(XS)) 566.23/149.18 , 22: U63^#(tt(), N, X, XS) -> 566.23/149.18 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS), 566.23/149.18 activate^#(X)) 566.23/149.18 , 23: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.23/149.18 , 24: U71^#(tt(), XS) -> 566.23/149.18 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.18 , 25: U72^#(tt(), XS) -> c_23(activate^#(XS)) 566.23/149.18 , 26: U81^#(tt(), N, XS) -> 566.23/149.18 c_24(U82^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , 27: U82^#(tt(), N, XS) -> 566.23/149.18 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , 28: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.23/149.18 , 29: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.23/149.18 , 30: tail^#(cons(N, XS)) -> 566.23/149.18 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.18 , 31: take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } 566.23/149.18 566.23/149.18 We are left with following problem, upon which TcT provides the 566.23/149.18 certificate YES(O(1),O(n^1)). 566.23/149.18 566.23/149.18 Strict DPs: 566.23/149.18 { U11^#(tt(), N, XS) -> 566.23/149.18 c_1(U12^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U12^#(tt(), N, XS) -> 566.23/149.18 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.23/149.18 , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.23/149.18 , splitAt^#(s(N), cons(X, XS)) -> 566.23/149.18 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.23/149.18 , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.23/149.18 , U61^#(tt(), N, X, XS) -> 566.23/149.18 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(X), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.23/149.18 , U22^#(tt(), X) -> c_9(activate^#(X)) 566.23/149.18 , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.23/149.18 , U32^#(tt(), N) -> c_11(activate^#(N)) 566.23/149.18 , U41^#(tt(), N, XS) -> 566.23/149.18 c_12(U42^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U42^#(tt(), N, XS) -> 566.23/149.18 c_13(head^#(afterNth(activate(N), activate(XS))), 566.23/149.18 afterNth^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.23/149.18 , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.23/149.18 , U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.23/149.18 , U62^#(tt(), N, X, XS) -> 566.23/149.18 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(X), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U63^#(tt(), N, X, XS) -> 566.23/149.18 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS), 566.23/149.18 activate^#(X)) 566.23/149.18 , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.23/149.18 , U71^#(tt(), XS) -> 566.23/149.18 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.18 , U72^#(tt(), XS) -> c_23(activate^#(XS)) 566.23/149.18 , U81^#(tt(), N, XS) -> 566.23/149.18 c_24(U82^#(tt(), activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , U82^#(tt(), N, XS) -> 566.23/149.18 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.23/149.18 splitAt^#(activate(N), activate(XS)), 566.23/149.18 activate^#(N), 566.23/149.18 activate^#(XS)) 566.23/149.18 , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.23/149.18 , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.23/149.18 , tail^#(cons(N, XS)) -> 566.23/149.18 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.18 , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } 566.23/149.18 Weak DPs: 566.23/149.18 { activate^#(X) -> c_3() 566.23/149.18 , splitAt^#(0(), XS) -> c_7() 566.23/149.18 , natsFrom^#(N) -> c_27() 566.23/149.18 , natsFrom^#(X) -> c_28() } 566.23/149.18 Weak Trs: 566.23/149.18 { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) 566.23/149.18 , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 566.23/149.18 , activate(X) -> X 566.23/149.18 , activate(n__natsFrom(X)) -> natsFrom(X) 566.23/149.18 , snd(pair(X, Y)) -> U51(tt(), Y) 566.23/149.18 , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) 566.23/149.18 , splitAt(0(), XS) -> pair(nil(), XS) 566.23/149.18 , U21(tt(), X) -> U22(tt(), activate(X)) 566.23/149.18 , U22(tt(), X) -> activate(X) 566.23/149.18 , U31(tt(), N) -> U32(tt(), activate(N)) 566.23/149.18 , U32(tt(), N) -> activate(N) 566.23/149.18 , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) 566.23/149.18 , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 566.23/149.18 , head(cons(N, XS)) -> U31(tt(), N) 566.23/149.18 , afterNth(N, XS) -> U11(tt(), N, XS) 566.23/149.18 , U51(tt(), Y) -> U52(tt(), activate(Y)) 566.23/149.18 , U52(tt(), Y) -> activate(Y) 566.23/149.18 , U61(tt(), N, X, XS) -> 566.23/149.18 U62(tt(), activate(N), activate(X), activate(XS)) 566.23/149.18 , U62(tt(), N, X, XS) -> 566.23/149.18 U63(tt(), activate(N), activate(X), activate(XS)) 566.23/149.18 , U63(tt(), N, X, XS) -> 566.23/149.18 U64(splitAt(activate(N), activate(XS)), activate(X)) 566.23/149.18 , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 566.23/149.18 , U71(tt(), XS) -> U72(tt(), activate(XS)) 566.23/149.18 , U72(tt(), XS) -> activate(XS) 566.23/149.18 , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) 566.23/149.18 , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 566.23/149.18 , fst(pair(X, Y)) -> U21(tt(), X) 566.23/149.18 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.23/149.18 , natsFrom(X) -> n__natsFrom(X) 566.23/149.18 , sel(N, XS) -> U41(tt(), N, XS) 566.23/149.18 , tail(cons(N, XS)) -> U71(tt(), activate(XS)) 566.23/149.18 , take(N, XS) -> U81(tt(), N, XS) } 566.23/149.18 Obligation: 566.23/149.18 innermost runtime complexity 566.23/149.18 Answer: 566.23/149.18 YES(O(1),O(n^1)) 566.23/149.18 566.23/149.18 We estimate the number of application of {3} by applications of 566.23/149.18 Pre({3}) = {1,2,5,6,7,8,9,10,11,12,13,16,17,18,19,20,21,22,23,26}. 566.23/149.18 Here rules are labeled as follows: 566.23/149.18 566.23/149.18 DPs: 566.23/149.18 { 1: U11^#(tt(), N, XS) -> 566.23/149.19 c_1(U12^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 2: U12^#(tt(), N, XS) -> 566.23/149.19 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 3: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.23/149.19 , 4: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.23/149.19 , 5: splitAt^#(s(N), cons(X, XS)) -> 566.23/149.19 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.23/149.19 , 6: U51^#(tt(), Y) -> 566.23/149.19 c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.23/149.19 , 7: U61^#(tt(), N, X, XS) -> 566.23/149.19 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(X), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 8: U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.23/149.19 , 9: U22^#(tt(), X) -> c_9(activate^#(X)) 566.23/149.19 , 10: U31^#(tt(), N) -> 566.23/149.19 c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.23/149.19 , 11: U32^#(tt(), N) -> c_11(activate^#(N)) 566.23/149.19 , 12: U41^#(tt(), N, XS) -> 566.23/149.19 c_12(U42^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 13: U42^#(tt(), N, XS) -> 566.23/149.19 c_13(head^#(afterNth(activate(N), activate(XS))), 566.23/149.19 afterNth^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 14: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.23/149.19 , 15: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.23/149.19 , 16: U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.23/149.19 , 17: U62^#(tt(), N, X, XS) -> 566.23/149.19 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(X), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 18: U63^#(tt(), N, X, XS) -> 566.23/149.19 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS), 566.23/149.19 activate^#(X)) 566.23/149.19 , 19: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.23/149.19 , 20: U71^#(tt(), XS) -> 566.23/149.19 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.19 , 21: U72^#(tt(), XS) -> c_23(activate^#(XS)) 566.23/149.19 , 22: U81^#(tt(), N, XS) -> 566.23/149.19 c_24(U82^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 23: U82^#(tt(), N, XS) -> 566.23/149.19 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 24: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.23/149.19 , 25: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.23/149.19 , 26: tail^#(cons(N, XS)) -> 566.23/149.19 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.19 , 27: take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) 566.23/149.19 , 28: activate^#(X) -> c_3() 566.23/149.19 , 29: splitAt^#(0(), XS) -> c_7() 566.23/149.19 , 30: natsFrom^#(N) -> c_27() 566.23/149.19 , 31: natsFrom^#(X) -> c_28() } 566.23/149.19 566.23/149.19 We are left with following problem, upon which TcT provides the 566.23/149.19 certificate YES(O(1),O(n^1)). 566.23/149.19 566.23/149.19 Strict DPs: 566.23/149.19 { U11^#(tt(), N, XS) -> 566.23/149.19 c_1(U12^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , U12^#(tt(), N, XS) -> 566.23/149.19 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.23/149.19 , splitAt^#(s(N), cons(X, XS)) -> 566.23/149.19 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.23/149.19 , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.23/149.19 , U61^#(tt(), N, X, XS) -> 566.23/149.19 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(X), 566.23/149.19 activate^#(XS)) 566.23/149.19 , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.23/149.19 , U22^#(tt(), X) -> c_9(activate^#(X)) 566.23/149.19 , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.23/149.19 , U32^#(tt(), N) -> c_11(activate^#(N)) 566.23/149.19 , U41^#(tt(), N, XS) -> 566.23/149.19 c_12(U42^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , U42^#(tt(), N, XS) -> 566.23/149.19 c_13(head^#(afterNth(activate(N), activate(XS))), 566.23/149.19 afterNth^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.23/149.19 , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.23/149.19 , U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.23/149.19 , U62^#(tt(), N, X, XS) -> 566.23/149.19 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(X), 566.23/149.19 activate^#(XS)) 566.23/149.19 , U63^#(tt(), N, X, XS) -> 566.23/149.19 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS), 566.23/149.19 activate^#(X)) 566.23/149.19 , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.23/149.19 , U71^#(tt(), XS) -> 566.23/149.19 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.19 , U72^#(tt(), XS) -> c_23(activate^#(XS)) 566.23/149.19 , U81^#(tt(), N, XS) -> 566.23/149.19 c_24(U82^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , U82^#(tt(), N, XS) -> 566.23/149.19 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.23/149.19 , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.23/149.19 , tail^#(cons(N, XS)) -> 566.23/149.19 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.19 , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } 566.23/149.19 Weak DPs: 566.23/149.19 { activate^#(X) -> c_3() 566.23/149.19 , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.23/149.19 , splitAt^#(0(), XS) -> c_7() 566.23/149.19 , natsFrom^#(N) -> c_27() 566.23/149.19 , natsFrom^#(X) -> c_28() } 566.23/149.19 Weak Trs: 566.23/149.19 { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) 566.23/149.19 , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 566.23/149.19 , activate(X) -> X 566.23/149.19 , activate(n__natsFrom(X)) -> natsFrom(X) 566.23/149.19 , snd(pair(X, Y)) -> U51(tt(), Y) 566.23/149.19 , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) 566.23/149.19 , splitAt(0(), XS) -> pair(nil(), XS) 566.23/149.19 , U21(tt(), X) -> U22(tt(), activate(X)) 566.23/149.19 , U22(tt(), X) -> activate(X) 566.23/149.19 , U31(tt(), N) -> U32(tt(), activate(N)) 566.23/149.19 , U32(tt(), N) -> activate(N) 566.23/149.19 , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) 566.23/149.19 , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 566.23/149.19 , head(cons(N, XS)) -> U31(tt(), N) 566.23/149.19 , afterNth(N, XS) -> U11(tt(), N, XS) 566.23/149.19 , U51(tt(), Y) -> U52(tt(), activate(Y)) 566.23/149.19 , U52(tt(), Y) -> activate(Y) 566.23/149.19 , U61(tt(), N, X, XS) -> 566.23/149.19 U62(tt(), activate(N), activate(X), activate(XS)) 566.23/149.19 , U62(tt(), N, X, XS) -> 566.23/149.19 U63(tt(), activate(N), activate(X), activate(XS)) 566.23/149.19 , U63(tt(), N, X, XS) -> 566.23/149.19 U64(splitAt(activate(N), activate(XS)), activate(X)) 566.23/149.19 , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 566.23/149.19 , U71(tt(), XS) -> U72(tt(), activate(XS)) 566.23/149.19 , U72(tt(), XS) -> activate(XS) 566.23/149.19 , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) 566.23/149.19 , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 566.23/149.19 , fst(pair(X, Y)) -> U21(tt(), X) 566.23/149.19 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.23/149.19 , natsFrom(X) -> n__natsFrom(X) 566.23/149.19 , sel(N, XS) -> U41(tt(), N, XS) 566.23/149.19 , tail(cons(N, XS)) -> U71(tt(), activate(XS)) 566.23/149.19 , take(N, XS) -> U81(tt(), N, XS) } 566.23/149.19 Obligation: 566.23/149.19 innermost runtime complexity 566.23/149.19 Answer: 566.23/149.19 YES(O(1),O(n^1)) 566.23/149.19 566.23/149.19 We estimate the number of application of {8,10,15,18,20} by 566.23/149.19 applications of Pre({8,10,15,18,20}) = {5,7,9,17,19}. Here rules 566.23/149.19 are labeled as follows: 566.23/149.19 566.23/149.19 DPs: 566.23/149.19 { 1: U11^#(tt(), N, XS) -> 566.23/149.19 c_1(U12^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 2: U12^#(tt(), N, XS) -> 566.23/149.19 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 3: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.23/149.19 , 4: splitAt^#(s(N), cons(X, XS)) -> 566.23/149.19 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.23/149.19 , 5: U51^#(tt(), Y) -> 566.23/149.19 c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.23/149.19 , 6: U61^#(tt(), N, X, XS) -> 566.23/149.19 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(X), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 7: U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.23/149.19 , 8: U22^#(tt(), X) -> c_9(activate^#(X)) 566.23/149.19 , 9: U31^#(tt(), N) -> 566.23/149.19 c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.23/149.19 , 10: U32^#(tt(), N) -> c_11(activate^#(N)) 566.23/149.19 , 11: U41^#(tt(), N, XS) -> 566.23/149.19 c_12(U42^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 12: U42^#(tt(), N, XS) -> 566.23/149.19 c_13(head^#(afterNth(activate(N), activate(XS))), 566.23/149.19 afterNth^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 13: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.23/149.19 , 14: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.23/149.19 , 15: U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.23/149.19 , 16: U62^#(tt(), N, X, XS) -> 566.23/149.19 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(X), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 17: U63^#(tt(), N, X, XS) -> 566.23/149.19 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS), 566.23/149.19 activate^#(X)) 566.23/149.19 , 18: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.23/149.19 , 19: U71^#(tt(), XS) -> 566.23/149.19 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.19 , 20: U72^#(tt(), XS) -> c_23(activate^#(XS)) 566.23/149.19 , 21: U81^#(tt(), N, XS) -> 566.23/149.19 c_24(U82^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 22: U82^#(tt(), N, XS) -> 566.23/149.19 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 23: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.23/149.19 , 24: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.23/149.19 , 25: tail^#(cons(N, XS)) -> 566.23/149.19 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.19 , 26: take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) 566.23/149.19 , 27: activate^#(X) -> c_3() 566.23/149.19 , 28: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.23/149.19 , 29: splitAt^#(0(), XS) -> c_7() 566.23/149.19 , 30: natsFrom^#(N) -> c_27() 566.23/149.19 , 31: natsFrom^#(X) -> c_28() } 566.23/149.19 566.23/149.19 We are left with following problem, upon which TcT provides the 566.23/149.19 certificate YES(O(1),O(n^1)). 566.23/149.19 566.23/149.19 Strict DPs: 566.23/149.19 { U11^#(tt(), N, XS) -> 566.23/149.19 c_1(U12^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , U12^#(tt(), N, XS) -> 566.23/149.19 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.23/149.19 , splitAt^#(s(N), cons(X, XS)) -> 566.23/149.19 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.23/149.19 , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.23/149.19 , U61^#(tt(), N, X, XS) -> 566.23/149.19 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(X), 566.23/149.19 activate^#(XS)) 566.23/149.19 , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.23/149.19 , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.23/149.19 , U41^#(tt(), N, XS) -> 566.23/149.19 c_12(U42^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , U42^#(tt(), N, XS) -> 566.23/149.19 c_13(head^#(afterNth(activate(N), activate(XS))), 566.23/149.19 afterNth^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.23/149.19 , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.23/149.19 , U62^#(tt(), N, X, XS) -> 566.23/149.19 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(X), 566.23/149.19 activate^#(XS)) 566.23/149.19 , U63^#(tt(), N, X, XS) -> 566.23/149.19 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS), 566.23/149.19 activate^#(X)) 566.23/149.19 , U71^#(tt(), XS) -> 566.23/149.19 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.19 , U81^#(tt(), N, XS) -> 566.23/149.19 c_24(U82^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , U82^#(tt(), N, XS) -> 566.23/149.19 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.23/149.19 , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.23/149.19 , tail^#(cons(N, XS)) -> 566.23/149.19 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) 566.23/149.19 , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } 566.23/149.19 Weak DPs: 566.23/149.19 { activate^#(X) -> c_3() 566.23/149.19 , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.23/149.19 , splitAt^#(0(), XS) -> c_7() 566.23/149.19 , natsFrom^#(N) -> c_27() 566.23/149.19 , natsFrom^#(X) -> c_28() 566.23/149.19 , U22^#(tt(), X) -> c_9(activate^#(X)) 566.23/149.19 , U32^#(tt(), N) -> c_11(activate^#(N)) 566.23/149.19 , U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.23/149.19 , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.23/149.19 , U72^#(tt(), XS) -> c_23(activate^#(XS)) } 566.23/149.19 Weak Trs: 566.23/149.19 { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) 566.23/149.19 , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 566.23/149.19 , activate(X) -> X 566.23/149.19 , activate(n__natsFrom(X)) -> natsFrom(X) 566.23/149.19 , snd(pair(X, Y)) -> U51(tt(), Y) 566.23/149.19 , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) 566.23/149.19 , splitAt(0(), XS) -> pair(nil(), XS) 566.23/149.19 , U21(tt(), X) -> U22(tt(), activate(X)) 566.23/149.19 , U22(tt(), X) -> activate(X) 566.23/149.19 , U31(tt(), N) -> U32(tt(), activate(N)) 566.23/149.19 , U32(tt(), N) -> activate(N) 566.23/149.19 , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) 566.23/149.19 , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 566.23/149.19 , head(cons(N, XS)) -> U31(tt(), N) 566.23/149.19 , afterNth(N, XS) -> U11(tt(), N, XS) 566.23/149.19 , U51(tt(), Y) -> U52(tt(), activate(Y)) 566.23/149.19 , U52(tt(), Y) -> activate(Y) 566.23/149.19 , U61(tt(), N, X, XS) -> 566.23/149.19 U62(tt(), activate(N), activate(X), activate(XS)) 566.23/149.19 , U62(tt(), N, X, XS) -> 566.23/149.19 U63(tt(), activate(N), activate(X), activate(XS)) 566.23/149.19 , U63(tt(), N, X, XS) -> 566.23/149.19 U64(splitAt(activate(N), activate(XS)), activate(X)) 566.23/149.19 , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 566.23/149.19 , U71(tt(), XS) -> U72(tt(), activate(XS)) 566.23/149.19 , U72(tt(), XS) -> activate(XS) 566.23/149.19 , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) 566.23/149.19 , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 566.23/149.19 , fst(pair(X, Y)) -> U21(tt(), X) 566.23/149.19 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.23/149.19 , natsFrom(X) -> n__natsFrom(X) 566.23/149.19 , sel(N, XS) -> U41(tt(), N, XS) 566.23/149.19 , tail(cons(N, XS)) -> U71(tt(), activate(XS)) 566.23/149.19 , take(N, XS) -> U81(tt(), N, XS) } 566.23/149.19 Obligation: 566.23/149.19 innermost runtime complexity 566.23/149.19 Answer: 566.23/149.19 YES(O(1),O(n^1)) 566.23/149.19 566.23/149.19 We estimate the number of application of {5,7,8,15} by applications 566.23/149.19 of Pre({5,7,8,15}) = {3,11,18,20}. Here rules are labeled as 566.23/149.19 follows: 566.23/149.19 566.23/149.19 DPs: 566.23/149.19 { 1: U11^#(tt(), N, XS) -> 566.23/149.19 c_1(U12^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 2: U12^#(tt(), N, XS) -> 566.23/149.19 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.23/149.19 splitAt^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 3: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.23/149.19 , 4: splitAt^#(s(N), cons(X, XS)) -> 566.23/149.19 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.23/149.19 , 5: U51^#(tt(), Y) -> 566.23/149.19 c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.23/149.19 , 6: U61^#(tt(), N, X, XS) -> 566.23/149.19 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(X), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 7: U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.23/149.19 , 8: U31^#(tt(), N) -> 566.23/149.19 c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.23/149.19 , 9: U41^#(tt(), N, XS) -> 566.23/149.19 c_12(U42^#(tt(), activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 10: U42^#(tt(), N, XS) -> 566.23/149.19 c_13(head^#(afterNth(activate(N), activate(XS))), 566.23/149.19 afterNth^#(activate(N), activate(XS)), 566.23/149.19 activate^#(N), 566.23/149.19 activate^#(XS)) 566.23/149.19 , 11: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.23/149.19 , 12: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.23/149.19 , 13: U62^#(tt(), N, X, XS) -> 566.23/149.19 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(X), 566.59/149.20 activate^#(XS)) 566.59/149.20 , 14: U63^#(tt(), N, X, XS) -> 566.59/149.20 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS), 566.59/149.20 activate^#(X)) 566.59/149.20 , 15: U71^#(tt(), XS) -> 566.59/149.20 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.59/149.20 , 16: U81^#(tt(), N, XS) -> 566.59/149.20 c_24(U82^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , 17: U82^#(tt(), N, XS) -> 566.59/149.20 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , 18: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.59/149.20 , 19: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.59/149.20 , 20: tail^#(cons(N, XS)) -> 566.59/149.20 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) 566.59/149.20 , 21: take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) 566.59/149.20 , 22: activate^#(X) -> c_3() 566.59/149.20 , 23: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.59/149.20 , 24: splitAt^#(0(), XS) -> c_7() 566.59/149.20 , 25: natsFrom^#(N) -> c_27() 566.59/149.20 , 26: natsFrom^#(X) -> c_28() 566.59/149.20 , 27: U22^#(tt(), X) -> c_9(activate^#(X)) 566.59/149.20 , 28: U32^#(tt(), N) -> c_11(activate^#(N)) 566.59/149.20 , 29: U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.59/149.20 , 30: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.59/149.20 , 31: U72^#(tt(), XS) -> c_23(activate^#(XS)) } 566.59/149.20 566.59/149.20 We are left with following problem, upon which TcT provides the 566.59/149.20 certificate YES(O(1),O(n^1)). 566.59/149.20 566.59/149.20 Strict DPs: 566.59/149.20 { U11^#(tt(), N, XS) -> 566.59/149.20 c_1(U12^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U12^#(tt(), N, XS) -> 566.59/149.20 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.59/149.20 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.20 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.59/149.20 , U61^#(tt(), N, X, XS) -> 566.59/149.20 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(X), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U41^#(tt(), N, XS) -> 566.59/149.20 c_12(U42^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U42^#(tt(), N, XS) -> 566.59/149.20 c_13(head^#(afterNth(activate(N), activate(XS))), 566.59/149.20 afterNth^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.59/149.20 , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.59/149.20 , U62^#(tt(), N, X, XS) -> 566.59/149.20 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(X), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U63^#(tt(), N, X, XS) -> 566.59/149.20 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS), 566.59/149.20 activate^#(X)) 566.59/149.20 , U81^#(tt(), N, XS) -> 566.59/149.20 c_24(U82^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U82^#(tt(), N, XS) -> 566.59/149.20 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.59/149.20 , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.59/149.20 , tail^#(cons(N, XS)) -> 566.59/149.20 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) 566.59/149.20 , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } 566.59/149.20 Weak DPs: 566.59/149.20 { activate^#(X) -> c_3() 566.59/149.20 , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.59/149.20 , splitAt^#(0(), XS) -> c_7() 566.59/149.20 , natsFrom^#(N) -> c_27() 566.59/149.20 , natsFrom^#(X) -> c_28() 566.59/149.20 , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.59/149.20 , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.59/149.20 , U22^#(tt(), X) -> c_9(activate^#(X)) 566.59/149.20 , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.59/149.20 , U32^#(tt(), N) -> c_11(activate^#(N)) 566.59/149.20 , U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.59/149.20 , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.59/149.20 , U71^#(tt(), XS) -> 566.59/149.20 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.59/149.20 , U72^#(tt(), XS) -> c_23(activate^#(XS)) } 566.59/149.20 Weak Trs: 566.59/149.20 { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) 566.59/149.20 , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 566.59/149.20 , activate(X) -> X 566.59/149.20 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.20 , snd(pair(X, Y)) -> U51(tt(), Y) 566.59/149.20 , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) 566.59/149.20 , splitAt(0(), XS) -> pair(nil(), XS) 566.59/149.20 , U21(tt(), X) -> U22(tt(), activate(X)) 566.59/149.20 , U22(tt(), X) -> activate(X) 566.59/149.20 , U31(tt(), N) -> U32(tt(), activate(N)) 566.59/149.20 , U32(tt(), N) -> activate(N) 566.59/149.20 , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) 566.59/149.20 , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 566.59/149.20 , head(cons(N, XS)) -> U31(tt(), N) 566.59/149.20 , afterNth(N, XS) -> U11(tt(), N, XS) 566.59/149.20 , U51(tt(), Y) -> U52(tt(), activate(Y)) 566.59/149.20 , U52(tt(), Y) -> activate(Y) 566.59/149.20 , U61(tt(), N, X, XS) -> 566.59/149.20 U62(tt(), activate(N), activate(X), activate(XS)) 566.59/149.20 , U62(tt(), N, X, XS) -> 566.59/149.20 U63(tt(), activate(N), activate(X), activate(XS)) 566.59/149.20 , U63(tt(), N, X, XS) -> 566.59/149.20 U64(splitAt(activate(N), activate(XS)), activate(X)) 566.59/149.20 , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 566.59/149.20 , U71(tt(), XS) -> U72(tt(), activate(XS)) 566.59/149.20 , U72(tt(), XS) -> activate(XS) 566.59/149.20 , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) 566.59/149.20 , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 566.59/149.20 , fst(pair(X, Y)) -> U21(tt(), X) 566.59/149.20 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.20 , natsFrom(X) -> n__natsFrom(X) 566.59/149.20 , sel(N, XS) -> U41(tt(), N, XS) 566.59/149.20 , tail(cons(N, XS)) -> U71(tt(), activate(XS)) 566.59/149.20 , take(N, XS) -> U81(tt(), N, XS) } 566.59/149.20 Obligation: 566.59/149.20 innermost runtime complexity 566.59/149.20 Answer: 566.59/149.20 YES(O(1),O(n^1)) 566.59/149.20 566.59/149.20 We estimate the number of application of {3,8,14,16} by 566.59/149.20 applications of Pre({3,8,14,16}) = {2,7,13}. Here rules are labeled 566.59/149.20 as follows: 566.59/149.20 566.59/149.20 DPs: 566.59/149.20 { 1: U11^#(tt(), N, XS) -> 566.59/149.20 c_1(U12^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , 2: U12^#(tt(), N, XS) -> 566.59/149.20 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , 3: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.59/149.20 , 4: splitAt^#(s(N), cons(X, XS)) -> 566.59/149.20 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.59/149.20 , 5: U61^#(tt(), N, X, XS) -> 566.59/149.20 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(X), 566.59/149.20 activate^#(XS)) 566.59/149.20 , 6: U41^#(tt(), N, XS) -> 566.59/149.20 c_12(U42^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , 7: U42^#(tt(), N, XS) -> 566.59/149.20 c_13(head^#(afterNth(activate(N), activate(XS))), 566.59/149.20 afterNth^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , 8: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.59/149.20 , 9: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.59/149.20 , 10: U62^#(tt(), N, X, XS) -> 566.59/149.20 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(X), 566.59/149.20 activate^#(XS)) 566.59/149.20 , 11: U63^#(tt(), N, X, XS) -> 566.59/149.20 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS), 566.59/149.20 activate^#(X)) 566.59/149.20 , 12: U81^#(tt(), N, XS) -> 566.59/149.20 c_24(U82^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , 13: U82^#(tt(), N, XS) -> 566.59/149.20 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , 14: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.59/149.20 , 15: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.59/149.20 , 16: tail^#(cons(N, XS)) -> 566.59/149.20 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) 566.59/149.20 , 17: take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) 566.59/149.20 , 18: activate^#(X) -> c_3() 566.59/149.20 , 19: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.59/149.20 , 20: splitAt^#(0(), XS) -> c_7() 566.59/149.20 , 21: natsFrom^#(N) -> c_27() 566.59/149.20 , 22: natsFrom^#(X) -> c_28() 566.59/149.20 , 23: U51^#(tt(), Y) -> 566.59/149.20 c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.59/149.20 , 24: U21^#(tt(), X) -> 566.59/149.20 c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.59/149.20 , 25: U22^#(tt(), X) -> c_9(activate^#(X)) 566.59/149.20 , 26: U31^#(tt(), N) -> 566.59/149.20 c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.59/149.20 , 27: U32^#(tt(), N) -> c_11(activate^#(N)) 566.59/149.20 , 28: U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.59/149.20 , 29: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.59/149.20 , 30: U71^#(tt(), XS) -> 566.59/149.20 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.59/149.20 , 31: U72^#(tt(), XS) -> c_23(activate^#(XS)) } 566.59/149.20 566.59/149.20 We are left with following problem, upon which TcT provides the 566.59/149.20 certificate YES(O(1),O(n^1)). 566.59/149.20 566.59/149.20 Strict DPs: 566.59/149.20 { U11^#(tt(), N, XS) -> 566.59/149.20 c_1(U12^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U12^#(tt(), N, XS) -> 566.59/149.20 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.20 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.59/149.20 , U61^#(tt(), N, X, XS) -> 566.59/149.20 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(X), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U41^#(tt(), N, XS) -> 566.59/149.20 c_12(U42^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U42^#(tt(), N, XS) -> 566.59/149.20 c_13(head^#(afterNth(activate(N), activate(XS))), 566.59/149.20 afterNth^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.59/149.20 , U62^#(tt(), N, X, XS) -> 566.59/149.20 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(X), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U63^#(tt(), N, X, XS) -> 566.59/149.20 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS), 566.59/149.20 activate^#(X)) 566.59/149.20 , U81^#(tt(), N, XS) -> 566.59/149.20 c_24(U82^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U82^#(tt(), N, XS) -> 566.59/149.20 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.59/149.20 , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } 566.59/149.20 Weak DPs: 566.59/149.20 { activate^#(X) -> c_3() 566.59/149.20 , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.59/149.20 , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.59/149.20 , splitAt^#(0(), XS) -> c_7() 566.59/149.20 , natsFrom^#(N) -> c_27() 566.59/149.20 , natsFrom^#(X) -> c_28() 566.59/149.20 , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.59/149.20 , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.59/149.20 , U22^#(tt(), X) -> c_9(activate^#(X)) 566.59/149.20 , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.59/149.20 , U32^#(tt(), N) -> c_11(activate^#(N)) 566.59/149.20 , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.59/149.20 , U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.59/149.20 , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.59/149.20 , U71^#(tt(), XS) -> 566.59/149.20 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.59/149.20 , U72^#(tt(), XS) -> c_23(activate^#(XS)) 566.59/149.20 , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.59/149.20 , tail^#(cons(N, XS)) -> 566.59/149.20 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) } 566.59/149.20 Weak Trs: 566.59/149.20 { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) 566.59/149.20 , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 566.59/149.20 , activate(X) -> X 566.59/149.20 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.20 , snd(pair(X, Y)) -> U51(tt(), Y) 566.59/149.20 , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) 566.59/149.20 , splitAt(0(), XS) -> pair(nil(), XS) 566.59/149.20 , U21(tt(), X) -> U22(tt(), activate(X)) 566.59/149.20 , U22(tt(), X) -> activate(X) 566.59/149.20 , U31(tt(), N) -> U32(tt(), activate(N)) 566.59/149.20 , U32(tt(), N) -> activate(N) 566.59/149.20 , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) 566.59/149.20 , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 566.59/149.20 , head(cons(N, XS)) -> U31(tt(), N) 566.59/149.20 , afterNth(N, XS) -> U11(tt(), N, XS) 566.59/149.20 , U51(tt(), Y) -> U52(tt(), activate(Y)) 566.59/149.20 , U52(tt(), Y) -> activate(Y) 566.59/149.20 , U61(tt(), N, X, XS) -> 566.59/149.20 U62(tt(), activate(N), activate(X), activate(XS)) 566.59/149.20 , U62(tt(), N, X, XS) -> 566.59/149.20 U63(tt(), activate(N), activate(X), activate(XS)) 566.59/149.20 , U63(tt(), N, X, XS) -> 566.59/149.20 U64(splitAt(activate(N), activate(XS)), activate(X)) 566.59/149.20 , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 566.59/149.20 , U71(tt(), XS) -> U72(tt(), activate(XS)) 566.59/149.20 , U72(tt(), XS) -> activate(XS) 566.59/149.20 , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) 566.59/149.20 , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 566.59/149.20 , fst(pair(X, Y)) -> U21(tt(), X) 566.59/149.20 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.20 , natsFrom(X) -> n__natsFrom(X) 566.59/149.20 , sel(N, XS) -> U41(tt(), N, XS) 566.59/149.20 , tail(cons(N, XS)) -> U71(tt(), activate(XS)) 566.59/149.20 , take(N, XS) -> U81(tt(), N, XS) } 566.59/149.20 Obligation: 566.59/149.20 innermost runtime complexity 566.59/149.20 Answer: 566.59/149.20 YES(O(1),O(n^1)) 566.59/149.20 566.59/149.20 The following weak DPs constitute a sub-graph of the DG that is 566.59/149.20 closed under successors. The DPs are removed. 566.59/149.20 566.59/149.20 { activate^#(X) -> c_3() 566.59/149.20 , activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X)) 566.59/149.20 , snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) 566.59/149.20 , splitAt^#(0(), XS) -> c_7() 566.59/149.20 , natsFrom^#(N) -> c_27() 566.59/149.20 , natsFrom^#(X) -> c_28() 566.59/149.20 , U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y)) 566.59/149.20 , U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X)) 566.59/149.20 , U22^#(tt(), X) -> c_9(activate^#(X)) 566.59/149.20 , U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N)) 566.59/149.20 , U32^#(tt(), N) -> c_11(activate^#(N)) 566.59/149.20 , head^#(cons(N, XS)) -> c_14(U31^#(tt(), N)) 566.59/149.20 , U52^#(tt(), Y) -> c_17(activate^#(Y)) 566.59/149.20 , U64^#(pair(YS, ZS), X) -> c_21(activate^#(X)) 566.59/149.20 , U71^#(tt(), XS) -> 566.59/149.20 c_22(U72^#(tt(), activate(XS)), activate^#(XS)) 566.59/149.20 , U72^#(tt(), XS) -> c_23(activate^#(XS)) 566.59/149.20 , fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X)) 566.59/149.20 , tail^#(cons(N, XS)) -> 566.59/149.20 c_30(U71^#(tt(), activate(XS)), activate^#(XS)) } 566.59/149.20 566.59/149.20 We are left with following problem, upon which TcT provides the 566.59/149.20 certificate YES(O(1),O(n^1)). 566.59/149.20 566.59/149.20 Strict DPs: 566.59/149.20 { U11^#(tt(), N, XS) -> 566.59/149.20 c_1(U12^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U12^#(tt(), N, XS) -> 566.59/149.20 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.20 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.59/149.20 , U61^#(tt(), N, X, XS) -> 566.59/149.20 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(X), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U41^#(tt(), N, XS) -> 566.59/149.20 c_12(U42^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U42^#(tt(), N, XS) -> 566.59/149.20 c_13(head^#(afterNth(activate(N), activate(XS))), 566.59/149.20 afterNth^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS)) 566.59/149.20 , U62^#(tt(), N, X, XS) -> 566.59/149.20 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(X), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U63^#(tt(), N, X, XS) -> 566.59/149.20 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS), 566.59/149.20 activate^#(X)) 566.59/149.20 , U81^#(tt(), N, XS) -> 566.59/149.20 c_24(U82^#(tt(), activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , U82^#(tt(), N, XS) -> 566.59/149.20 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.59/149.20 splitAt^#(activate(N), activate(XS)), 566.59/149.20 activate^#(N), 566.59/149.20 activate^#(XS)) 566.59/149.20 , sel^#(N, XS) -> c_29(U41^#(tt(), N, XS)) 566.59/149.20 , take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) } 566.59/149.20 Weak Trs: 566.59/149.20 { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) 566.59/149.20 , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 566.59/149.20 , activate(X) -> X 566.59/149.20 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.20 , snd(pair(X, Y)) -> U51(tt(), Y) 566.59/149.20 , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) 566.59/149.20 , splitAt(0(), XS) -> pair(nil(), XS) 566.59/149.21 , U21(tt(), X) -> U22(tt(), activate(X)) 566.59/149.21 , U22(tt(), X) -> activate(X) 566.59/149.21 , U31(tt(), N) -> U32(tt(), activate(N)) 566.59/149.21 , U32(tt(), N) -> activate(N) 566.59/149.21 , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) 566.59/149.21 , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 566.59/149.21 , head(cons(N, XS)) -> U31(tt(), N) 566.59/149.21 , afterNth(N, XS) -> U11(tt(), N, XS) 566.59/149.21 , U51(tt(), Y) -> U52(tt(), activate(Y)) 566.59/149.21 , U52(tt(), Y) -> activate(Y) 566.59/149.21 , U61(tt(), N, X, XS) -> 566.59/149.21 U62(tt(), activate(N), activate(X), activate(XS)) 566.59/149.21 , U62(tt(), N, X, XS) -> 566.59/149.21 U63(tt(), activate(N), activate(X), activate(XS)) 566.59/149.21 , U63(tt(), N, X, XS) -> 566.59/149.21 U64(splitAt(activate(N), activate(XS)), activate(X)) 566.59/149.21 , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 566.59/149.21 , U71(tt(), XS) -> U72(tt(), activate(XS)) 566.59/149.21 , U72(tt(), XS) -> activate(XS) 566.59/149.21 , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) 566.59/149.21 , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 566.59/149.21 , fst(pair(X, Y)) -> U21(tt(), X) 566.59/149.21 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.21 , natsFrom(X) -> n__natsFrom(X) 566.59/149.21 , sel(N, XS) -> U41(tt(), N, XS) 566.59/149.21 , tail(cons(N, XS)) -> U71(tt(), activate(XS)) 566.59/149.21 , take(N, XS) -> U81(tt(), N, XS) } 566.59/149.21 Obligation: 566.59/149.21 innermost runtime complexity 566.59/149.21 Answer: 566.59/149.21 YES(O(1),O(n^1)) 566.59/149.21 566.59/149.21 Due to missing edges in the dependency-graph, the right-hand sides 566.59/149.21 of following rules could be simplified: 566.59/149.21 566.59/149.21 { U11^#(tt(), N, XS) -> 566.59/149.21 c_1(U12^#(tt(), activate(N), activate(XS)), 566.59/149.21 activate^#(N), 566.59/149.21 activate^#(XS)) 566.59/149.21 , U12^#(tt(), N, XS) -> 566.59/149.21 c_2(snd^#(splitAt(activate(N), activate(XS))), 566.59/149.21 splitAt^#(activate(N), activate(XS)), 566.59/149.21 activate^#(N), 566.59/149.21 activate^#(XS)) 566.59/149.21 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS)) 566.59/149.21 , U61^#(tt(), N, X, XS) -> 566.59/149.21 c_18(U62^#(tt(), activate(N), activate(X), activate(XS)), 566.59/149.21 activate^#(N), 566.59/149.21 activate^#(X), 566.59/149.21 activate^#(XS)) 566.59/149.21 , U41^#(tt(), N, XS) -> 566.59/149.21 c_12(U42^#(tt(), activate(N), activate(XS)), 566.59/149.21 activate^#(N), 566.59/149.21 activate^#(XS)) 566.59/149.21 , U42^#(tt(), N, XS) -> 566.59/149.21 c_13(head^#(afterNth(activate(N), activate(XS))), 566.59/149.21 afterNth^#(activate(N), activate(XS)), 566.59/149.21 activate^#(N), 566.59/149.21 activate^#(XS)) 566.59/149.21 , U62^#(tt(), N, X, XS) -> 566.59/149.21 c_19(U63^#(tt(), activate(N), activate(X), activate(XS)), 566.59/149.21 activate^#(N), 566.59/149.21 activate^#(X), 566.59/149.21 activate^#(XS)) 566.59/149.21 , U63^#(tt(), N, X, XS) -> 566.59/149.21 c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)), 566.59/149.21 splitAt^#(activate(N), activate(XS)), 566.59/149.21 activate^#(N), 566.59/149.21 activate^#(XS), 566.59/149.21 activate^#(X)) 566.59/149.21 , U81^#(tt(), N, XS) -> 566.59/149.21 c_24(U82^#(tt(), activate(N), activate(XS)), 566.59/149.21 activate^#(N), 566.59/149.21 activate^#(XS)) 566.59/149.21 , U82^#(tt(), N, XS) -> 566.59/149.21 c_25(fst^#(splitAt(activate(N), activate(XS))), 566.59/149.21 splitAt^#(activate(N), activate(XS)), 566.59/149.21 activate^#(N), 566.59/149.21 activate^#(XS)) } 566.59/149.21 566.59/149.21 We are left with following problem, upon which TcT provides the 566.59/149.21 certificate YES(O(1),O(n^1)). 566.59/149.21 566.59/149.21 Strict DPs: 566.59/149.21 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.21 , U61^#(tt(), N, X, XS) -> 566.59/149.21 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.21 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.21 , U62^#(tt(), N, X, XS) -> 566.59/149.21 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U63^#(tt(), N, X, XS) -> 566.59/149.21 c_9(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , U81^#(tt(), N, XS) -> 566.59/149.21 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , sel^#(N, XS) -> c_12(U41^#(tt(), N, XS)) 566.59/149.21 , take^#(N, XS) -> c_13(U81^#(tt(), N, XS)) } 566.59/149.21 Weak Trs: 566.59/149.21 { U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)) 566.59/149.21 , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 566.59/149.21 , activate(X) -> X 566.59/149.21 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.21 , snd(pair(X, Y)) -> U51(tt(), Y) 566.59/149.21 , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) 566.59/149.21 , splitAt(0(), XS) -> pair(nil(), XS) 566.59/149.21 , U21(tt(), X) -> U22(tt(), activate(X)) 566.59/149.21 , U22(tt(), X) -> activate(X) 566.59/149.21 , U31(tt(), N) -> U32(tt(), activate(N)) 566.59/149.21 , U32(tt(), N) -> activate(N) 566.59/149.21 , U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)) 566.59/149.21 , U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 566.59/149.21 , head(cons(N, XS)) -> U31(tt(), N) 566.59/149.21 , afterNth(N, XS) -> U11(tt(), N, XS) 566.59/149.21 , U51(tt(), Y) -> U52(tt(), activate(Y)) 566.59/149.21 , U52(tt(), Y) -> activate(Y) 566.59/149.21 , U61(tt(), N, X, XS) -> 566.59/149.21 U62(tt(), activate(N), activate(X), activate(XS)) 566.59/149.21 , U62(tt(), N, X, XS) -> 566.59/149.21 U63(tt(), activate(N), activate(X), activate(XS)) 566.59/149.21 , U63(tt(), N, X, XS) -> 566.59/149.21 U64(splitAt(activate(N), activate(XS)), activate(X)) 566.59/149.21 , U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 566.59/149.21 , U71(tt(), XS) -> U72(tt(), activate(XS)) 566.59/149.21 , U72(tt(), XS) -> activate(XS) 566.59/149.21 , U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)) 566.59/149.21 , U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 566.59/149.21 , fst(pair(X, Y)) -> U21(tt(), X) 566.59/149.21 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.21 , natsFrom(X) -> n__natsFrom(X) 566.59/149.21 , sel(N, XS) -> U41(tt(), N, XS) 566.59/149.21 , tail(cons(N, XS)) -> U71(tt(), activate(XS)) 566.59/149.21 , take(N, XS) -> U81(tt(), N, XS) } 566.59/149.21 Obligation: 566.59/149.21 innermost runtime complexity 566.59/149.21 Answer: 566.59/149.21 YES(O(1),O(n^1)) 566.59/149.21 566.59/149.21 We replace rewrite rules by usable rules: 566.59/149.21 566.59/149.21 Weak Usable Rules: 566.59/149.21 { activate(X) -> X 566.59/149.21 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.21 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.21 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.21 566.59/149.21 We are left with following problem, upon which TcT provides the 566.59/149.21 certificate YES(O(1),O(n^1)). 566.59/149.21 566.59/149.21 Strict DPs: 566.59/149.21 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.21 , U61^#(tt(), N, X, XS) -> 566.59/149.21 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.21 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.21 , U62^#(tt(), N, X, XS) -> 566.59/149.21 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U63^#(tt(), N, X, XS) -> 566.59/149.21 c_9(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , U81^#(tt(), N, XS) -> 566.59/149.21 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , sel^#(N, XS) -> c_12(U41^#(tt(), N, XS)) 566.59/149.21 , take^#(N, XS) -> c_13(U81^#(tt(), N, XS)) } 566.59/149.21 Weak Trs: 566.59/149.21 { activate(X) -> X 566.59/149.21 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.21 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.21 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.21 Obligation: 566.59/149.21 innermost runtime complexity 566.59/149.21 Answer: 566.59/149.21 YES(O(1),O(n^1)) 566.59/149.21 566.59/149.21 Consider the dependency graph 566.59/149.21 566.59/149.21 1: U11^#(tt(), N, XS) -> 566.59/149.21 c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.21 -->_1 U12^#(tt(), N, XS) -> 566.59/149.21 c_2(splitAt^#(activate(N), activate(XS))) :2 566.59/149.21 566.59/149.21 2: U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.21 -->_1 splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) :3 566.59/149.21 566.59/149.21 3: splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.21 -->_1 U61^#(tt(), N, X, XS) -> 566.59/149.21 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) :4 566.59/149.21 566.59/149.21 4: U61^#(tt(), N, X, XS) -> 566.59/149.21 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 -->_1 U62^#(tt(), N, X, XS) -> 566.59/149.21 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) :8 566.59/149.21 566.59/149.21 5: U41^#(tt(), N, XS) -> 566.59/149.21 c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.21 -->_1 U42^#(tt(), N, XS) -> 566.59/149.21 c_6(afterNth^#(activate(N), activate(XS))) :6 566.59/149.21 566.59/149.21 6: U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.21 -->_1 afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) :7 566.59/149.21 566.59/149.21 7: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.21 -->_1 U11^#(tt(), N, XS) -> 566.59/149.21 c_1(U12^#(tt(), activate(N), activate(XS))) :1 566.59/149.21 566.59/149.21 8: U62^#(tt(), N, X, XS) -> 566.59/149.21 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 -->_1 U63^#(tt(), N, X, XS) -> 566.59/149.21 c_9(splitAt^#(activate(N), activate(XS))) :9 566.59/149.21 566.59/149.21 9: U63^#(tt(), N, X, XS) -> 566.59/149.21 c_9(splitAt^#(activate(N), activate(XS))) 566.59/149.21 -->_1 splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) :3 566.59/149.21 566.59/149.21 10: U81^#(tt(), N, XS) -> 566.59/149.21 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.21 -->_1 U82^#(tt(), N, XS) -> 566.59/149.21 c_11(splitAt^#(activate(N), activate(XS))) :11 566.59/149.21 566.59/149.21 11: U82^#(tt(), N, XS) -> 566.59/149.21 c_11(splitAt^#(activate(N), activate(XS))) 566.59/149.21 -->_1 splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) :3 566.59/149.21 566.59/149.21 12: sel^#(N, XS) -> c_12(U41^#(tt(), N, XS)) 566.59/149.21 -->_1 U41^#(tt(), N, XS) -> 566.59/149.21 c_5(U42^#(tt(), activate(N), activate(XS))) :5 566.59/149.21 566.59/149.21 13: take^#(N, XS) -> c_13(U81^#(tt(), N, XS)) 566.59/149.21 -->_1 U81^#(tt(), N, XS) -> 566.59/149.21 c_10(U82^#(tt(), activate(N), activate(XS))) :10 566.59/149.21 566.59/149.21 566.59/149.21 Following roots of the dependency graph are removed, as the 566.59/149.21 considered set of starting terms is closed under reduction with 566.59/149.21 respect to these rules (modulo compound contexts). 566.59/149.21 566.59/149.21 { sel^#(N, XS) -> c_12(U41^#(tt(), N, XS)) 566.59/149.21 , take^#(N, XS) -> c_13(U81^#(tt(), N, XS)) } 566.59/149.21 566.59/149.21 566.59/149.21 We are left with following problem, upon which TcT provides the 566.59/149.21 certificate YES(O(1),O(n^1)). 566.59/149.21 566.59/149.21 Strict DPs: 566.59/149.21 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.21 , U61^#(tt(), N, X, XS) -> 566.59/149.21 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.21 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.21 , U62^#(tt(), N, X, XS) -> 566.59/149.21 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U63^#(tt(), N, X, XS) -> 566.59/149.21 c_9(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , U81^#(tt(), N, XS) -> 566.59/149.21 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U82^#(tt(), N, XS) -> 566.59/149.21 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.21 Weak Trs: 566.59/149.21 { activate(X) -> X 566.59/149.21 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.21 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.21 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.21 Obligation: 566.59/149.21 innermost runtime complexity 566.59/149.21 Answer: 566.59/149.21 YES(O(1),O(n^1)) 566.59/149.21 566.59/149.21 We analyse the complexity of following sub-problems (R) and (S). 566.59/149.21 Problem (S) is obtained from the input problem by shifting strict 566.59/149.21 rules from (R) into the weak component: 566.59/149.21 566.59/149.21 Problem (R): 566.59/149.21 ------------ 566.59/149.21 Strict DPs: 566.59/149.21 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.21 , U61^#(tt(), N, X, XS) -> 566.59/149.21 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.21 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.21 , U62^#(tt(), N, X, XS) -> 566.59/149.21 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U63^#(tt(), N, X, XS) -> 566.59/149.21 c_9(splitAt^#(activate(N), activate(XS))) } 566.59/149.21 Weak DPs: 566.59/149.21 { U81^#(tt(), N, XS) -> 566.59/149.21 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U82^#(tt(), N, XS) -> 566.59/149.21 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.21 Weak Trs: 566.59/149.21 { activate(X) -> X 566.59/149.21 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.21 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.21 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.21 StartTerms: basic terms 566.59/149.21 Strategy: innermost 566.59/149.21 566.59/149.21 Problem (S): 566.59/149.21 ------------ 566.59/149.21 Strict DPs: 566.59/149.21 { U81^#(tt(), N, XS) -> 566.59/149.21 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U82^#(tt(), N, XS) -> 566.59/149.21 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.21 Weak DPs: 566.59/149.21 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.21 , U61^#(tt(), N, X, XS) -> 566.59/149.21 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.21 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.21 , U62^#(tt(), N, X, XS) -> 566.59/149.21 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U63^#(tt(), N, X, XS) -> 566.59/149.21 c_9(splitAt^#(activate(N), activate(XS))) } 566.59/149.21 Weak Trs: 566.59/149.21 { activate(X) -> X 566.59/149.21 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.21 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.21 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.21 StartTerms: basic terms 566.59/149.21 Strategy: innermost 566.59/149.21 566.59/149.21 Overall, the transformation results in the following sub-problem(s): 566.59/149.21 566.59/149.21 Generated new problems: 566.59/149.21 ----------------------- 566.59/149.21 R) Strict DPs: 566.59/149.21 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.21 , U61^#(tt(), N, X, XS) -> 566.59/149.21 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.21 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.21 , U62^#(tt(), N, X, XS) -> 566.59/149.21 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U63^#(tt(), N, X, XS) -> 566.59/149.21 c_9(splitAt^#(activate(N), activate(XS))) } 566.59/149.21 Weak DPs: 566.59/149.21 { U81^#(tt(), N, XS) -> 566.59/149.21 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U82^#(tt(), N, XS) -> 566.59/149.21 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.21 Weak Trs: 566.59/149.21 { activate(X) -> X 566.59/149.21 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.21 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.21 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.21 StartTerms: basic terms 566.59/149.21 Strategy: innermost 566.59/149.21 566.59/149.21 This problem was proven YES(O(1),O(n^1)). 566.59/149.21 566.59/149.21 S) Strict DPs: 566.59/149.21 { U81^#(tt(), N, XS) -> 566.59/149.21 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U82^#(tt(), N, XS) -> 566.59/149.21 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.21 Weak DPs: 566.59/149.21 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.21 , U61^#(tt(), N, X, XS) -> 566.59/149.21 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.21 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.21 , U62^#(tt(), N, X, XS) -> 566.59/149.21 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U63^#(tt(), N, X, XS) -> 566.59/149.21 c_9(splitAt^#(activate(N), activate(XS))) } 566.59/149.21 Weak Trs: 566.59/149.21 { activate(X) -> X 566.59/149.21 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.21 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.21 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.21 StartTerms: basic terms 566.59/149.21 Strategy: innermost 566.59/149.21 566.59/149.21 This problem was proven YES(O(1),O(1)). 566.59/149.21 566.59/149.21 566.59/149.21 Proofs for generated problems: 566.59/149.21 ------------------------------ 566.59/149.21 R) We are left with following problem, upon which TcT provides the 566.59/149.21 certificate YES(O(1),O(n^1)). 566.59/149.21 566.59/149.21 Strict DPs: 566.59/149.21 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.21 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.21 , U61^#(tt(), N, X, XS) -> 566.59/149.21 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.21 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.21 , U62^#(tt(), N, X, XS) -> 566.59/149.21 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.21 , U63^#(tt(), N, X, XS) -> 566.59/149.21 c_9(splitAt^#(activate(N), activate(XS))) } 566.59/149.21 Weak DPs: 566.59/149.21 { U81^#(tt(), N, XS) -> 566.59/149.21 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.21 , U82^#(tt(), N, XS) -> 566.59/149.21 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.21 Weak Trs: 566.59/149.21 { activate(X) -> X 566.59/149.21 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.21 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.21 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.21 Obligation: 566.59/149.21 innermost runtime complexity 566.59/149.21 Answer: 566.59/149.21 YES(O(1),O(n^1)) 566.59/149.21 566.59/149.21 We use the processor 'matrix interpretation of dimension 1' to 566.59/149.21 orient following rules strictly. 566.59/149.21 566.59/149.21 DPs: 566.59/149.21 { 3: splitAt^#(s(N), cons(X, XS)) -> 566.59/149.21 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.21 , 5: U41^#(tt(), N, XS) -> 566.59/149.21 c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.21 , 10: U81^#(tt(), N, XS) -> 566.59/149.21 c_10(U82^#(tt(), activate(N), activate(XS))) } 566.59/149.21 566.59/149.21 Sub-proof: 566.59/149.21 ---------- 566.59/149.21 The following argument positions are usable: 566.59/149.21 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 566.59/149.21 Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, 566.59/149.21 Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, 566.59/149.21 Uargs(c_10) = {1}, Uargs(c_11) = {1} 566.59/149.21 566.59/149.21 TcT has computed the following constructor-based matrix 566.59/149.21 interpretation satisfying not(EDA). 566.59/149.21 566.59/149.21 [tt] = [0] 566.59/149.21 566.59/149.21 [activate](x1) = [1] x1 + [0] 566.59/149.21 566.59/149.21 [cons](x1, x2) = [0] 566.59/149.21 566.59/149.21 [natsFrom](x1) = [0] 566.59/149.21 566.59/149.21 [n__natsFrom](x1) = [0] 566.59/149.21 566.59/149.21 [s](x1) = [1] x1 + [1] 566.59/149.21 566.59/149.21 [U11^#](x1, x2, x3) = [4] x2 + [0] 566.59/149.21 566.59/149.21 [U12^#](x1, x2, x3) = [4] x2 + [0] 566.59/149.21 566.59/149.21 [splitAt^#](x1, x2) = [1] x1 + [0] 566.59/149.21 566.59/149.21 [U61^#](x1, x2, x3, x4) = [1] x2 + [0] 566.59/149.21 566.59/149.21 [U41^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 566.59/149.21 566.59/149.21 [U42^#](x1, x2, x3) = [4] x2 + [4] x3 + [0] 566.59/149.21 566.59/149.21 [afterNth^#](x1, x2) = [4] x1 + [4] x2 + [0] 566.59/149.21 566.59/149.21 [U62^#](x1, x2, x3, x4) = [1] x2 + [0] 566.59/149.21 566.59/149.21 [U63^#](x1, x2, x3, x4) = [1] x2 + [0] 566.59/149.21 566.59/149.21 [U81^#](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 566.59/149.21 566.59/149.21 [U82^#](x1, x2, x3) = [2] x2 + [0] 566.59/149.21 566.59/149.21 [c_1](x1) = [1] x1 + [0] 566.59/149.21 566.59/149.21 [c_2](x1) = [4] x1 + [0] 566.59/149.21 566.59/149.21 [c_3](x1) = [1] x1 + [0] 566.59/149.21 566.59/149.21 [c_4](x1) = [1] x1 + [0] 566.59/149.21 566.59/149.21 [c_5](x1) = [1] x1 + [3] 566.59/149.21 566.59/149.21 [c_6](x1) = [1] x1 + [0] 566.59/149.21 566.59/149.21 [c_7](x1) = [1] x1 + [0] 566.59/149.21 566.59/149.21 [c_8](x1) = [1] x1 + [0] 566.59/149.21 566.59/149.21 [c_9](x1) = [1] x1 + [0] 566.59/149.21 566.59/149.21 [c_10](x1) = [2] x1 + [3] 566.59/149.21 566.59/149.21 [c_11](x1) = [2] x1 + [0] 566.59/149.21 566.59/149.21 The order satisfies the following ordering constraints: 566.59/149.21 566.59/149.21 [activate(X)] = [1] X + [0] 566.59/149.21 >= [1] X + [0] 566.59/149.21 = [X] 566.59/149.21 566.59/149.21 [activate(n__natsFrom(X))] = [0] 566.59/149.21 >= [0] 566.59/149.21 = [natsFrom(X)] 566.59/149.21 566.59/149.21 [natsFrom(N)] = [0] 566.59/149.21 >= [0] 566.59/149.21 = [cons(N, n__natsFrom(s(N)))] 566.59/149.21 566.59/149.21 [natsFrom(X)] = [0] 566.59/149.21 >= [0] 566.59/149.21 = [n__natsFrom(X)] 566.59/149.21 566.59/149.21 [U11^#(tt(), N, XS)] = [4] N + [0] 566.59/149.21 >= [4] N + [0] 566.59/149.21 = [c_1(U12^#(tt(), activate(N), activate(XS)))] 566.59/149.21 566.59/149.21 [U12^#(tt(), N, XS)] = [4] N + [0] 566.59/149.21 >= [4] N + [0] 566.59/149.21 = [c_2(splitAt^#(activate(N), activate(XS)))] 566.59/149.21 566.59/149.21 [splitAt^#(s(N), cons(X, XS))] = [1] N + [1] 566.59/149.21 > [1] N + [0] 566.59/149.21 = [c_3(U61^#(tt(), N, X, activate(XS)))] 566.59/149.21 566.59/149.21 [U61^#(tt(), N, X, XS)] = [1] N + [0] 566.59/149.21 >= [1] N + [0] 566.59/149.21 = [c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))] 566.59/149.21 566.59/149.21 [U41^#(tt(), N, XS)] = [7] N + [7] XS + [7] 566.59/149.22 > [4] N + [4] XS + [3] 566.59/149.22 = [c_5(U42^#(tt(), activate(N), activate(XS)))] 566.59/149.22 566.59/149.22 [U42^#(tt(), N, XS)] = [4] N + [4] XS + [0] 566.59/149.22 >= [4] N + [4] XS + [0] 566.59/149.22 = [c_6(afterNth^#(activate(N), activate(XS)))] 566.59/149.22 566.59/149.22 [afterNth^#(N, XS)] = [4] N + [4] XS + [0] 566.59/149.22 >= [4] N + [0] 566.59/149.22 = [c_7(U11^#(tt(), N, XS))] 566.59/149.22 566.59/149.22 [U62^#(tt(), N, X, XS)] = [1] N + [0] 566.59/149.22 >= [1] N + [0] 566.59/149.22 = [c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))] 566.59/149.22 566.59/149.22 [U63^#(tt(), N, X, XS)] = [1] N + [0] 566.59/149.22 >= [1] N + [0] 566.59/149.22 = [c_9(splitAt^#(activate(N), activate(XS)))] 566.59/149.22 566.59/149.22 [U81^#(tt(), N, XS)] = [7] N + [7] XS + [7] 566.59/149.22 > [4] N + [3] 566.59/149.22 = [c_10(U82^#(tt(), activate(N), activate(XS)))] 566.59/149.22 566.59/149.22 [U82^#(tt(), N, XS)] = [2] N + [0] 566.59/149.22 >= [2] N + [0] 566.59/149.22 = [c_11(splitAt^#(activate(N), activate(XS)))] 566.59/149.22 566.59/149.22 566.59/149.22 We return to the main proof. Consider the set of all dependency 566.59/149.22 pairs 566.59/149.22 566.59/149.22 : 566.59/149.22 { 1: U11^#(tt(), N, XS) -> 566.59/149.22 c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.22 , 2: U12^#(tt(), N, XS) -> 566.59/149.22 c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , 3: splitAt^#(s(N), cons(X, XS)) -> 566.59/149.22 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.22 , 4: U61^#(tt(), N, X, XS) -> 566.59/149.22 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , 5: U41^#(tt(), N, XS) -> 566.59/149.22 c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.22 , 6: U42^#(tt(), N, XS) -> 566.59/149.22 c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.22 , 7: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.22 , 8: U62^#(tt(), N, X, XS) -> 566.59/149.22 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , 9: U63^#(tt(), N, X, XS) -> 566.59/149.22 c_9(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , 10: U81^#(tt(), N, XS) -> 566.59/149.22 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.22 , 11: U82^#(tt(), N, XS) -> 566.59/149.22 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.22 566.59/149.22 Processor 'matrix interpretation of dimension 1' induces the 566.59/149.22 complexity certificate YES(?,O(n^1)) on application of dependency 566.59/149.22 pairs {3,5,10}. These cover all (indirect) predecessors of 566.59/149.22 dependency pairs {1,2,3,4,5,6,7,8,9,10,11}, their number of 566.59/149.22 application is equally bounded. The dependency pairs are shifted 566.59/149.22 into the weak component. 566.59/149.22 566.59/149.22 We are left with following problem, upon which TcT provides the 566.59/149.22 certificate YES(O(1),O(1)). 566.59/149.22 566.59/149.22 Weak DPs: 566.59/149.22 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.22 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.22 , U61^#(tt(), N, X, XS) -> 566.59/149.22 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.22 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.22 , U62^#(tt(), N, X, XS) -> 566.59/149.22 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U63^#(tt(), N, X, XS) -> 566.59/149.22 c_9(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , U81^#(tt(), N, XS) -> 566.59/149.22 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U82^#(tt(), N, XS) -> 566.59/149.22 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.22 Weak Trs: 566.59/149.22 { activate(X) -> X 566.59/149.22 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.22 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.22 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.22 Obligation: 566.59/149.22 innermost runtime complexity 566.59/149.22 Answer: 566.59/149.22 YES(O(1),O(1)) 566.59/149.22 566.59/149.22 The following weak DPs constitute a sub-graph of the DG that is 566.59/149.22 closed under successors. The DPs are removed. 566.59/149.22 566.59/149.22 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.22 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.22 , U61^#(tt(), N, X, XS) -> 566.59/149.22 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.22 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.22 , U62^#(tt(), N, X, XS) -> 566.59/149.22 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U63^#(tt(), N, X, XS) -> 566.59/149.22 c_9(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , U81^#(tt(), N, XS) -> 566.59/149.22 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U82^#(tt(), N, XS) -> 566.59/149.22 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.22 566.59/149.22 We are left with following problem, upon which TcT provides the 566.59/149.22 certificate YES(O(1),O(1)). 566.59/149.22 566.59/149.22 Weak Trs: 566.59/149.22 { activate(X) -> X 566.59/149.22 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.22 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.22 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.22 Obligation: 566.59/149.22 innermost runtime complexity 566.59/149.22 Answer: 566.59/149.22 YES(O(1),O(1)) 566.59/149.22 566.59/149.22 No rule is usable, rules are removed from the input problem. 566.59/149.22 566.59/149.22 We are left with following problem, upon which TcT provides the 566.59/149.22 certificate YES(O(1),O(1)). 566.59/149.22 566.59/149.22 Rules: Empty 566.59/149.22 Obligation: 566.59/149.22 innermost runtime complexity 566.59/149.22 Answer: 566.59/149.22 YES(O(1),O(1)) 566.59/149.22 566.59/149.22 Empty rules are trivially bounded 566.59/149.22 566.59/149.22 S) We are left with following problem, upon which TcT provides the 566.59/149.22 certificate YES(O(1),O(1)). 566.59/149.22 566.59/149.22 Strict DPs: 566.59/149.22 { U81^#(tt(), N, XS) -> 566.59/149.22 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U82^#(tt(), N, XS) -> 566.59/149.22 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.22 Weak DPs: 566.59/149.22 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.22 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.22 , U61^#(tt(), N, X, XS) -> 566.59/149.22 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.22 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.22 , U62^#(tt(), N, X, XS) -> 566.59/149.22 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U63^#(tt(), N, X, XS) -> 566.59/149.22 c_9(splitAt^#(activate(N), activate(XS))) } 566.59/149.22 Weak Trs: 566.59/149.22 { activate(X) -> X 566.59/149.22 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.22 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.22 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.22 Obligation: 566.59/149.22 innermost runtime complexity 566.59/149.22 Answer: 566.59/149.22 YES(O(1),O(1)) 566.59/149.22 566.59/149.22 We estimate the number of application of {2} by applications of 566.59/149.22 Pre({2}) = {1}. Here rules are labeled as follows: 566.59/149.22 566.59/149.22 DPs: 566.59/149.22 { 1: U81^#(tt(), N, XS) -> 566.59/149.22 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.22 , 2: U82^#(tt(), N, XS) -> 566.59/149.22 c_11(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , 3: U11^#(tt(), N, XS) -> 566.59/149.22 c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.22 , 4: U12^#(tt(), N, XS) -> 566.59/149.22 c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , 5: splitAt^#(s(N), cons(X, XS)) -> 566.59/149.22 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.22 , 6: U61^#(tt(), N, X, XS) -> 566.59/149.22 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , 7: U41^#(tt(), N, XS) -> 566.59/149.22 c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.22 , 8: U42^#(tt(), N, XS) -> 566.59/149.22 c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.22 , 9: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.22 , 10: U62^#(tt(), N, X, XS) -> 566.59/149.22 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , 11: U63^#(tt(), N, X, XS) -> 566.59/149.22 c_9(splitAt^#(activate(N), activate(XS))) } 566.59/149.22 566.59/149.22 We are left with following problem, upon which TcT provides the 566.59/149.22 certificate YES(O(1),O(1)). 566.59/149.22 566.59/149.22 Strict DPs: 566.59/149.22 { U81^#(tt(), N, XS) -> 566.59/149.22 c_10(U82^#(tt(), activate(N), activate(XS))) } 566.59/149.22 Weak DPs: 566.59/149.22 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.22 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.22 , U61^#(tt(), N, X, XS) -> 566.59/149.22 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.22 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.22 , U62^#(tt(), N, X, XS) -> 566.59/149.22 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U63^#(tt(), N, X, XS) -> 566.59/149.22 c_9(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , U82^#(tt(), N, XS) -> 566.59/149.22 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.22 Weak Trs: 566.59/149.22 { activate(X) -> X 566.59/149.22 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.22 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.22 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.22 Obligation: 566.59/149.22 innermost runtime complexity 566.59/149.22 Answer: 566.59/149.22 YES(O(1),O(1)) 566.59/149.22 566.59/149.22 We estimate the number of application of {1} by applications of 566.59/149.22 Pre({1}) = {}. Here rules are labeled as follows: 566.59/149.22 566.59/149.22 DPs: 566.59/149.22 { 1: U81^#(tt(), N, XS) -> 566.59/149.22 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.22 , 2: U11^#(tt(), N, XS) -> 566.59/149.22 c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.22 , 3: U12^#(tt(), N, XS) -> 566.59/149.22 c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , 4: splitAt^#(s(N), cons(X, XS)) -> 566.59/149.22 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.22 , 5: U61^#(tt(), N, X, XS) -> 566.59/149.22 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , 6: U41^#(tt(), N, XS) -> 566.59/149.22 c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.22 , 7: U42^#(tt(), N, XS) -> 566.59/149.22 c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.22 , 8: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.22 , 9: U62^#(tt(), N, X, XS) -> 566.59/149.22 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , 10: U63^#(tt(), N, X, XS) -> 566.59/149.22 c_9(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , 11: U82^#(tt(), N, XS) -> 566.59/149.22 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.22 566.59/149.22 We are left with following problem, upon which TcT provides the 566.59/149.22 certificate YES(O(1),O(1)). 566.59/149.22 566.59/149.22 Weak DPs: 566.59/149.22 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.22 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.22 , U61^#(tt(), N, X, XS) -> 566.59/149.22 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.22 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.22 , U62^#(tt(), N, X, XS) -> 566.59/149.22 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U63^#(tt(), N, X, XS) -> 566.59/149.22 c_9(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , U81^#(tt(), N, XS) -> 566.59/149.22 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U82^#(tt(), N, XS) -> 566.59/149.22 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.22 Weak Trs: 566.59/149.22 { activate(X) -> X 566.59/149.22 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.22 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.22 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.22 Obligation: 566.59/149.22 innermost runtime complexity 566.59/149.22 Answer: 566.59/149.22 YES(O(1),O(1)) 566.59/149.22 566.59/149.22 The following weak DPs constitute a sub-graph of the DG that is 566.59/149.22 closed under successors. The DPs are removed. 566.59/149.22 566.59/149.22 { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , splitAt^#(s(N), cons(X, XS)) -> 566.59/149.22 c_3(U61^#(tt(), N, X, activate(XS))) 566.59/149.22 , U61^#(tt(), N, X, XS) -> 566.59/149.22 c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS))) 566.59/149.22 , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) 566.59/149.22 , U62^#(tt(), N, X, XS) -> 566.59/149.22 c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) 566.59/149.22 , U63^#(tt(), N, X, XS) -> 566.59/149.22 c_9(splitAt^#(activate(N), activate(XS))) 566.59/149.22 , U81^#(tt(), N, XS) -> 566.59/149.22 c_10(U82^#(tt(), activate(N), activate(XS))) 566.59/149.22 , U82^#(tt(), N, XS) -> 566.59/149.22 c_11(splitAt^#(activate(N), activate(XS))) } 566.59/149.22 566.59/149.22 We are left with following problem, upon which TcT provides the 566.59/149.22 certificate YES(O(1),O(1)). 566.59/149.22 566.59/149.22 Weak Trs: 566.59/149.22 { activate(X) -> X 566.59/149.22 , activate(n__natsFrom(X)) -> natsFrom(X) 566.59/149.22 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 566.59/149.22 , natsFrom(X) -> n__natsFrom(X) } 566.59/149.22 Obligation: 566.59/149.22 innermost runtime complexity 566.59/149.22 Answer: 566.59/149.22 YES(O(1),O(1)) 566.59/149.22 566.59/149.22 No rule is usable, rules are removed from the input problem. 566.59/149.22 566.59/149.22 We are left with following problem, upon which TcT provides the 566.59/149.22 certificate YES(O(1),O(1)). 566.59/149.22 566.59/149.22 Rules: Empty 566.59/149.22 Obligation: 566.59/149.22 innermost runtime complexity 566.59/149.22 Answer: 566.59/149.22 YES(O(1),O(1)) 566.59/149.22 566.59/149.22 Empty rules are trivially bounded 566.59/149.22 566.59/149.22 566.59/149.22 Hurray, we answered YES(O(1),O(n^1)) 566.82/149.45 EOF