YES(O(1),O(n^1)) 3.26/1.24 YES(O(1),O(n^1)) 3.26/1.24 3.26/1.24 We are left with following problem, upon which TcT provides the 3.26/1.24 certificate YES(O(1),O(n^1)). 3.26/1.24 3.26/1.24 Strict Trs: 3.26/1.24 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.24 , natsFrom(X) -> n__natsFrom(X) 3.26/1.24 , fst(pair(XS, YS)) -> XS 3.26/1.24 , snd(pair(XS, YS)) -> YS 3.26/1.24 , splitAt(s(N), cons(X, XS)) -> 3.26/1.24 u(splitAt(N, activate(XS)), N, X, activate(XS)) 3.26/1.24 , splitAt(0(), XS) -> pair(nil(), XS) 3.26/1.24 , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS) 3.26/1.24 , activate(X) -> X 3.26/1.24 , activate(n__natsFrom(X)) -> natsFrom(X) 3.26/1.24 , head(cons(N, XS)) -> N 3.26/1.24 , tail(cons(N, XS)) -> activate(XS) 3.26/1.24 , sel(N, XS) -> head(afterNth(N, XS)) 3.26/1.24 , afterNth(N, XS) -> snd(splitAt(N, XS)) 3.26/1.24 , take(N, XS) -> fst(splitAt(N, XS)) } 3.26/1.24 Obligation: 3.26/1.24 innermost runtime complexity 3.26/1.24 Answer: 3.26/1.24 YES(O(1),O(n^1)) 3.26/1.24 3.26/1.24 We add the following dependency tuples: 3.26/1.24 3.26/1.24 Strict DPs: 3.26/1.24 { natsFrom^#(N) -> c_1() 3.26/1.24 , natsFrom^#(X) -> c_2() 3.26/1.24 , fst^#(pair(XS, YS)) -> c_3() 3.26/1.24 , snd^#(pair(XS, YS)) -> c_4() 3.26/1.24 , splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_5(u^#(splitAt(N, activate(XS)), N, X, activate(XS)), 3.26/1.24 splitAt^#(N, activate(XS)), 3.26/1.24 activate^#(XS), 3.26/1.24 activate^#(XS)) 3.26/1.24 , splitAt^#(0(), XS) -> c_6() 3.26/1.24 , u^#(pair(YS, ZS), N, X, XS) -> c_7(activate^#(X)) 3.26/1.24 , activate^#(X) -> c_8() 3.26/1.24 , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(X)) 3.26/1.24 , head^#(cons(N, XS)) -> c_10() 3.26/1.24 , tail^#(cons(N, XS)) -> c_11(activate^#(XS)) 3.26/1.24 , sel^#(N, XS) -> c_12(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 3.26/1.24 , afterNth^#(N, XS) -> 3.26/1.24 c_13(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , take^#(N, XS) -> c_14(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 3.26/1.24 3.26/1.24 and mark the set of starting terms. 3.26/1.24 3.26/1.24 We are left with following problem, upon which TcT provides the 3.26/1.24 certificate YES(O(1),O(n^1)). 3.26/1.24 3.26/1.24 Strict DPs: 3.26/1.24 { natsFrom^#(N) -> c_1() 3.26/1.24 , natsFrom^#(X) -> c_2() 3.26/1.24 , fst^#(pair(XS, YS)) -> c_3() 3.26/1.24 , snd^#(pair(XS, YS)) -> c_4() 3.26/1.24 , splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_5(u^#(splitAt(N, activate(XS)), N, X, activate(XS)), 3.26/1.24 splitAt^#(N, activate(XS)), 3.26/1.24 activate^#(XS), 3.26/1.24 activate^#(XS)) 3.26/1.24 , splitAt^#(0(), XS) -> c_6() 3.26/1.24 , u^#(pair(YS, ZS), N, X, XS) -> c_7(activate^#(X)) 3.26/1.24 , activate^#(X) -> c_8() 3.26/1.24 , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(X)) 3.26/1.24 , head^#(cons(N, XS)) -> c_10() 3.26/1.24 , tail^#(cons(N, XS)) -> c_11(activate^#(XS)) 3.26/1.24 , sel^#(N, XS) -> c_12(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 3.26/1.24 , afterNth^#(N, XS) -> 3.26/1.24 c_13(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , take^#(N, XS) -> c_14(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 3.26/1.24 Weak Trs: 3.26/1.24 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.24 , natsFrom(X) -> n__natsFrom(X) 3.26/1.24 , fst(pair(XS, YS)) -> XS 3.26/1.24 , snd(pair(XS, YS)) -> YS 3.26/1.24 , splitAt(s(N), cons(X, XS)) -> 3.26/1.24 u(splitAt(N, activate(XS)), N, X, activate(XS)) 3.26/1.24 , splitAt(0(), XS) -> pair(nil(), XS) 3.26/1.24 , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS) 3.26/1.24 , activate(X) -> X 3.26/1.24 , activate(n__natsFrom(X)) -> natsFrom(X) 3.26/1.24 , head(cons(N, XS)) -> N 3.26/1.24 , tail(cons(N, XS)) -> activate(XS) 3.26/1.24 , sel(N, XS) -> head(afterNth(N, XS)) 3.26/1.24 , afterNth(N, XS) -> snd(splitAt(N, XS)) 3.26/1.24 , take(N, XS) -> fst(splitAt(N, XS)) } 3.26/1.24 Obligation: 3.26/1.24 innermost runtime complexity 3.26/1.24 Answer: 3.26/1.24 YES(O(1),O(n^1)) 3.26/1.24 3.26/1.24 We estimate the number of application of {1,2,3,4,6,8,10} by 3.26/1.24 applications of Pre({1,2,3,4,6,8,10}) = {5,7,9,11,12,13,14}. Here 3.26/1.24 rules are labeled as follows: 3.26/1.24 3.26/1.24 DPs: 3.26/1.24 { 1: natsFrom^#(N) -> c_1() 3.26/1.24 , 2: natsFrom^#(X) -> c_2() 3.26/1.24 , 3: fst^#(pair(XS, YS)) -> c_3() 3.26/1.24 , 4: snd^#(pair(XS, YS)) -> c_4() 3.26/1.24 , 5: splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_5(u^#(splitAt(N, activate(XS)), N, X, activate(XS)), 3.26/1.24 splitAt^#(N, activate(XS)), 3.26/1.24 activate^#(XS), 3.26/1.24 activate^#(XS)) 3.26/1.24 , 6: splitAt^#(0(), XS) -> c_6() 3.26/1.24 , 7: u^#(pair(YS, ZS), N, X, XS) -> c_7(activate^#(X)) 3.26/1.24 , 8: activate^#(X) -> c_8() 3.26/1.24 , 9: activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(X)) 3.26/1.24 , 10: head^#(cons(N, XS)) -> c_10() 3.26/1.24 , 11: tail^#(cons(N, XS)) -> c_11(activate^#(XS)) 3.26/1.24 , 12: sel^#(N, XS) -> 3.26/1.24 c_12(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 3.26/1.24 , 13: afterNth^#(N, XS) -> 3.26/1.24 c_13(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , 14: take^#(N, XS) -> 3.26/1.24 c_14(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 3.26/1.24 3.26/1.24 We are left with following problem, upon which TcT provides the 3.26/1.24 certificate YES(O(1),O(n^1)). 3.26/1.24 3.26/1.24 Strict DPs: 3.26/1.24 { splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_5(u^#(splitAt(N, activate(XS)), N, X, activate(XS)), 3.26/1.24 splitAt^#(N, activate(XS)), 3.26/1.24 activate^#(XS), 3.26/1.24 activate^#(XS)) 3.26/1.24 , u^#(pair(YS, ZS), N, X, XS) -> c_7(activate^#(X)) 3.26/1.24 , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(X)) 3.26/1.24 , tail^#(cons(N, XS)) -> c_11(activate^#(XS)) 3.26/1.24 , sel^#(N, XS) -> c_12(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 3.26/1.24 , afterNth^#(N, XS) -> 3.26/1.24 c_13(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , take^#(N, XS) -> c_14(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 3.26/1.24 Weak DPs: 3.26/1.24 { natsFrom^#(N) -> c_1() 3.26/1.24 , natsFrom^#(X) -> c_2() 3.26/1.24 , fst^#(pair(XS, YS)) -> c_3() 3.26/1.24 , snd^#(pair(XS, YS)) -> c_4() 3.26/1.24 , splitAt^#(0(), XS) -> c_6() 3.26/1.24 , activate^#(X) -> c_8() 3.26/1.24 , head^#(cons(N, XS)) -> c_10() } 3.26/1.24 Weak Trs: 3.26/1.24 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.24 , natsFrom(X) -> n__natsFrom(X) 3.26/1.24 , fst(pair(XS, YS)) -> XS 3.26/1.24 , snd(pair(XS, YS)) -> YS 3.26/1.24 , splitAt(s(N), cons(X, XS)) -> 3.26/1.24 u(splitAt(N, activate(XS)), N, X, activate(XS)) 3.26/1.24 , splitAt(0(), XS) -> pair(nil(), XS) 3.26/1.24 , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS) 3.26/1.24 , activate(X) -> X 3.26/1.24 , activate(n__natsFrom(X)) -> natsFrom(X) 3.26/1.24 , head(cons(N, XS)) -> N 3.26/1.24 , tail(cons(N, XS)) -> activate(XS) 3.26/1.24 , sel(N, XS) -> head(afterNth(N, XS)) 3.26/1.24 , afterNth(N, XS) -> snd(splitAt(N, XS)) 3.26/1.24 , take(N, XS) -> fst(splitAt(N, XS)) } 3.26/1.24 Obligation: 3.26/1.24 innermost runtime complexity 3.26/1.24 Answer: 3.26/1.24 YES(O(1),O(n^1)) 3.26/1.24 3.26/1.24 We estimate the number of application of {3} by applications of 3.26/1.24 Pre({3}) = {1,2,4}. Here rules are labeled as follows: 3.26/1.24 3.26/1.24 DPs: 3.26/1.24 { 1: splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_5(u^#(splitAt(N, activate(XS)), N, X, activate(XS)), 3.26/1.24 splitAt^#(N, activate(XS)), 3.26/1.24 activate^#(XS), 3.26/1.24 activate^#(XS)) 3.26/1.24 , 2: u^#(pair(YS, ZS), N, X, XS) -> c_7(activate^#(X)) 3.26/1.24 , 3: activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(X)) 3.26/1.24 , 4: tail^#(cons(N, XS)) -> c_11(activate^#(XS)) 3.26/1.24 , 5: sel^#(N, XS) -> 3.26/1.24 c_12(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 3.26/1.24 , 6: afterNth^#(N, XS) -> 3.26/1.24 c_13(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , 7: take^#(N, XS) -> c_14(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , 8: natsFrom^#(N) -> c_1() 3.26/1.24 , 9: natsFrom^#(X) -> c_2() 3.26/1.24 , 10: fst^#(pair(XS, YS)) -> c_3() 3.26/1.24 , 11: snd^#(pair(XS, YS)) -> c_4() 3.26/1.24 , 12: splitAt^#(0(), XS) -> c_6() 3.26/1.24 , 13: activate^#(X) -> c_8() 3.26/1.24 , 14: head^#(cons(N, XS)) -> c_10() } 3.26/1.24 3.26/1.24 We are left with following problem, upon which TcT provides the 3.26/1.24 certificate YES(O(1),O(n^1)). 3.26/1.24 3.26/1.24 Strict DPs: 3.26/1.24 { splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_5(u^#(splitAt(N, activate(XS)), N, X, activate(XS)), 3.26/1.24 splitAt^#(N, activate(XS)), 3.26/1.24 activate^#(XS), 3.26/1.24 activate^#(XS)) 3.26/1.24 , u^#(pair(YS, ZS), N, X, XS) -> c_7(activate^#(X)) 3.26/1.24 , tail^#(cons(N, XS)) -> c_11(activate^#(XS)) 3.26/1.24 , sel^#(N, XS) -> c_12(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 3.26/1.24 , afterNth^#(N, XS) -> 3.26/1.24 c_13(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , take^#(N, XS) -> c_14(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 3.26/1.24 Weak DPs: 3.26/1.24 { natsFrom^#(N) -> c_1() 3.26/1.24 , natsFrom^#(X) -> c_2() 3.26/1.24 , fst^#(pair(XS, YS)) -> c_3() 3.26/1.24 , snd^#(pair(XS, YS)) -> c_4() 3.26/1.24 , splitAt^#(0(), XS) -> c_6() 3.26/1.24 , activate^#(X) -> c_8() 3.26/1.24 , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(X)) 3.26/1.24 , head^#(cons(N, XS)) -> c_10() } 3.26/1.24 Weak Trs: 3.26/1.24 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.24 , natsFrom(X) -> n__natsFrom(X) 3.26/1.24 , fst(pair(XS, YS)) -> XS 3.26/1.24 , snd(pair(XS, YS)) -> YS 3.26/1.24 , splitAt(s(N), cons(X, XS)) -> 3.26/1.24 u(splitAt(N, activate(XS)), N, X, activate(XS)) 3.26/1.24 , splitAt(0(), XS) -> pair(nil(), XS) 3.26/1.24 , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS) 3.26/1.24 , activate(X) -> X 3.26/1.24 , activate(n__natsFrom(X)) -> natsFrom(X) 3.26/1.24 , head(cons(N, XS)) -> N 3.26/1.24 , tail(cons(N, XS)) -> activate(XS) 3.26/1.24 , sel(N, XS) -> head(afterNth(N, XS)) 3.26/1.24 , afterNth(N, XS) -> snd(splitAt(N, XS)) 3.26/1.24 , take(N, XS) -> fst(splitAt(N, XS)) } 3.26/1.24 Obligation: 3.26/1.24 innermost runtime complexity 3.26/1.24 Answer: 3.26/1.24 YES(O(1),O(n^1)) 3.26/1.24 3.26/1.24 We estimate the number of application of {2,3} by applications of 3.26/1.24 Pre({2,3}) = {1}. Here rules are labeled as follows: 3.26/1.24 3.26/1.24 DPs: 3.26/1.24 { 1: splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_5(u^#(splitAt(N, activate(XS)), N, X, activate(XS)), 3.26/1.24 splitAt^#(N, activate(XS)), 3.26/1.24 activate^#(XS), 3.26/1.24 activate^#(XS)) 3.26/1.24 , 2: u^#(pair(YS, ZS), N, X, XS) -> c_7(activate^#(X)) 3.26/1.24 , 3: tail^#(cons(N, XS)) -> c_11(activate^#(XS)) 3.26/1.24 , 4: sel^#(N, XS) -> 3.26/1.24 c_12(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 3.26/1.24 , 5: afterNth^#(N, XS) -> 3.26/1.24 c_13(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , 6: take^#(N, XS) -> c_14(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , 7: natsFrom^#(N) -> c_1() 3.26/1.24 , 8: natsFrom^#(X) -> c_2() 3.26/1.24 , 9: fst^#(pair(XS, YS)) -> c_3() 3.26/1.24 , 10: snd^#(pair(XS, YS)) -> c_4() 3.26/1.24 , 11: splitAt^#(0(), XS) -> c_6() 3.26/1.24 , 12: activate^#(X) -> c_8() 3.26/1.24 , 13: activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(X)) 3.26/1.24 , 14: head^#(cons(N, XS)) -> c_10() } 3.26/1.24 3.26/1.24 We are left with following problem, upon which TcT provides the 3.26/1.24 certificate YES(O(1),O(n^1)). 3.26/1.24 3.26/1.24 Strict DPs: 3.26/1.24 { splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_5(u^#(splitAt(N, activate(XS)), N, X, activate(XS)), 3.26/1.24 splitAt^#(N, activate(XS)), 3.26/1.24 activate^#(XS), 3.26/1.24 activate^#(XS)) 3.26/1.24 , sel^#(N, XS) -> c_12(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 3.26/1.24 , afterNth^#(N, XS) -> 3.26/1.24 c_13(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , take^#(N, XS) -> c_14(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 3.26/1.24 Weak DPs: 3.26/1.24 { natsFrom^#(N) -> c_1() 3.26/1.24 , natsFrom^#(X) -> c_2() 3.26/1.24 , fst^#(pair(XS, YS)) -> c_3() 3.26/1.24 , snd^#(pair(XS, YS)) -> c_4() 3.26/1.24 , splitAt^#(0(), XS) -> c_6() 3.26/1.24 , u^#(pair(YS, ZS), N, X, XS) -> c_7(activate^#(X)) 3.26/1.24 , activate^#(X) -> c_8() 3.26/1.24 , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(X)) 3.26/1.24 , head^#(cons(N, XS)) -> c_10() 3.26/1.24 , tail^#(cons(N, XS)) -> c_11(activate^#(XS)) } 3.26/1.24 Weak Trs: 3.26/1.24 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.24 , natsFrom(X) -> n__natsFrom(X) 3.26/1.24 , fst(pair(XS, YS)) -> XS 3.26/1.24 , snd(pair(XS, YS)) -> YS 3.26/1.24 , splitAt(s(N), cons(X, XS)) -> 3.26/1.24 u(splitAt(N, activate(XS)), N, X, activate(XS)) 3.26/1.24 , splitAt(0(), XS) -> pair(nil(), XS) 3.26/1.24 , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS) 3.26/1.24 , activate(X) -> X 3.26/1.24 , activate(n__natsFrom(X)) -> natsFrom(X) 3.26/1.24 , head(cons(N, XS)) -> N 3.26/1.24 , tail(cons(N, XS)) -> activate(XS) 3.26/1.24 , sel(N, XS) -> head(afterNth(N, XS)) 3.26/1.24 , afterNth(N, XS) -> snd(splitAt(N, XS)) 3.26/1.24 , take(N, XS) -> fst(splitAt(N, XS)) } 3.26/1.24 Obligation: 3.26/1.24 innermost runtime complexity 3.26/1.24 Answer: 3.26/1.24 YES(O(1),O(n^1)) 3.26/1.24 3.26/1.24 The following weak DPs constitute a sub-graph of the DG that is 3.26/1.24 closed under successors. The DPs are removed. 3.26/1.24 3.26/1.24 { natsFrom^#(N) -> c_1() 3.26/1.24 , natsFrom^#(X) -> c_2() 3.26/1.24 , fst^#(pair(XS, YS)) -> c_3() 3.26/1.24 , snd^#(pair(XS, YS)) -> c_4() 3.26/1.24 , splitAt^#(0(), XS) -> c_6() 3.26/1.24 , u^#(pair(YS, ZS), N, X, XS) -> c_7(activate^#(X)) 3.26/1.24 , activate^#(X) -> c_8() 3.26/1.24 , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(X)) 3.26/1.24 , head^#(cons(N, XS)) -> c_10() 3.26/1.24 , tail^#(cons(N, XS)) -> c_11(activate^#(XS)) } 3.26/1.24 3.26/1.24 We are left with following problem, upon which TcT provides the 3.26/1.24 certificate YES(O(1),O(n^1)). 3.26/1.24 3.26/1.24 Strict DPs: 3.26/1.24 { splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_5(u^#(splitAt(N, activate(XS)), N, X, activate(XS)), 3.26/1.24 splitAt^#(N, activate(XS)), 3.26/1.24 activate^#(XS), 3.26/1.24 activate^#(XS)) 3.26/1.24 , sel^#(N, XS) -> c_12(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 3.26/1.24 , afterNth^#(N, XS) -> 3.26/1.24 c_13(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , take^#(N, XS) -> c_14(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 3.26/1.24 Weak Trs: 3.26/1.24 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.24 , natsFrom(X) -> n__natsFrom(X) 3.26/1.24 , fst(pair(XS, YS)) -> XS 3.26/1.24 , snd(pair(XS, YS)) -> YS 3.26/1.24 , splitAt(s(N), cons(X, XS)) -> 3.26/1.24 u(splitAt(N, activate(XS)), N, X, activate(XS)) 3.26/1.24 , splitAt(0(), XS) -> pair(nil(), XS) 3.26/1.24 , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS) 3.26/1.24 , activate(X) -> X 3.26/1.24 , activate(n__natsFrom(X)) -> natsFrom(X) 3.26/1.24 , head(cons(N, XS)) -> N 3.26/1.24 , tail(cons(N, XS)) -> activate(XS) 3.26/1.24 , sel(N, XS) -> head(afterNth(N, XS)) 3.26/1.24 , afterNth(N, XS) -> snd(splitAt(N, XS)) 3.26/1.24 , take(N, XS) -> fst(splitAt(N, XS)) } 3.26/1.24 Obligation: 3.26/1.24 innermost runtime complexity 3.26/1.24 Answer: 3.26/1.24 YES(O(1),O(n^1)) 3.26/1.24 3.26/1.24 Due to missing edges in the dependency-graph, the right-hand sides 3.26/1.24 of following rules could be simplified: 3.26/1.24 3.26/1.24 { splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_5(u^#(splitAt(N, activate(XS)), N, X, activate(XS)), 3.26/1.24 splitAt^#(N, activate(XS)), 3.26/1.24 activate^#(XS), 3.26/1.24 activate^#(XS)) 3.26/1.24 , sel^#(N, XS) -> c_12(head^#(afterNth(N, XS)), afterNth^#(N, XS)) 3.26/1.24 , afterNth^#(N, XS) -> 3.26/1.24 c_13(snd^#(splitAt(N, XS)), splitAt^#(N, XS)) 3.26/1.24 , take^#(N, XS) -> c_14(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) } 3.26/1.24 3.26/1.24 We are left with following problem, upon which TcT provides the 3.26/1.24 certificate YES(O(1),O(n^1)). 3.26/1.24 3.26/1.24 Strict DPs: 3.26/1.24 { splitAt^#(s(N), cons(X, XS)) -> c_1(splitAt^#(N, activate(XS))) 3.26/1.24 , sel^#(N, XS) -> c_2(afterNth^#(N, XS)) 3.26/1.24 , afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) 3.26/1.24 , take^#(N, XS) -> c_4(splitAt^#(N, XS)) } 3.26/1.24 Weak Trs: 3.26/1.24 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.24 , natsFrom(X) -> n__natsFrom(X) 3.26/1.24 , fst(pair(XS, YS)) -> XS 3.26/1.24 , snd(pair(XS, YS)) -> YS 3.26/1.24 , splitAt(s(N), cons(X, XS)) -> 3.26/1.24 u(splitAt(N, activate(XS)), N, X, activate(XS)) 3.26/1.24 , splitAt(0(), XS) -> pair(nil(), XS) 3.26/1.24 , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS) 3.26/1.24 , activate(X) -> X 3.26/1.24 , activate(n__natsFrom(X)) -> natsFrom(X) 3.26/1.24 , head(cons(N, XS)) -> N 3.26/1.24 , tail(cons(N, XS)) -> activate(XS) 3.26/1.24 , sel(N, XS) -> head(afterNth(N, XS)) 3.26/1.24 , afterNth(N, XS) -> snd(splitAt(N, XS)) 3.26/1.24 , take(N, XS) -> fst(splitAt(N, XS)) } 3.26/1.24 Obligation: 3.26/1.24 innermost runtime complexity 3.26/1.24 Answer: 3.26/1.24 YES(O(1),O(n^1)) 3.26/1.24 3.26/1.24 We replace rewrite rules by usable rules: 3.26/1.24 3.26/1.24 Weak Usable Rules: 3.26/1.24 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.24 , natsFrom(X) -> n__natsFrom(X) 3.26/1.24 , activate(X) -> X 3.26/1.24 , activate(n__natsFrom(X)) -> natsFrom(X) } 3.26/1.24 3.26/1.24 We are left with following problem, upon which TcT provides the 3.26/1.24 certificate YES(O(1),O(n^1)). 3.26/1.24 3.26/1.24 Strict DPs: 3.26/1.24 { splitAt^#(s(N), cons(X, XS)) -> c_1(splitAt^#(N, activate(XS))) 3.26/1.24 , sel^#(N, XS) -> c_2(afterNth^#(N, XS)) 3.26/1.24 , afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) 3.26/1.24 , take^#(N, XS) -> c_4(splitAt^#(N, XS)) } 3.26/1.24 Weak Trs: 3.26/1.24 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.24 , natsFrom(X) -> n__natsFrom(X) 3.26/1.24 , activate(X) -> X 3.26/1.24 , activate(n__natsFrom(X)) -> natsFrom(X) } 3.26/1.24 Obligation: 3.26/1.24 innermost runtime complexity 3.26/1.24 Answer: 3.26/1.24 YES(O(1),O(n^1)) 3.26/1.24 3.26/1.24 Consider the dependency graph 3.26/1.24 3.26/1.24 1: splitAt^#(s(N), cons(X, XS)) -> c_1(splitAt^#(N, activate(XS))) 3.26/1.24 -->_1 splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_1(splitAt^#(N, activate(XS))) :1 3.26/1.24 3.26/1.24 2: sel^#(N, XS) -> c_2(afterNth^#(N, XS)) 3.26/1.24 -->_1 afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) :3 3.26/1.24 3.26/1.24 3: afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) 3.26/1.24 -->_1 splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_1(splitAt^#(N, activate(XS))) :1 3.26/1.24 3.26/1.24 4: take^#(N, XS) -> c_4(splitAt^#(N, XS)) 3.26/1.24 -->_1 splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_1(splitAt^#(N, activate(XS))) :1 3.26/1.24 3.26/1.24 3.26/1.24 Following roots of the dependency graph are removed, as the 3.26/1.24 considered set of starting terms is closed under reduction with 3.26/1.24 respect to these rules (modulo compound contexts). 3.26/1.24 3.26/1.24 { sel^#(N, XS) -> c_2(afterNth^#(N, XS)) 3.26/1.24 , take^#(N, XS) -> c_4(splitAt^#(N, XS)) } 3.26/1.24 3.26/1.24 3.26/1.24 We are left with following problem, upon which TcT provides the 3.26/1.24 certificate YES(O(1),O(n^1)). 3.26/1.24 3.26/1.24 Strict DPs: 3.26/1.24 { splitAt^#(s(N), cons(X, XS)) -> c_1(splitAt^#(N, activate(XS))) 3.26/1.24 , afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) } 3.26/1.24 Weak Trs: 3.26/1.24 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.24 , natsFrom(X) -> n__natsFrom(X) 3.26/1.24 , activate(X) -> X 3.26/1.24 , activate(n__natsFrom(X)) -> natsFrom(X) } 3.26/1.24 Obligation: 3.26/1.24 innermost runtime complexity 3.26/1.24 Answer: 3.26/1.24 YES(O(1),O(n^1)) 3.26/1.24 3.26/1.24 Consider the dependency graph 3.26/1.24 3.26/1.24 1: splitAt^#(s(N), cons(X, XS)) -> c_1(splitAt^#(N, activate(XS))) 3.26/1.24 -->_1 splitAt^#(s(N), cons(X, XS)) -> 3.26/1.24 c_1(splitAt^#(N, activate(XS))) :1 3.26/1.24 3.26/1.24 2: afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) 3.26/1.25 -->_1 splitAt^#(s(N), cons(X, XS)) -> 3.26/1.25 c_1(splitAt^#(N, activate(XS))) :1 3.26/1.25 3.26/1.25 3.26/1.25 Following roots of the dependency graph are removed, as the 3.26/1.25 considered set of starting terms is closed under reduction with 3.26/1.25 respect to these rules (modulo compound contexts). 3.26/1.25 3.26/1.25 { afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) } 3.26/1.25 3.26/1.25 3.26/1.25 We are left with following problem, upon which TcT provides the 3.26/1.25 certificate YES(O(1),O(n^1)). 3.26/1.25 3.26/1.25 Strict DPs: 3.26/1.25 { splitAt^#(s(N), cons(X, XS)) -> c_1(splitAt^#(N, activate(XS))) } 3.26/1.25 Weak Trs: 3.26/1.25 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.25 , natsFrom(X) -> n__natsFrom(X) 3.26/1.25 , activate(X) -> X 3.26/1.25 , activate(n__natsFrom(X)) -> natsFrom(X) } 3.26/1.25 Obligation: 3.26/1.25 innermost runtime complexity 3.26/1.25 Answer: 3.26/1.25 YES(O(1),O(n^1)) 3.26/1.25 3.26/1.25 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 3.26/1.25 to orient following rules strictly. 3.26/1.25 3.26/1.25 DPs: 3.26/1.25 { 1: splitAt^#(s(N), cons(X, XS)) -> 3.26/1.25 c_1(splitAt^#(N, activate(XS))) } 3.26/1.25 Trs: { natsFrom(X) -> n__natsFrom(X) } 3.26/1.25 3.26/1.25 Sub-proof: 3.26/1.25 ---------- 3.26/1.25 The input was oriented with the instance of 'Small Polynomial Path 3.26/1.25 Order (PS,1-bounded)' as induced by the safe mapping 3.26/1.25 3.26/1.25 safe(natsFrom) = {1}, safe(cons) = {1, 2}, safe(n__natsFrom) = {1}, 3.26/1.25 safe(s) = {1}, safe(activate) = {}, safe(splitAt^#) = {2}, 3.26/1.25 safe(c_1) = {} 3.26/1.25 3.26/1.25 and precedence 3.26/1.25 3.26/1.25 natsFrom ~ activate, natsFrom ~ splitAt^#, activate ~ splitAt^# . 3.26/1.25 3.26/1.25 Following symbols are considered recursive: 3.26/1.25 3.26/1.25 {natsFrom, activate, splitAt^#} 3.26/1.25 3.26/1.25 The recursion depth is 1. 3.26/1.25 3.26/1.25 Further, following argument filtering is employed: 3.26/1.25 3.26/1.25 pi(natsFrom) = [], pi(cons) = [], pi(n__natsFrom) = [], 3.26/1.25 pi(s) = [1], pi(activate) = [], pi(splitAt^#) = [1], pi(c_1) = [1] 3.26/1.25 3.26/1.25 Usable defined function symbols are a subset of: 3.26/1.25 3.26/1.25 {splitAt^#} 3.26/1.25 3.26/1.25 For your convenience, here are the satisfied ordering constraints: 3.26/1.25 3.26/1.25 pi(splitAt^#(s(N), cons(X, XS))) = splitAt^#(s(; N);) 3.26/1.25 > c_1(splitAt^#(N;);) 3.26/1.25 = pi(c_1(splitAt^#(N, activate(XS)))) 3.26/1.25 3.26/1.25 3.26/1.25 The strictly oriented rules are moved into the weak component. 3.26/1.25 3.26/1.25 We are left with following problem, upon which TcT provides the 3.26/1.25 certificate YES(O(1),O(1)). 3.26/1.25 3.26/1.25 Weak DPs: 3.26/1.25 { splitAt^#(s(N), cons(X, XS)) -> c_1(splitAt^#(N, activate(XS))) } 3.26/1.25 Weak Trs: 3.26/1.25 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.25 , natsFrom(X) -> n__natsFrom(X) 3.26/1.25 , activate(X) -> X 3.26/1.25 , activate(n__natsFrom(X)) -> natsFrom(X) } 3.26/1.25 Obligation: 3.26/1.25 innermost runtime complexity 3.26/1.25 Answer: 3.26/1.25 YES(O(1),O(1)) 3.26/1.25 3.26/1.25 The following weak DPs constitute a sub-graph of the DG that is 3.26/1.25 closed under successors. The DPs are removed. 3.26/1.25 3.26/1.25 { splitAt^#(s(N), cons(X, XS)) -> c_1(splitAt^#(N, activate(XS))) } 3.26/1.25 3.26/1.25 We are left with following problem, upon which TcT provides the 3.26/1.25 certificate YES(O(1),O(1)). 3.26/1.25 3.26/1.25 Weak Trs: 3.26/1.25 { natsFrom(N) -> cons(N, n__natsFrom(s(N))) 3.26/1.25 , natsFrom(X) -> n__natsFrom(X) 3.26/1.25 , activate(X) -> X 3.26/1.25 , activate(n__natsFrom(X)) -> natsFrom(X) } 3.26/1.25 Obligation: 3.26/1.25 innermost runtime complexity 3.26/1.25 Answer: 3.26/1.25 YES(O(1),O(1)) 3.26/1.25 3.26/1.25 No rule is usable, rules are removed from the input problem. 3.26/1.25 3.26/1.25 We are left with following problem, upon which TcT provides the 3.26/1.25 certificate YES(O(1),O(1)). 3.26/1.25 3.26/1.25 Rules: Empty 3.26/1.25 Obligation: 3.26/1.25 innermost runtime complexity 3.26/1.25 Answer: 3.26/1.25 YES(O(1),O(1)) 3.26/1.25 3.26/1.25 Empty rules are trivially bounded 3.26/1.25 3.26/1.25 Hurray, we answered YES(O(1),O(n^1)) 3.26/1.25 EOF