WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__incr(X)) -> incr(activate(X)) activate(n__oddNs()) -> oddNs() activate(n__repItems(X)) -> repItems(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zip(X1,X2)) -> zip(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) incr(X) -> n__incr(X) incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS))) oddNs() -> incr(pairNs()) oddNs() -> n__oddNs() pairNs() -> cons(0(),n__incr(n__oddNs())) repItems(X) -> n__repItems(X) repItems(cons(X,XS)) -> cons(X,n__cons(X,n__repItems(activate(XS)))) repItems(nil()) -> nil() tail(cons(X,XS)) -> activate(XS) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) zip(X,nil()) -> nil() zip(X1,X2) -> n__zip(X1,X2) zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),n__zip(activate(XS),activate(YS))) zip(nil(),XS) -> nil() - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2} / {0/0,n__cons/2,n__incr/1 ,n__oddNs/0,n__repItems/1,n__take/2,n__zip/2,nil/0,pair/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,cons,incr,oddNs,pairNs,repItems,tail,take ,zip} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__incr(X)) -> incr(activate(X)) activate(n__oddNs()) -> oddNs() activate(n__repItems(X)) -> repItems(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zip(X1,X2)) -> zip(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) incr(X) -> n__incr(X) incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS))) oddNs() -> incr(pairNs()) oddNs() -> n__oddNs() pairNs() -> cons(0(),n__incr(n__oddNs())) repItems(X) -> n__repItems(X) repItems(cons(X,XS)) -> cons(X,n__cons(X,n__repItems(activate(XS)))) repItems(nil()) -> nil() tail(cons(X,XS)) -> activate(XS) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) zip(X,nil()) -> nil() zip(X1,X2) -> n__zip(X1,X2) zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),n__zip(activate(XS),activate(YS))) zip(nil(),XS) -> nil() - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2} / {0/0,n__cons/2,n__incr/1 ,n__oddNs/0,n__repItems/1,n__take/2,n__zip/2,nil/0,pair/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,cons,incr,oddNs,pairNs,repItems,tail,take ,zip} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: activate(x){x -> n__cons(x,y)} = activate(n__cons(x,y)) ->^+ cons(activate(x),y) = C[activate(x) = activate(x){}] ** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__incr(X)) -> incr(activate(X)) activate(n__oddNs()) -> oddNs() activate(n__repItems(X)) -> repItems(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zip(X1,X2)) -> zip(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) incr(X) -> n__incr(X) incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS))) oddNs() -> incr(pairNs()) oddNs() -> n__oddNs() pairNs() -> cons(0(),n__incr(n__oddNs())) repItems(X) -> n__repItems(X) repItems(cons(X,XS)) -> cons(X,n__cons(X,n__repItems(activate(XS)))) repItems(nil()) -> nil() tail(cons(X,XS)) -> activate(XS) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) zip(X,nil()) -> nil() zip(X1,X2) -> n__zip(X1,X2) zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),n__zip(activate(XS),activate(YS))) zip(nil(),XS) -> nil() - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2} / {0/0,n__cons/2,n__incr/1 ,n__oddNs/0,n__repItems/1,n__take/2,n__zip/2,nil/0,pair/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,cons,incr,oddNs,pairNs,repItems,tail,take ,zip} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs activate#(X) -> c_1() activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) activate#(n__oddNs()) -> c_4(oddNs#()) activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) cons#(X1,X2) -> c_8() incr#(X) -> c_9() incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) oddNs#() -> c_11(incr#(pairNs()),pairNs#()) oddNs#() -> c_12() pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) repItems#(X) -> c_14() repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) repItems#(nil()) -> c_16() tail#(cons(X,XS)) -> c_17(activate#(XS)) take#(X1,X2) -> c_18() take#(0(),XS) -> c_19() take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) zip#(X,nil()) -> c_21() zip#(X1,X2) -> c_22() zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) zip#(nil(),XS) -> c_24() Weak DPs and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) activate#(n__oddNs()) -> c_4(oddNs#()) activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) cons#(X1,X2) -> c_8() incr#(X) -> c_9() incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) oddNs#() -> c_11(incr#(pairNs()),pairNs#()) oddNs#() -> c_12() pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) repItems#(X) -> c_14() repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) repItems#(nil()) -> c_16() tail#(cons(X,XS)) -> c_17(activate#(XS)) take#(X1,X2) -> c_18() take#(0(),XS) -> c_19() take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) zip#(X,nil()) -> c_21() zip#(X1,X2) -> c_22() zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) zip#(nil(),XS) -> c_24() - Weak TRS: activate(X) -> X activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__incr(X)) -> incr(activate(X)) activate(n__oddNs()) -> oddNs() activate(n__repItems(X)) -> repItems(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zip(X1,X2)) -> zip(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) incr(X) -> n__incr(X) incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS))) oddNs() -> incr(pairNs()) oddNs() -> n__oddNs() pairNs() -> cons(0(),n__incr(n__oddNs())) repItems(X) -> n__repItems(X) repItems(cons(X,XS)) -> cons(X,n__cons(X,n__repItems(activate(XS)))) repItems(nil()) -> nil() tail(cons(X,XS)) -> activate(XS) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) zip(X,nil()) -> nil() zip(X1,X2) -> n__zip(X1,X2) zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),n__zip(activate(XS),activate(YS))) zip(nil(),XS) -> nil() - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/2,c_3/2,c_4/1,c_5/2,c_6/3,c_7/3,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,8,9,10,12,14,15,16,17,18,19,20,21,22,23,24} by application of Pre({1,8,9,10,12,14,15,16,17,18,19,20,21,22,23,24}) = {2,3,4,5,6,7,11,13}. Here rules are labelled as follows: 1: activate#(X) -> c_1() 2: activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) 3: activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) 4: activate#(n__oddNs()) -> c_4(oddNs#()) 5: activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) 6: activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 7: activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 8: cons#(X1,X2) -> c_8() 9: incr#(X) -> c_9() 10: incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) 11: oddNs#() -> c_11(incr#(pairNs()),pairNs#()) 12: oddNs#() -> c_12() 13: pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) 14: repItems#(X) -> c_14() 15: repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) 16: repItems#(nil()) -> c_16() 17: tail#(cons(X,XS)) -> c_17(activate#(XS)) 18: take#(X1,X2) -> c_18() 19: take#(0(),XS) -> c_19() 20: take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) 21: zip#(X,nil()) -> c_21() 22: zip#(X1,X2) -> c_22() 23: zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) 24: zip#(nil(),XS) -> c_24() ** Step 1.b:3: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) activate#(n__oddNs()) -> c_4(oddNs#()) activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) oddNs#() -> c_11(incr#(pairNs()),pairNs#()) pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) - Weak DPs: activate#(X) -> c_1() cons#(X1,X2) -> c_8() incr#(X) -> c_9() incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) oddNs#() -> c_12() repItems#(X) -> c_14() repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) repItems#(nil()) -> c_16() tail#(cons(X,XS)) -> c_17(activate#(XS)) take#(X1,X2) -> c_18() take#(0(),XS) -> c_19() take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) zip#(X,nil()) -> c_21() zip#(X1,X2) -> c_22() zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) zip#(nil(),XS) -> c_24() - Weak TRS: activate(X) -> X activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__incr(X)) -> incr(activate(X)) activate(n__oddNs()) -> oddNs() activate(n__repItems(X)) -> repItems(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zip(X1,X2)) -> zip(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) incr(X) -> n__incr(X) incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS))) oddNs() -> incr(pairNs()) oddNs() -> n__oddNs() pairNs() -> cons(0(),n__incr(n__oddNs())) repItems(X) -> n__repItems(X) repItems(cons(X,XS)) -> cons(X,n__cons(X,n__repItems(activate(XS)))) repItems(nil()) -> nil() tail(cons(X,XS)) -> activate(XS) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) zip(X,nil()) -> nil() zip(X1,X2) -> n__zip(X1,X2) zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),n__zip(activate(XS),activate(YS))) zip(nil(),XS) -> nil() - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/2,c_3/2,c_4/1,c_5/2,c_6/3,c_7/3,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {8} by application of Pre({8}) = {7}. Here rules are labelled as follows: 1: activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) 2: activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) 3: activate#(n__oddNs()) -> c_4(oddNs#()) 4: activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) 5: activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 6: activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 7: oddNs#() -> c_11(incr#(pairNs()),pairNs#()) 8: pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) 9: activate#(X) -> c_1() 10: cons#(X1,X2) -> c_8() 11: incr#(X) -> c_9() 12: incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) 13: oddNs#() -> c_12() 14: repItems#(X) -> c_14() 15: repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) 16: repItems#(nil()) -> c_16() 17: tail#(cons(X,XS)) -> c_17(activate#(XS)) 18: take#(X1,X2) -> c_18() 19: take#(0(),XS) -> c_19() 20: take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) 21: zip#(X,nil()) -> c_21() 22: zip#(X1,X2) -> c_22() 23: zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) 24: zip#(nil(),XS) -> c_24() ** Step 1.b:4: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) activate#(n__oddNs()) -> c_4(oddNs#()) activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) oddNs#() -> c_11(incr#(pairNs()),pairNs#()) - Weak DPs: activate#(X) -> c_1() cons#(X1,X2) -> c_8() incr#(X) -> c_9() incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) oddNs#() -> c_12() pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) repItems#(X) -> c_14() repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) repItems#(nil()) -> c_16() tail#(cons(X,XS)) -> c_17(activate#(XS)) take#(X1,X2) -> c_18() take#(0(),XS) -> c_19() take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) zip#(X,nil()) -> c_21() zip#(X1,X2) -> c_22() zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) zip#(nil(),XS) -> c_24() - Weak TRS: activate(X) -> X activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__incr(X)) -> incr(activate(X)) activate(n__oddNs()) -> oddNs() activate(n__repItems(X)) -> repItems(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zip(X1,X2)) -> zip(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) incr(X) -> n__incr(X) incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS))) oddNs() -> incr(pairNs()) oddNs() -> n__oddNs() pairNs() -> cons(0(),n__incr(n__oddNs())) repItems(X) -> n__repItems(X) repItems(cons(X,XS)) -> cons(X,n__cons(X,n__repItems(activate(XS)))) repItems(nil()) -> nil() tail(cons(X,XS)) -> activate(XS) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) zip(X,nil()) -> nil() zip(X1,X2) -> n__zip(X1,X2) zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),n__zip(activate(XS),activate(YS))) zip(nil(),XS) -> nil() - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/2,c_3/2,c_4/1,c_5/2,c_6/3,c_7/3,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {7} by application of Pre({7}) = {3}. Here rules are labelled as follows: 1: activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) 2: activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) 3: activate#(n__oddNs()) -> c_4(oddNs#()) 4: activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) 5: activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 6: activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 7: oddNs#() -> c_11(incr#(pairNs()),pairNs#()) 8: activate#(X) -> c_1() 9: cons#(X1,X2) -> c_8() 10: incr#(X) -> c_9() 11: incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) 12: oddNs#() -> c_12() 13: pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) 14: repItems#(X) -> c_14() 15: repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) 16: repItems#(nil()) -> c_16() 17: tail#(cons(X,XS)) -> c_17(activate#(XS)) 18: take#(X1,X2) -> c_18() 19: take#(0(),XS) -> c_19() 20: take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) 21: zip#(X,nil()) -> c_21() 22: zip#(X1,X2) -> c_22() 23: zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) 24: zip#(nil(),XS) -> c_24() ** Step 1.b:5: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) activate#(n__oddNs()) -> c_4(oddNs#()) activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) - Weak DPs: activate#(X) -> c_1() cons#(X1,X2) -> c_8() incr#(X) -> c_9() incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) oddNs#() -> c_11(incr#(pairNs()),pairNs#()) oddNs#() -> c_12() pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) repItems#(X) -> c_14() repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) repItems#(nil()) -> c_16() tail#(cons(X,XS)) -> c_17(activate#(XS)) take#(X1,X2) -> c_18() take#(0(),XS) -> c_19() take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) zip#(X,nil()) -> c_21() zip#(X1,X2) -> c_22() zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) zip#(nil(),XS) -> c_24() - Weak TRS: activate(X) -> X activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__incr(X)) -> incr(activate(X)) activate(n__oddNs()) -> oddNs() activate(n__repItems(X)) -> repItems(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zip(X1,X2)) -> zip(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) incr(X) -> n__incr(X) incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS))) oddNs() -> incr(pairNs()) oddNs() -> n__oddNs() pairNs() -> cons(0(),n__incr(n__oddNs())) repItems(X) -> n__repItems(X) repItems(cons(X,XS)) -> cons(X,n__cons(X,n__repItems(activate(XS)))) repItems(nil()) -> nil() tail(cons(X,XS)) -> activate(XS) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) zip(X,nil()) -> nil() zip(X1,X2) -> n__zip(X1,X2) zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),n__zip(activate(XS),activate(YS))) zip(nil(),XS) -> nil() - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/2,c_3/2,c_4/1,c_5/2,c_6/3,c_7/3,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3} by application of Pre({3}) = {1,2,4,5,6}. Here rules are labelled as follows: 1: activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) 2: activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) 3: activate#(n__oddNs()) -> c_4(oddNs#()) 4: activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) 5: activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 6: activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 7: activate#(X) -> c_1() 8: cons#(X1,X2) -> c_8() 9: incr#(X) -> c_9() 10: incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) 11: oddNs#() -> c_11(incr#(pairNs()),pairNs#()) 12: oddNs#() -> c_12() 13: pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) 14: repItems#(X) -> c_14() 15: repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) 16: repItems#(nil()) -> c_16() 17: tail#(cons(X,XS)) -> c_17(activate#(XS)) 18: take#(X1,X2) -> c_18() 19: take#(0(),XS) -> c_19() 20: take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) 21: zip#(X,nil()) -> c_21() 22: zip#(X1,X2) -> c_22() 23: zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) 24: zip#(nil(),XS) -> c_24() ** Step 1.b:6: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) - Weak DPs: activate#(X) -> c_1() activate#(n__oddNs()) -> c_4(oddNs#()) cons#(X1,X2) -> c_8() incr#(X) -> c_9() incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) oddNs#() -> c_11(incr#(pairNs()),pairNs#()) oddNs#() -> c_12() pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) repItems#(X) -> c_14() repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) repItems#(nil()) -> c_16() tail#(cons(X,XS)) -> c_17(activate#(XS)) take#(X1,X2) -> c_18() take#(0(),XS) -> c_19() take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) zip#(X,nil()) -> c_21() zip#(X1,X2) -> c_22() zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) zip#(nil(),XS) -> c_24() - Weak TRS: activate(X) -> X activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__incr(X)) -> incr(activate(X)) activate(n__oddNs()) -> oddNs() activate(n__repItems(X)) -> repItems(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zip(X1,X2)) -> zip(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) incr(X) -> n__incr(X) incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS))) oddNs() -> incr(pairNs()) oddNs() -> n__oddNs() pairNs() -> cons(0(),n__incr(n__oddNs())) repItems(X) -> n__repItems(X) repItems(cons(X,XS)) -> cons(X,n__cons(X,n__repItems(activate(XS)))) repItems(nil()) -> nil() tail(cons(X,XS)) -> activate(XS) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) zip(X,nil()) -> nil() zip(X1,X2) -> n__zip(X1,X2) zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),n__zip(activate(XS),activate(YS))) zip(nil(),XS) -> nil() - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/2,c_3/2,c_4/1,c_5/2,c_6/3,c_7/3,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) -->_2 activate#(n__oddNs()) -> c_4(oddNs#()):7 -->_2 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_2 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_1 cons#(X1,X2) -> c_8():8 -->_2 activate#(X) -> c_1():6 -->_2 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 2:S:activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) -->_2 activate#(n__oddNs()) -> c_4(oddNs#()):7 -->_2 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_1 incr#(X) -> c_9():9 -->_2 activate#(X) -> c_1():6 -->_2 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 3:S:activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) -->_2 activate#(n__oddNs()) -> c_4(oddNs#()):7 -->_2 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_1 repItems#(nil()) -> c_16():16 -->_1 repItems#(X) -> c_14():14 -->_2 activate#(X) -> c_1():6 -->_2 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_2 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 4:S:activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__oddNs()) -> c_4(oddNs#()):7 -->_2 activate#(n__oddNs()) -> c_4(oddNs#()):7 -->_3 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 take#(0(),XS) -> c_19():19 -->_1 take#(X1,X2) -> c_18():18 -->_3 activate#(X) -> c_1():6 -->_2 activate#(X) -> c_1():6 -->_3 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_2 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_3 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_2 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_3 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 5:S:activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__oddNs()) -> c_4(oddNs#()):7 -->_2 activate#(n__oddNs()) -> c_4(oddNs#()):7 -->_1 zip#(nil(),XS) -> c_24():24 -->_1 zip#(X1,X2) -> c_22():22 -->_1 zip#(X,nil()) -> c_21():21 -->_3 activate#(X) -> c_1():6 -->_2 activate#(X) -> c_1():6 -->_3 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_2 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_3 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_2 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_3 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 6:W:activate#(X) -> c_1() 7:W:activate#(n__oddNs()) -> c_4(oddNs#()) -->_1 oddNs#() -> c_11(incr#(pairNs()),pairNs#()):11 -->_1 oddNs#() -> c_12():12 8:W:cons#(X1,X2) -> c_8() 9:W:incr#(X) -> c_9() 10:W:incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) 11:W:oddNs#() -> c_11(incr#(pairNs()),pairNs#()) -->_2 pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))):13 -->_1 incr#(X) -> c_9():9 12:W:oddNs#() -> c_12() 13:W:pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) -->_1 cons#(X1,X2) -> c_8():8 14:W:repItems#(X) -> c_14() 15:W:repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) 16:W:repItems#(nil()) -> c_16() 17:W:tail#(cons(X,XS)) -> c_17(activate#(XS)) 18:W:take#(X1,X2) -> c_18() 19:W:take#(0(),XS) -> c_19() 20:W:take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) 21:W:zip#(X,nil()) -> c_21() 22:W:zip#(X1,X2) -> c_22() 23:W:zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) 24:W:zip#(nil(),XS) -> c_24() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 23: zip#(cons(X,XS),cons(Y,YS)) -> c_23(cons#(pair(X,Y),n__zip(activate(XS),activate(YS))) ,activate#(XS) ,activate#(YS)) 20: take#(s(N),cons(X,XS)) -> c_20(cons#(X,n__take(N,activate(XS))),activate#(XS)) 17: tail#(cons(X,XS)) -> c_17(activate#(XS)) 15: repItems#(cons(X,XS)) -> c_15(cons#(X,n__cons(X,n__repItems(activate(XS)))),activate#(XS)) 10: incr#(cons(X,XS)) -> c_10(cons#(s(X),n__incr(activate(XS))),activate#(XS)) 14: repItems#(X) -> c_14() 16: repItems#(nil()) -> c_16() 18: take#(X1,X2) -> c_18() 19: take#(0(),XS) -> c_19() 6: activate#(X) -> c_1() 21: zip#(X,nil()) -> c_21() 22: zip#(X1,X2) -> c_22() 24: zip#(nil(),XS) -> c_24() 7: activate#(n__oddNs()) -> c_4(oddNs#()) 12: oddNs#() -> c_12() 11: oddNs#() -> c_11(incr#(pairNs()),pairNs#()) 9: incr#(X) -> c_9() 13: pairNs#() -> c_13(cons#(0(),n__incr(n__oddNs()))) 8: cons#(X1,X2) -> c_8() ** Step 1.b:7: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) - Weak TRS: activate(X) -> X activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__incr(X)) -> incr(activate(X)) activate(n__oddNs()) -> oddNs() activate(n__repItems(X)) -> repItems(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zip(X1,X2)) -> zip(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) incr(X) -> n__incr(X) incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS))) oddNs() -> incr(pairNs()) oddNs() -> n__oddNs() pairNs() -> cons(0(),n__incr(n__oddNs())) repItems(X) -> n__repItems(X) repItems(cons(X,XS)) -> cons(X,n__cons(X,n__repItems(activate(XS)))) repItems(nil()) -> nil() tail(cons(X,XS)) -> activate(XS) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) zip(X,nil()) -> nil() zip(X1,X2) -> n__zip(X1,X2) zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),n__zip(activate(XS),activate(YS))) zip(nil(),XS) -> nil() - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/2,c_3/2,c_4/1,c_5/2,c_6/3,c_7/3,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)) -->_2 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_2 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 2:S:activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)) -->_2 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_2 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 3:S:activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)) -->_2 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_2 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 4:S:activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_2 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_3 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_2 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_3 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 5:S:activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__zip(X1,X2)) -> c_7(zip#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_6(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_2 activate#(n__repItems(X)) -> c_5(repItems#(activate(X)),activate#(X)):3 -->_3 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_2 activate#(n__incr(X)) -> c_3(incr#(activate(X)),activate#(X)):2 -->_3 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_2(cons#(activate(X1),X2),activate#(X1)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: activate#(n__cons(X1,X2)) -> c_2(activate#(X1)) activate#(n__incr(X)) -> c_3(activate#(X)) activate#(n__repItems(X)) -> c_5(activate#(X)) activate#(n__take(X1,X2)) -> c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(activate#(X1),activate#(X2)) ** Step 1.b:8: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_2(activate#(X1)) activate#(n__incr(X)) -> c_3(activate#(X)) activate#(n__repItems(X)) -> c_5(activate#(X)) activate#(n__take(X1,X2)) -> c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(activate#(X1),activate#(X2)) - Weak TRS: activate(X) -> X activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__incr(X)) -> incr(activate(X)) activate(n__oddNs()) -> oddNs() activate(n__repItems(X)) -> repItems(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zip(X1,X2)) -> zip(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) incr(X) -> n__incr(X) incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS))) oddNs() -> incr(pairNs()) oddNs() -> n__oddNs() pairNs() -> cons(0(),n__incr(n__oddNs())) repItems(X) -> n__repItems(X) repItems(cons(X,XS)) -> cons(X,n__cons(X,n__repItems(activate(XS)))) repItems(nil()) -> nil() tail(cons(X,XS)) -> activate(XS) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) zip(X,nil()) -> nil() zip(X1,X2) -> n__zip(X1,X2) zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),n__zip(activate(XS),activate(YS))) zip(nil(),XS) -> nil() - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/2,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: activate#(n__cons(X1,X2)) -> c_2(activate#(X1)) activate#(n__incr(X)) -> c_3(activate#(X)) activate#(n__repItems(X)) -> c_5(activate#(X)) activate#(n__take(X1,X2)) -> c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(activate#(X1),activate#(X2)) ** Step 1.b:9: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_2(activate#(X1)) activate#(n__incr(X)) -> c_3(activate#(X)) activate#(n__repItems(X)) -> c_5(activate#(X)) activate#(n__take(X1,X2)) -> c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(activate#(X1),activate#(X2)) - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/2,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_3) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [0] p(cons) = [0] p(incr) = [0] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__incr) = [1] x1 + [0] p(n__oddNs) = [0] p(n__repItems) = [1] x1 + [0] p(n__take) = [1] x1 + [1] x2 + [8] p(n__zip) = [1] x1 + [1] x2 + [2] p(nil) = [0] p(oddNs) = [0] p(pair) = [1] x1 + [1] x2 + [0] p(pairNs) = [0] p(repItems) = [0] p(s) = [1] x1 + [0] p(tail) = [0] p(take) = [0] p(zip) = [0] p(activate#) = [1] x1 + [1] p(cons#) = [0] p(incr#) = [0] p(oddNs#) = [0] p(pairNs#) = [0] p(repItems#) = [0] p(tail#) = [2] x1 + [0] p(take#) = [1] p(zip#) = [1] x1 + [1] x2 + [1] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [15] p(c_4) = [2] x1 + [1] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [1] x2 + [2] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] Following rules are strictly oriented: activate#(n__take(X1,X2)) = [1] X1 + [1] X2 + [9] > [1] X1 + [1] X2 + [4] = c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) = [1] X1 + [1] X2 + [3] > [1] X1 + [1] X2 + [2] = c_7(activate#(X1),activate#(X2)) Following rules are (at-least) weakly oriented: activate#(n__cons(X1,X2)) = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] = c_2(activate#(X1)) activate#(n__incr(X)) = [1] X + [1] >= [1] X + [16] = c_3(activate#(X)) activate#(n__repItems(X)) = [1] X + [1] >= [1] X + [1] = c_5(activate#(X)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:10: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_2(activate#(X1)) activate#(n__incr(X)) -> c_3(activate#(X)) activate#(n__repItems(X)) -> c_5(activate#(X)) - Weak DPs: activate#(n__take(X1,X2)) -> c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(activate#(X1),activate#(X2)) - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/2,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_3) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [0] p(cons) = [0] p(incr) = [0] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__incr) = [1] x1 + [0] p(n__oddNs) = [0] p(n__repItems) = [1] x1 + [13] p(n__take) = [1] x1 + [1] x2 + [0] p(n__zip) = [1] x1 + [1] x2 + [0] p(nil) = [0] p(oddNs) = [0] p(pair) = [1] x1 + [1] x2 + [0] p(pairNs) = [0] p(repItems) = [0] p(s) = [1] x1 + [0] p(tail) = [1] x1 + [0] p(take) = [0] p(zip) = [0] p(activate#) = [1] x1 + [0] p(cons#) = [0] p(incr#) = [0] p(oddNs#) = [0] p(pairNs#) = [0] p(repItems#) = [0] p(tail#) = [0] p(take#) = [0] p(zip#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [1] x2 + [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] Following rules are strictly oriented: activate#(n__repItems(X)) = [1] X + [13] > [1] X + [0] = c_5(activate#(X)) Following rules are (at-least) weakly oriented: activate#(n__cons(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [0] = c_2(activate#(X1)) activate#(n__incr(X)) = [1] X + [0] >= [1] X + [0] = c_3(activate#(X)) activate#(n__take(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = c_7(activate#(X1),activate#(X2)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:11: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_2(activate#(X1)) activate#(n__incr(X)) -> c_3(activate#(X)) - Weak DPs: activate#(n__repItems(X)) -> c_5(activate#(X)) activate#(n__take(X1,X2)) -> c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(activate#(X1),activate#(X2)) - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/2,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_3) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [0] p(cons) = [0] p(incr) = [0] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__incr) = [1] x1 + [1] p(n__oddNs) = [0] p(n__repItems) = [1] x1 + [0] p(n__take) = [1] x1 + [1] x2 + [0] p(n__zip) = [1] x1 + [1] x2 + [0] p(nil) = [0] p(oddNs) = [0] p(pair) = [1] x1 + [1] x2 + [0] p(pairNs) = [0] p(repItems) = [0] p(s) = [1] x1 + [0] p(tail) = [0] p(take) = [0] p(zip) = [0] p(activate#) = [4] x1 + [0] p(cons#) = [0] p(incr#) = [0] p(oddNs#) = [0] p(pairNs#) = [0] p(repItems#) = [0] p(tail#) = [0] p(take#) = [0] p(zip#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [4] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [1] x2 + [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [8] x1 + [8] p(c_14) = [1] p(c_15) = [4] x1 + [0] p(c_16) = [2] p(c_17) = [2] x1 + [1] p(c_18) = [1] p(c_19) = [1] p(c_20) = [4] x1 + [4] x2 + [1] p(c_21) = [0] p(c_22) = [1] p(c_23) = [4] x1 + [1] x2 + [2] x3 + [1] p(c_24) = [1] Following rules are strictly oriented: activate#(n__incr(X)) = [4] X + [4] > [4] X + [0] = c_3(activate#(X)) Following rules are (at-least) weakly oriented: activate#(n__cons(X1,X2)) = [4] X1 + [4] X2 + [0] >= [4] X1 + [4] = c_2(activate#(X1)) activate#(n__repItems(X)) = [4] X + [0] >= [4] X + [0] = c_5(activate#(X)) activate#(n__take(X1,X2)) = [4] X1 + [4] X2 + [0] >= [4] X1 + [4] X2 + [0] = c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) = [4] X1 + [4] X2 + [0] >= [4] X1 + [4] X2 + [0] = c_7(activate#(X1),activate#(X2)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:12: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_2(activate#(X1)) - Weak DPs: activate#(n__incr(X)) -> c_3(activate#(X)) activate#(n__repItems(X)) -> c_5(activate#(X)) activate#(n__take(X1,X2)) -> c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(activate#(X1),activate#(X2)) - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/2,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_3) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [0] p(cons) = [0] p(incr) = [0] p(n__cons) = [1] x1 + [1] x2 + [2] p(n__incr) = [1] x1 + [0] p(n__oddNs) = [0] p(n__repItems) = [1] x1 + [0] p(n__take) = [1] x1 + [1] x2 + [2] p(n__zip) = [1] x1 + [1] x2 + [0] p(nil) = [0] p(oddNs) = [0] p(pair) = [1] x1 + [1] x2 + [0] p(pairNs) = [0] p(repItems) = [0] p(s) = [1] x1 + [0] p(tail) = [0] p(take) = [0] p(zip) = [0] p(activate#) = [8] x1 + [0] p(cons#) = [0] p(incr#) = [0] p(oddNs#) = [0] p(pairNs#) = [0] p(repItems#) = [0] p(tail#) = [0] p(take#) = [0] p(zip#) = [2] x2 + [0] p(c_1) = [1] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [0] p(c_4) = [1] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [1] x2 + [0] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [2] x1 + [1] p(c_16) = [8] p(c_17) = [1] x1 + [1] p(c_18) = [1] p(c_19) = [0] p(c_20) = [1] x1 + [1] x2 + [4] p(c_21) = [0] p(c_22) = [1] p(c_23) = [1] x1 + [1] x2 + [2] x3 + [1] p(c_24) = [2] Following rules are strictly oriented: activate#(n__cons(X1,X2)) = [8] X1 + [8] X2 + [16] > [8] X1 + [0] = c_2(activate#(X1)) Following rules are (at-least) weakly oriented: activate#(n__incr(X)) = [8] X + [0] >= [8] X + [0] = c_3(activate#(X)) activate#(n__repItems(X)) = [8] X + [0] >= [8] X + [0] = c_5(activate#(X)) activate#(n__take(X1,X2)) = [8] X1 + [8] X2 + [16] >= [8] X1 + [8] X2 + [0] = c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) = [8] X1 + [8] X2 + [0] >= [8] X1 + [8] X2 + [0] = c_7(activate#(X1),activate#(X2)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:13: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: activate#(n__cons(X1,X2)) -> c_2(activate#(X1)) activate#(n__incr(X)) -> c_3(activate#(X)) activate#(n__repItems(X)) -> c_5(activate#(X)) activate#(n__take(X1,X2)) -> c_6(activate#(X1),activate#(X2)) activate#(n__zip(X1,X2)) -> c_7(activate#(X1),activate#(X2)) - Signature: {activate/1,cons/2,incr/1,oddNs/0,pairNs/0,repItems/1,tail/1,take/2,zip/2,activate#/1,cons#/2,incr#/1 ,oddNs#/0,pairNs#/0,repItems#/1,tail#/1,take#/2,zip#/2} / {0/0,n__cons/2,n__incr/1,n__oddNs/0,n__repItems/1 ,n__take/2,n__zip/2,nil/0,pair/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/2,c_7/2,c_8/0,c_9/0,c_10/2,c_11/2 ,c_12/0,c_13/1,c_14/0,c_15/2,c_16/0,c_17/1,c_18/0,c_19/0,c_20/2,c_21/0,c_22/0,c_23/3,c_24/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,cons#,incr#,oddNs#,pairNs#,repItems#,tail# ,take#,zip#} and constructors {0,n__cons,n__incr,n__oddNs,n__repItems,n__take,n__zip,nil,pair,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))