YES(O(1),O(n^1)) 432.22/149.18 YES(O(1),O(n^1)) 432.22/149.18 432.22/149.18 We are left with following problem, upon which TcT provides the 432.22/149.18 certificate YES(O(1),O(n^1)). 432.22/149.18 432.22/149.18 Strict Trs: 432.22/149.18 { U11(tt(), N, X, XS) -> 432.22/149.18 U12(splitAt(activate(N), activate(XS)), activate(X)) 432.22/149.18 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 432.22/149.18 , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS)) 432.22/149.18 , splitAt(0(), XS) -> pair(nil(), XS) 432.22/149.18 , activate(X) -> X 432.22/149.18 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.18 , afterNth(N, XS) -> snd(splitAt(N, XS)) 432.22/149.18 , snd(pair(X, Y)) -> Y 432.22/149.18 , and(tt(), X) -> activate(X) 432.22/149.18 , fst(pair(X, Y)) -> X 432.22/149.18 , head(cons(N, XS)) -> N 432.22/149.18 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.18 , natsFrom(X) -> n__natsFrom(X) 432.22/149.18 , sel(N, XS) -> head(afterNth(N, XS)) 432.22/149.18 , tail(cons(N, XS)) -> activate(XS) 432.22/149.18 , take(N, XS) -> fst(splitAt(N, XS)) } 432.22/149.18 Obligation: 432.22/149.18 innermost runtime complexity 432.22/149.18 Answer: 432.22/149.18 YES(O(1),O(n^1)) 432.22/149.18 432.22/149.18 We add the following dependency tuples: 432.22/149.18 432.22/149.18 Strict DPs: 432.22/149.18 { U11^#(tt(), N, X, XS) -> 432.22/149.18 c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)), 432.22/149.18 splitAt^#(activate(N), activate(XS)), 432.22/149.18 activate^#(N), 432.22/149.18 activate^#(XS), 432.22/149.18 activate^#(X)) 432.22/149.18 , U12^#(pair(YS, ZS), X) -> c_2(activate^#(X)) 432.22/149.18 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.18 c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS)) 432.22/149.18 , splitAt^#(0(), XS) -> c_4() 432.22/149.18 , activate^#(X) -> c_5() 432.22/149.18 , activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X)) 432.22/149.18 , natsFrom^#(N) -> c_12() 432.22/149.18 , natsFrom^#(X) -> c_13() 432.22/149.18 , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , snd^#(pair(X, Y)) -> c_8() 432.22/149.18 , and^#(tt(), X) -> c_9(activate^#(X)) 432.22/149.18 , fst^#(pair(X, Y)) -> c_10() 432.22/149.18 , head^#(cons(N, XS)) -> c_11() 432.22/149.18 , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 432.22/149.18 , tail^#(cons(N, XS)) -> c_15(activate^#(XS)) 432.22/149.18 , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 432.22/149.18 432.22/149.18 and mark the set of starting terms. 432.22/149.18 432.22/149.18 We are left with following problem, upon which TcT provides the 432.22/149.18 certificate YES(O(1),O(n^1)). 432.22/149.18 432.22/149.18 Strict DPs: 432.22/149.18 { U11^#(tt(), N, X, XS) -> 432.22/149.18 c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)), 432.22/149.18 splitAt^#(activate(N), activate(XS)), 432.22/149.18 activate^#(N), 432.22/149.18 activate^#(XS), 432.22/149.18 activate^#(X)) 432.22/149.18 , U12^#(pair(YS, ZS), X) -> c_2(activate^#(X)) 432.22/149.18 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.18 c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS)) 432.22/149.18 , splitAt^#(0(), XS) -> c_4() 432.22/149.18 , activate^#(X) -> c_5() 432.22/149.18 , activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X)) 432.22/149.18 , natsFrom^#(N) -> c_12() 432.22/149.18 , natsFrom^#(X) -> c_13() 432.22/149.18 , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , snd^#(pair(X, Y)) -> c_8() 432.22/149.18 , and^#(tt(), X) -> c_9(activate^#(X)) 432.22/149.18 , fst^#(pair(X, Y)) -> c_10() 432.22/149.18 , head^#(cons(N, XS)) -> c_11() 432.22/149.18 , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 432.22/149.18 , tail^#(cons(N, XS)) -> c_15(activate^#(XS)) 432.22/149.18 , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 432.22/149.18 Weak Trs: 432.22/149.18 { U11(tt(), N, X, XS) -> 432.22/149.18 U12(splitAt(activate(N), activate(XS)), activate(X)) 432.22/149.18 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 432.22/149.18 , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS)) 432.22/149.18 , splitAt(0(), XS) -> pair(nil(), XS) 432.22/149.18 , activate(X) -> X 432.22/149.18 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.18 , afterNth(N, XS) -> snd(splitAt(N, XS)) 432.22/149.18 , snd(pair(X, Y)) -> Y 432.22/149.18 , and(tt(), X) -> activate(X) 432.22/149.18 , fst(pair(X, Y)) -> X 432.22/149.18 , head(cons(N, XS)) -> N 432.22/149.18 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.18 , natsFrom(X) -> n__natsFrom(X) 432.22/149.18 , sel(N, XS) -> head(afterNth(N, XS)) 432.22/149.18 , tail(cons(N, XS)) -> activate(XS) 432.22/149.18 , take(N, XS) -> fst(splitAt(N, XS)) } 432.22/149.18 Obligation: 432.22/149.18 innermost runtime complexity 432.22/149.18 Answer: 432.22/149.18 YES(O(1),O(n^1)) 432.22/149.18 432.22/149.18 We estimate the number of application of {4,5,7,8,10,12,13} by 432.22/149.18 applications of Pre({4,5,7,8,10,12,13}) = {1,2,3,6,9,11,14,15,16}. 432.22/149.18 Here rules are labeled as follows: 432.22/149.18 432.22/149.18 DPs: 432.22/149.18 { 1: U11^#(tt(), N, X, XS) -> 432.22/149.18 c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)), 432.22/149.18 splitAt^#(activate(N), activate(XS)), 432.22/149.18 activate^#(N), 432.22/149.18 activate^#(XS), 432.22/149.18 activate^#(X)) 432.22/149.18 , 2: U12^#(pair(YS, ZS), X) -> c_2(activate^#(X)) 432.22/149.18 , 3: splitAt^#(s(N), cons(X, XS)) -> 432.22/149.18 c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS)) 432.22/149.18 , 4: splitAt^#(0(), XS) -> c_4() 432.22/149.18 , 5: activate^#(X) -> c_5() 432.22/149.18 , 6: activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X)) 432.22/149.18 , 7: natsFrom^#(N) -> c_12() 432.22/149.18 , 8: natsFrom^#(X) -> c_13() 432.22/149.18 , 9: afterNth^#(N, XS) -> 432.22/149.18 c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , 10: snd^#(pair(X, Y)) -> c_8() 432.22/149.18 , 11: and^#(tt(), X) -> c_9(activate^#(X)) 432.22/149.18 , 12: fst^#(pair(X, Y)) -> c_10() 432.22/149.18 , 13: head^#(cons(N, XS)) -> c_11() 432.22/149.18 , 14: sel^#(N, XS) -> 432.22/149.18 c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 432.22/149.18 , 15: tail^#(cons(N, XS)) -> c_15(activate^#(XS)) 432.22/149.18 , 16: take^#(N, XS) -> 432.22/149.18 c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 432.22/149.18 432.22/149.18 We are left with following problem, upon which TcT provides the 432.22/149.18 certificate YES(O(1),O(n^1)). 432.22/149.18 432.22/149.18 Strict DPs: 432.22/149.18 { U11^#(tt(), N, X, XS) -> 432.22/149.18 c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)), 432.22/149.18 splitAt^#(activate(N), activate(XS)), 432.22/149.18 activate^#(N), 432.22/149.18 activate^#(XS), 432.22/149.18 activate^#(X)) 432.22/149.18 , U12^#(pair(YS, ZS), X) -> c_2(activate^#(X)) 432.22/149.18 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.18 c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS)) 432.22/149.18 , activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X)) 432.22/149.18 , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , and^#(tt(), X) -> c_9(activate^#(X)) 432.22/149.18 , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 432.22/149.18 , tail^#(cons(N, XS)) -> c_15(activate^#(XS)) 432.22/149.18 , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 432.22/149.18 Weak DPs: 432.22/149.18 { splitAt^#(0(), XS) -> c_4() 432.22/149.18 , activate^#(X) -> c_5() 432.22/149.18 , natsFrom^#(N) -> c_12() 432.22/149.18 , natsFrom^#(X) -> c_13() 432.22/149.18 , snd^#(pair(X, Y)) -> c_8() 432.22/149.18 , fst^#(pair(X, Y)) -> c_10() 432.22/149.18 , head^#(cons(N, XS)) -> c_11() } 432.22/149.18 Weak Trs: 432.22/149.18 { U11(tt(), N, X, XS) -> 432.22/149.18 U12(splitAt(activate(N), activate(XS)), activate(X)) 432.22/149.18 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 432.22/149.18 , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS)) 432.22/149.18 , splitAt(0(), XS) -> pair(nil(), XS) 432.22/149.18 , activate(X) -> X 432.22/149.18 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.18 , afterNth(N, XS) -> snd(splitAt(N, XS)) 432.22/149.18 , snd(pair(X, Y)) -> Y 432.22/149.18 , and(tt(), X) -> activate(X) 432.22/149.18 , fst(pair(X, Y)) -> X 432.22/149.18 , head(cons(N, XS)) -> N 432.22/149.18 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.18 , natsFrom(X) -> n__natsFrom(X) 432.22/149.18 , sel(N, XS) -> head(afterNth(N, XS)) 432.22/149.18 , tail(cons(N, XS)) -> activate(XS) 432.22/149.18 , take(N, XS) -> fst(splitAt(N, XS)) } 432.22/149.18 Obligation: 432.22/149.18 innermost runtime complexity 432.22/149.18 Answer: 432.22/149.18 YES(O(1),O(n^1)) 432.22/149.18 432.22/149.18 We estimate the number of application of {4} by applications of 432.22/149.18 Pre({4}) = {1,2,3,6,8}. Here rules are labeled as follows: 432.22/149.18 432.22/149.18 DPs: 432.22/149.18 { 1: U11^#(tt(), N, X, XS) -> 432.22/149.18 c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)), 432.22/149.18 splitAt^#(activate(N), activate(XS)), 432.22/149.18 activate^#(N), 432.22/149.18 activate^#(XS), 432.22/149.18 activate^#(X)) 432.22/149.18 , 2: U12^#(pair(YS, ZS), X) -> c_2(activate^#(X)) 432.22/149.18 , 3: splitAt^#(s(N), cons(X, XS)) -> 432.22/149.18 c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS)) 432.22/149.18 , 4: activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X)) 432.22/149.18 , 5: afterNth^#(N, XS) -> 432.22/149.18 c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , 6: and^#(tt(), X) -> c_9(activate^#(X)) 432.22/149.18 , 7: sel^#(N, XS) -> 432.22/149.18 c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 432.22/149.18 , 8: tail^#(cons(N, XS)) -> c_15(activate^#(XS)) 432.22/149.18 , 9: take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , 10: splitAt^#(0(), XS) -> c_4() 432.22/149.18 , 11: activate^#(X) -> c_5() 432.22/149.18 , 12: natsFrom^#(N) -> c_12() 432.22/149.18 , 13: natsFrom^#(X) -> c_13() 432.22/149.18 , 14: snd^#(pair(X, Y)) -> c_8() 432.22/149.18 , 15: fst^#(pair(X, Y)) -> c_10() 432.22/149.18 , 16: head^#(cons(N, XS)) -> c_11() } 432.22/149.18 432.22/149.18 We are left with following problem, upon which TcT provides the 432.22/149.18 certificate YES(O(1),O(n^1)). 432.22/149.18 432.22/149.18 Strict DPs: 432.22/149.18 { U11^#(tt(), N, X, XS) -> 432.22/149.18 c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)), 432.22/149.18 splitAt^#(activate(N), activate(XS)), 432.22/149.18 activate^#(N), 432.22/149.18 activate^#(XS), 432.22/149.18 activate^#(X)) 432.22/149.18 , U12^#(pair(YS, ZS), X) -> c_2(activate^#(X)) 432.22/149.18 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.18 c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS)) 432.22/149.18 , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , and^#(tt(), X) -> c_9(activate^#(X)) 432.22/149.18 , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 432.22/149.18 , tail^#(cons(N, XS)) -> c_15(activate^#(XS)) 432.22/149.18 , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 432.22/149.18 Weak DPs: 432.22/149.18 { splitAt^#(0(), XS) -> c_4() 432.22/149.18 , activate^#(X) -> c_5() 432.22/149.18 , activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X)) 432.22/149.18 , natsFrom^#(N) -> c_12() 432.22/149.18 , natsFrom^#(X) -> c_13() 432.22/149.18 , snd^#(pair(X, Y)) -> c_8() 432.22/149.18 , fst^#(pair(X, Y)) -> c_10() 432.22/149.18 , head^#(cons(N, XS)) -> c_11() } 432.22/149.18 Weak Trs: 432.22/149.18 { U11(tt(), N, X, XS) -> 432.22/149.18 U12(splitAt(activate(N), activate(XS)), activate(X)) 432.22/149.18 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 432.22/149.18 , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS)) 432.22/149.18 , splitAt(0(), XS) -> pair(nil(), XS) 432.22/149.18 , activate(X) -> X 432.22/149.18 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.18 , afterNth(N, XS) -> snd(splitAt(N, XS)) 432.22/149.18 , snd(pair(X, Y)) -> Y 432.22/149.18 , and(tt(), X) -> activate(X) 432.22/149.18 , fst(pair(X, Y)) -> X 432.22/149.18 , head(cons(N, XS)) -> N 432.22/149.18 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.18 , natsFrom(X) -> n__natsFrom(X) 432.22/149.18 , sel(N, XS) -> head(afterNth(N, XS)) 432.22/149.18 , tail(cons(N, XS)) -> activate(XS) 432.22/149.18 , take(N, XS) -> fst(splitAt(N, XS)) } 432.22/149.18 Obligation: 432.22/149.18 innermost runtime complexity 432.22/149.18 Answer: 432.22/149.18 YES(O(1),O(n^1)) 432.22/149.18 432.22/149.18 We estimate the number of application of {2,5,7} by applications of 432.22/149.18 Pre({2,5,7}) = {1}. Here rules are labeled as follows: 432.22/149.18 432.22/149.18 DPs: 432.22/149.18 { 1: U11^#(tt(), N, X, XS) -> 432.22/149.18 c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)), 432.22/149.18 splitAt^#(activate(N), activate(XS)), 432.22/149.18 activate^#(N), 432.22/149.18 activate^#(XS), 432.22/149.18 activate^#(X)) 432.22/149.18 , 2: U12^#(pair(YS, ZS), X) -> c_2(activate^#(X)) 432.22/149.18 , 3: splitAt^#(s(N), cons(X, XS)) -> 432.22/149.18 c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS)) 432.22/149.18 , 4: afterNth^#(N, XS) -> 432.22/149.18 c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , 5: and^#(tt(), X) -> c_9(activate^#(X)) 432.22/149.18 , 6: sel^#(N, XS) -> 432.22/149.18 c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 432.22/149.18 , 7: tail^#(cons(N, XS)) -> c_15(activate^#(XS)) 432.22/149.18 , 8: take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , 9: splitAt^#(0(), XS) -> c_4() 432.22/149.18 , 10: activate^#(X) -> c_5() 432.22/149.18 , 11: activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X)) 432.22/149.18 , 12: natsFrom^#(N) -> c_12() 432.22/149.18 , 13: natsFrom^#(X) -> c_13() 432.22/149.18 , 14: snd^#(pair(X, Y)) -> c_8() 432.22/149.18 , 15: fst^#(pair(X, Y)) -> c_10() 432.22/149.18 , 16: head^#(cons(N, XS)) -> c_11() } 432.22/149.18 432.22/149.18 We are left with following problem, upon which TcT provides the 432.22/149.18 certificate YES(O(1),O(n^1)). 432.22/149.18 432.22/149.18 Strict DPs: 432.22/149.18 { U11^#(tt(), N, X, XS) -> 432.22/149.18 c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)), 432.22/149.18 splitAt^#(activate(N), activate(XS)), 432.22/149.18 activate^#(N), 432.22/149.18 activate^#(XS), 432.22/149.18 activate^#(X)) 432.22/149.18 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.18 c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS)) 432.22/149.18 , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 432.22/149.18 , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 432.22/149.18 Weak DPs: 432.22/149.18 { U12^#(pair(YS, ZS), X) -> c_2(activate^#(X)) 432.22/149.18 , splitAt^#(0(), XS) -> c_4() 432.22/149.18 , activate^#(X) -> c_5() 432.22/149.18 , activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X)) 432.22/149.18 , natsFrom^#(N) -> c_12() 432.22/149.18 , natsFrom^#(X) -> c_13() 432.22/149.18 , snd^#(pair(X, Y)) -> c_8() 432.22/149.18 , and^#(tt(), X) -> c_9(activate^#(X)) 432.22/149.18 , fst^#(pair(X, Y)) -> c_10() 432.22/149.18 , head^#(cons(N, XS)) -> c_11() 432.22/149.18 , tail^#(cons(N, XS)) -> c_15(activate^#(XS)) } 432.22/149.18 Weak Trs: 432.22/149.18 { U11(tt(), N, X, XS) -> 432.22/149.18 U12(splitAt(activate(N), activate(XS)), activate(X)) 432.22/149.18 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 432.22/149.18 , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS)) 432.22/149.18 , splitAt(0(), XS) -> pair(nil(), XS) 432.22/149.18 , activate(X) -> X 432.22/149.18 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.18 , afterNth(N, XS) -> snd(splitAt(N, XS)) 432.22/149.18 , snd(pair(X, Y)) -> Y 432.22/149.18 , and(tt(), X) -> activate(X) 432.22/149.18 , fst(pair(X, Y)) -> X 432.22/149.18 , head(cons(N, XS)) -> N 432.22/149.18 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.18 , natsFrom(X) -> n__natsFrom(X) 432.22/149.18 , sel(N, XS) -> head(afterNth(N, XS)) 432.22/149.18 , tail(cons(N, XS)) -> activate(XS) 432.22/149.18 , take(N, XS) -> fst(splitAt(N, XS)) } 432.22/149.18 Obligation: 432.22/149.18 innermost runtime complexity 432.22/149.18 Answer: 432.22/149.18 YES(O(1),O(n^1)) 432.22/149.18 432.22/149.18 The following weak DPs constitute a sub-graph of the DG that is 432.22/149.18 closed under successors. The DPs are removed. 432.22/149.18 432.22/149.18 { U12^#(pair(YS, ZS), X) -> c_2(activate^#(X)) 432.22/149.18 , splitAt^#(0(), XS) -> c_4() 432.22/149.18 , activate^#(X) -> c_5() 432.22/149.18 , activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X)) 432.22/149.18 , natsFrom^#(N) -> c_12() 432.22/149.18 , natsFrom^#(X) -> c_13() 432.22/149.18 , snd^#(pair(X, Y)) -> c_8() 432.22/149.18 , and^#(tt(), X) -> c_9(activate^#(X)) 432.22/149.18 , fst^#(pair(X, Y)) -> c_10() 432.22/149.18 , head^#(cons(N, XS)) -> c_11() 432.22/149.18 , tail^#(cons(N, XS)) -> c_15(activate^#(XS)) } 432.22/149.18 432.22/149.18 We are left with following problem, upon which TcT provides the 432.22/149.18 certificate YES(O(1),O(n^1)). 432.22/149.18 432.22/149.18 Strict DPs: 432.22/149.18 { U11^#(tt(), N, X, XS) -> 432.22/149.18 c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)), 432.22/149.18 splitAt^#(activate(N), activate(XS)), 432.22/149.18 activate^#(N), 432.22/149.18 activate^#(XS), 432.22/149.18 activate^#(X)) 432.22/149.18 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.18 c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS)) 432.22/149.18 , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 432.22/149.18 , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 432.22/149.18 Weak Trs: 432.22/149.18 { U11(tt(), N, X, XS) -> 432.22/149.18 U12(splitAt(activate(N), activate(XS)), activate(X)) 432.22/149.18 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 432.22/149.18 , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS)) 432.22/149.18 , splitAt(0(), XS) -> pair(nil(), XS) 432.22/149.18 , activate(X) -> X 432.22/149.18 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.18 , afterNth(N, XS) -> snd(splitAt(N, XS)) 432.22/149.18 , snd(pair(X, Y)) -> Y 432.22/149.18 , and(tt(), X) -> activate(X) 432.22/149.18 , fst(pair(X, Y)) -> X 432.22/149.18 , head(cons(N, XS)) -> N 432.22/149.18 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.18 , natsFrom(X) -> n__natsFrom(X) 432.22/149.18 , sel(N, XS) -> head(afterNth(N, XS)) 432.22/149.18 , tail(cons(N, XS)) -> activate(XS) 432.22/149.18 , take(N, XS) -> fst(splitAt(N, XS)) } 432.22/149.18 Obligation: 432.22/149.18 innermost runtime complexity 432.22/149.18 Answer: 432.22/149.18 YES(O(1),O(n^1)) 432.22/149.18 432.22/149.18 Due to missing edges in the dependency-graph, the right-hand sides 432.22/149.18 of following rules could be simplified: 432.22/149.18 432.22/149.18 { U11^#(tt(), N, X, XS) -> 432.22/149.18 c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)), 432.22/149.18 splitAt^#(activate(N), activate(XS)), 432.22/149.18 activate^#(N), 432.22/149.18 activate^#(XS), 432.22/149.18 activate^#(X)) 432.22/149.18 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.18 c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS)) 432.22/149.18 , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 432.22/149.18 , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 432.22/149.18 , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 432.22/149.18 432.22/149.18 We are left with following problem, upon which TcT provides the 432.22/149.18 certificate YES(O(1),O(n^1)). 432.22/149.18 432.22/149.18 Strict DPs: 432.22/149.18 { U11^#(tt(), N, X, XS) -> 432.22/149.18 c_1(splitAt^#(activate(N), activate(XS))) 432.22/149.18 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.18 c_2(U11^#(tt(), N, X, activate(XS))) 432.22/149.18 , afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) 432.22/149.18 , sel^#(N, XS) -> c_4(afterNth^#(N, XS)) 432.22/149.18 , take^#(N, XS) -> c_5(splitAt^#(N, XS)) } 432.22/149.18 Weak Trs: 432.22/149.18 { U11(tt(), N, X, XS) -> 432.22/149.18 U12(splitAt(activate(N), activate(XS)), activate(X)) 432.22/149.18 , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 432.22/149.18 , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS)) 432.22/149.18 , splitAt(0(), XS) -> pair(nil(), XS) 432.22/149.18 , activate(X) -> X 432.22/149.18 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.18 , afterNth(N, XS) -> snd(splitAt(N, XS)) 432.22/149.18 , snd(pair(X, Y)) -> Y 432.22/149.18 , and(tt(), X) -> activate(X) 432.22/149.18 , fst(pair(X, Y)) -> X 432.22/149.18 , head(cons(N, XS)) -> N 432.22/149.18 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.18 , natsFrom(X) -> n__natsFrom(X) 432.22/149.18 , sel(N, XS) -> head(afterNth(N, XS)) 432.22/149.18 , tail(cons(N, XS)) -> activate(XS) 432.22/149.18 , take(N, XS) -> fst(splitAt(N, XS)) } 432.22/149.18 Obligation: 432.22/149.18 innermost runtime complexity 432.22/149.18 Answer: 432.22/149.18 YES(O(1),O(n^1)) 432.22/149.18 432.22/149.18 We replace rewrite rules by usable rules: 432.22/149.19 432.22/149.19 Weak Usable Rules: 432.22/149.19 { activate(X) -> X 432.22/149.19 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.19 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.19 , natsFrom(X) -> n__natsFrom(X) } 432.22/149.19 432.22/149.19 We are left with following problem, upon which TcT provides the 432.22/149.19 certificate YES(O(1),O(n^1)). 432.22/149.19 432.22/149.19 Strict DPs: 432.22/149.19 { U11^#(tt(), N, X, XS) -> 432.22/149.19 c_1(splitAt^#(activate(N), activate(XS))) 432.22/149.19 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) 432.22/149.19 , afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) 432.22/149.19 , sel^#(N, XS) -> c_4(afterNth^#(N, XS)) 432.22/149.19 , take^#(N, XS) -> c_5(splitAt^#(N, XS)) } 432.22/149.19 Weak Trs: 432.22/149.19 { activate(X) -> X 432.22/149.19 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.19 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.19 , natsFrom(X) -> n__natsFrom(X) } 432.22/149.19 Obligation: 432.22/149.19 innermost runtime complexity 432.22/149.19 Answer: 432.22/149.19 YES(O(1),O(n^1)) 432.22/149.19 432.22/149.19 Consider the dependency graph 432.22/149.19 432.22/149.19 1: U11^#(tt(), N, X, XS) -> 432.22/149.19 c_1(splitAt^#(activate(N), activate(XS))) 432.22/149.19 -->_1 splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) :2 432.22/149.19 432.22/149.19 2: splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) 432.22/149.19 -->_1 U11^#(tt(), N, X, XS) -> 432.22/149.19 c_1(splitAt^#(activate(N), activate(XS))) :1 432.22/149.19 432.22/149.19 3: afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) 432.22/149.19 -->_1 splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) :2 432.22/149.19 432.22/149.19 4: sel^#(N, XS) -> c_4(afterNth^#(N, XS)) 432.22/149.19 -->_1 afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) :3 432.22/149.19 432.22/149.19 5: take^#(N, XS) -> c_5(splitAt^#(N, XS)) 432.22/149.19 -->_1 splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) :2 432.22/149.19 432.22/149.19 432.22/149.19 Following roots of the dependency graph are removed, as the 432.22/149.19 considered set of starting terms is closed under reduction with 432.22/149.19 respect to these rules (modulo compound contexts). 432.22/149.19 432.22/149.19 { sel^#(N, XS) -> c_4(afterNth^#(N, XS)) 432.22/149.19 , take^#(N, XS) -> c_5(splitAt^#(N, XS)) } 432.22/149.19 432.22/149.19 432.22/149.19 We are left with following problem, upon which TcT provides the 432.22/149.19 certificate YES(O(1),O(n^1)). 432.22/149.19 432.22/149.19 Strict DPs: 432.22/149.19 { U11^#(tt(), N, X, XS) -> 432.22/149.19 c_1(splitAt^#(activate(N), activate(XS))) 432.22/149.19 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) 432.22/149.19 , afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) } 432.22/149.19 Weak Trs: 432.22/149.19 { activate(X) -> X 432.22/149.19 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.19 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.19 , natsFrom(X) -> n__natsFrom(X) } 432.22/149.19 Obligation: 432.22/149.19 innermost runtime complexity 432.22/149.19 Answer: 432.22/149.19 YES(O(1),O(n^1)) 432.22/149.19 432.22/149.19 Consider the dependency graph 432.22/149.19 432.22/149.19 1: U11^#(tt(), N, X, XS) -> 432.22/149.19 c_1(splitAt^#(activate(N), activate(XS))) 432.22/149.19 -->_1 splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) :2 432.22/149.19 432.22/149.19 2: splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) 432.22/149.19 -->_1 U11^#(tt(), N, X, XS) -> 432.22/149.19 c_1(splitAt^#(activate(N), activate(XS))) :1 432.22/149.19 432.22/149.19 3: afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) 432.22/149.19 -->_1 splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) :2 432.22/149.19 432.22/149.19 432.22/149.19 Following roots of the dependency graph are removed, as the 432.22/149.19 considered set of starting terms is closed under reduction with 432.22/149.19 respect to these rules (modulo compound contexts). 432.22/149.19 432.22/149.19 { afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) } 432.22/149.19 432.22/149.19 432.22/149.19 We are left with following problem, upon which TcT provides the 432.22/149.19 certificate YES(O(1),O(n^1)). 432.22/149.19 432.22/149.19 Strict DPs: 432.22/149.19 { U11^#(tt(), N, X, XS) -> 432.22/149.19 c_1(splitAt^#(activate(N), activate(XS))) 432.22/149.19 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) } 432.22/149.19 Weak Trs: 432.22/149.19 { activate(X) -> X 432.22/149.19 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.19 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.19 , natsFrom(X) -> n__natsFrom(X) } 432.22/149.19 Obligation: 432.22/149.19 innermost runtime complexity 432.22/149.19 Answer: 432.22/149.19 YES(O(1),O(n^1)) 432.22/149.19 432.22/149.19 We use the processor 'matrix interpretation of dimension 1' to 432.22/149.19 orient following rules strictly. 432.22/149.19 432.22/149.19 DPs: 432.22/149.19 { 2: splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) } 432.22/149.19 Trs: { natsFrom(N) -> cons(N, n__natsFrom(s(N))) } 432.22/149.19 432.22/149.19 Sub-proof: 432.22/149.19 ---------- 432.22/149.19 The following argument positions are usable: 432.22/149.19 Uargs(c_1) = {1}, Uargs(c_2) = {1} 432.22/149.19 432.22/149.19 TcT has computed the following constructor-based matrix 432.22/149.19 interpretation satisfying not(EDA). 432.22/149.19 432.22/149.19 [tt] = [0] 432.22/149.19 432.22/149.19 [activate](x1) = [1] x1 + [0] 432.22/149.19 432.22/149.19 [cons](x1, x2) = [1] x1 + [0] 432.22/149.19 432.22/149.19 [natsFrom](x1) = [1] x1 + [4] 432.22/149.19 432.22/149.19 [n__natsFrom](x1) = [1] x1 + [4] 432.22/149.19 432.22/149.19 [s](x1) = [1] x1 + [1] 432.22/149.19 432.22/149.19 [U11^#](x1, x2, x3, x4) = [1] x2 + [0] 432.22/149.19 432.22/149.19 [splitAt^#](x1, x2) = [1] x1 + [0] 432.22/149.19 432.22/149.19 [c_1](x1) = [1] x1 + [0] 432.22/149.19 432.22/149.19 [c_2](x1) = [1] x1 + [0] 432.22/149.19 432.22/149.19 The order satisfies the following ordering constraints: 432.22/149.19 432.22/149.19 [activate(X)] = [1] X + [0] 432.22/149.19 >= [1] X + [0] 432.22/149.19 = [X] 432.22/149.19 432.22/149.19 [activate(n__natsFrom(X))] = [1] X + [4] 432.22/149.19 >= [1] X + [4] 432.22/149.19 = [natsFrom(X)] 432.22/149.19 432.22/149.19 [natsFrom(N)] = [1] N + [4] 432.22/149.19 > [1] N + [0] 432.22/149.19 = [cons(N, n__natsFrom(s(N)))] 432.22/149.19 432.22/149.19 [natsFrom(X)] = [1] X + [4] 432.22/149.19 >= [1] X + [4] 432.22/149.19 = [n__natsFrom(X)] 432.22/149.19 432.22/149.19 [U11^#(tt(), N, X, XS)] = [1] N + [0] 432.22/149.19 >= [1] N + [0] 432.22/149.19 = [c_1(splitAt^#(activate(N), activate(XS)))] 432.22/149.19 432.22/149.19 [splitAt^#(s(N), cons(X, XS))] = [1] N + [1] 432.22/149.19 > [1] N + [0] 432.22/149.19 = [c_2(U11^#(tt(), N, X, activate(XS)))] 432.22/149.19 432.22/149.19 432.22/149.19 We return to the main proof. Consider the set of all dependency 432.22/149.19 pairs 432.22/149.19 432.22/149.19 : 432.22/149.19 { 1: U11^#(tt(), N, X, XS) -> 432.22/149.19 c_1(splitAt^#(activate(N), activate(XS))) 432.22/149.19 , 2: splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) } 432.22/149.19 432.22/149.19 Processor 'matrix interpretation of dimension 1' induces the 432.22/149.19 complexity certificate YES(?,O(n^1)) on application of dependency 432.22/149.19 pairs {2}. These cover all (indirect) predecessors of dependency 432.22/149.19 pairs {1,2}, their number of application is equally bounded. The 432.22/149.19 dependency pairs are shifted into the weak component. 432.22/149.19 432.22/149.19 We are left with following problem, upon which TcT provides the 432.22/149.19 certificate YES(O(1),O(1)). 432.22/149.19 432.22/149.19 Weak DPs: 432.22/149.19 { U11^#(tt(), N, X, XS) -> 432.22/149.19 c_1(splitAt^#(activate(N), activate(XS))) 432.22/149.19 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) } 432.22/149.19 Weak Trs: 432.22/149.19 { activate(X) -> X 432.22/149.19 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.19 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.19 , natsFrom(X) -> n__natsFrom(X) } 432.22/149.19 Obligation: 432.22/149.19 innermost runtime complexity 432.22/149.19 Answer: 432.22/149.19 YES(O(1),O(1)) 432.22/149.19 432.22/149.19 The following weak DPs constitute a sub-graph of the DG that is 432.22/149.19 closed under successors. The DPs are removed. 432.22/149.19 432.22/149.19 { U11^#(tt(), N, X, XS) -> 432.22/149.19 c_1(splitAt^#(activate(N), activate(XS))) 432.22/149.19 , splitAt^#(s(N), cons(X, XS)) -> 432.22/149.19 c_2(U11^#(tt(), N, X, activate(XS))) } 432.22/149.19 432.22/149.19 We are left with following problem, upon which TcT provides the 432.22/149.19 certificate YES(O(1),O(1)). 432.22/149.19 432.22/149.19 Weak Trs: 432.22/149.19 { activate(X) -> X 432.22/149.19 , activate(n__natsFrom(X)) -> natsFrom(X) 432.22/149.19 , natsFrom(N) -> cons(N, n__natsFrom(s(N))) 432.22/149.19 , natsFrom(X) -> n__natsFrom(X) } 432.22/149.19 Obligation: 432.22/149.19 innermost runtime complexity 432.22/149.19 Answer: 432.22/149.19 YES(O(1),O(1)) 432.22/149.19 432.22/149.19 No rule is usable, rules are removed from the input problem. 432.22/149.19 432.22/149.19 We are left with following problem, upon which TcT provides the 432.22/149.19 certificate YES(O(1),O(1)). 432.22/149.19 432.22/149.19 Rules: Empty 432.22/149.19 Obligation: 432.22/149.19 innermost runtime complexity 432.22/149.19 Answer: 432.22/149.19 YES(O(1),O(1)) 432.22/149.19 432.22/149.19 Empty rules are trivially bounded 432.22/149.19 432.22/149.19 Hurray, we answered YES(O(1),O(n^1)) 432.86/149.55 EOF