MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__oddNs() -> a__incr(a__pairNs()) a__oddNs() -> oddNs() a__pairNs() -> cons(0(),incr(oddNs())) a__pairNs() -> pairNs() a__repItems(X) -> repItems(X) a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS))) a__repItems(nil()) -> nil() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) a__take(X1,X2) -> take(X1,X2) a__take(0(),XS) -> nil() a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS)) a__zip(X,nil()) -> nil() a__zip(X1,X2) -> zip(X1,X2) a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS)) a__zip(nil(),XS) -> nil() mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(incr(X)) -> a__incr(mark(X)) mark(nil()) -> nil() mark(oddNs()) -> a__oddNs() mark(pair(X1,X2)) -> pair(mark(X1),mark(X2)) mark(pairNs()) -> a__pairNs() mark(repItems(X)) -> a__repItems(mark(X)) mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2)) - Signature: {a__incr/1,a__oddNs/0,a__pairNs/0,a__repItems/1,a__tail/1,a__take/2,a__zip/2,mark/1} / {0/0,cons/2,incr/1 ,nil/0,oddNs/0,pair/2,pairNs/0,repItems/1,s/1,tail/1,take/2,zip/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__incr,a__oddNs,a__pairNs,a__repItems,a__tail,a__take ,a__zip,mark} and constructors {0,cons,incr,nil,oddNs,pair,pairNs,repItems,s,tail,take,zip} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a__incr#(X) -> c_1() a__incr#(cons(X,XS)) -> c_2(mark#(X)) a__oddNs#() -> c_3(a__incr#(a__pairNs()),a__pairNs#()) a__oddNs#() -> c_4() a__pairNs#() -> c_5() a__pairNs#() -> c_6() a__repItems#(X) -> c_7() a__repItems#(cons(X,XS)) -> c_8(mark#(X)) a__repItems#(nil()) -> c_9() a__tail#(X) -> c_10() a__tail#(cons(X,XS)) -> c_11(mark#(XS)) a__take#(X1,X2) -> c_12() a__take#(0(),XS) -> c_13() a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)) a__zip#(X,nil()) -> c_15() a__zip#(X1,X2) -> c_16() a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)) a__zip#(nil(),XS) -> c_18() mark#(0()) -> c_19() mark#(cons(X1,X2)) -> c_20(mark#(X1)) mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)) mark#(nil()) -> c_22() mark#(oddNs()) -> c_23(a__oddNs#()) mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)) mark#(pairNs()) -> c_25(a__pairNs#()) mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)) mark#(s(X)) -> c_27(mark#(X)) mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)) mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__incr#(X) -> c_1() a__incr#(cons(X,XS)) -> c_2(mark#(X)) a__oddNs#() -> c_3(a__incr#(a__pairNs()),a__pairNs#()) a__oddNs#() -> c_4() a__pairNs#() -> c_5() a__pairNs#() -> c_6() a__repItems#(X) -> c_7() a__repItems#(cons(X,XS)) -> c_8(mark#(X)) a__repItems#(nil()) -> c_9() a__tail#(X) -> c_10() a__tail#(cons(X,XS)) -> c_11(mark#(XS)) a__take#(X1,X2) -> c_12() a__take#(0(),XS) -> c_13() a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)) a__zip#(X,nil()) -> c_15() a__zip#(X1,X2) -> c_16() a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)) a__zip#(nil(),XS) -> c_18() mark#(0()) -> c_19() mark#(cons(X1,X2)) -> c_20(mark#(X1)) mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)) mark#(nil()) -> c_22() mark#(oddNs()) -> c_23(a__oddNs#()) mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)) mark#(pairNs()) -> c_25(a__pairNs#()) mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)) mark#(s(X)) -> c_27(mark#(X)) mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)) mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak TRS: a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__oddNs() -> a__incr(a__pairNs()) a__oddNs() -> oddNs() a__pairNs() -> cons(0(),incr(oddNs())) a__pairNs() -> pairNs() a__repItems(X) -> repItems(X) a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS))) a__repItems(nil()) -> nil() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) a__take(X1,X2) -> take(X1,X2) a__take(0(),XS) -> nil() a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS)) a__zip(X,nil()) -> nil() a__zip(X1,X2) -> zip(X1,X2) a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS)) a__zip(nil(),XS) -> nil() mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(incr(X)) -> a__incr(mark(X)) mark(nil()) -> nil() mark(oddNs()) -> a__oddNs() mark(pair(X1,X2)) -> pair(mark(X1),mark(X2)) mark(pairNs()) -> a__pairNs() mark(repItems(X)) -> a__repItems(mark(X)) mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2)) - Signature: {a__incr/1,a__oddNs/0,a__pairNs/0,a__repItems/1,a__tail/1,a__take/2,a__zip/2,mark/1,a__incr#/1,a__oddNs#/0 ,a__pairNs#/0,a__repItems#/1,a__tail#/1,a__take#/2,a__zip#/2,mark#/1} / {0/0,cons/2,incr/1,nil/0,oddNs/0 ,pair/2,pairNs/0,repItems/1,s/1,tail/1,take/2,zip/2,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/2,c_18/0,c_19/0,c_20/1,c_21/2,c_22/0,c_23/1,c_24/2 ,c_25/1,c_26/2,c_27/1,c_28/2,c_29/3,c_30/3} - Obligation: innermost runtime complexity wrt. defined symbols {a__incr#,a__oddNs#,a__pairNs#,a__repItems#,a__tail# ,a__take#,a__zip#,mark#} and constructors {0,cons,incr,nil,oddNs,pair,pairNs,repItems,s,tail,take,zip} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,4,5,6,7,9,10,12,13,15,16,18,19,22} by application of Pre({1,4,5,6,7,9,10,12,13,15,16,18,19,22}) = {2,3,8,11,14,17,20,21,23,24,25,26,27,28,29,30}. Here rules are labelled as follows: 1: a__incr#(X) -> c_1() 2: a__incr#(cons(X,XS)) -> c_2(mark#(X)) 3: a__oddNs#() -> c_3(a__incr#(a__pairNs()),a__pairNs#()) 4: a__oddNs#() -> c_4() 5: a__pairNs#() -> c_5() 6: a__pairNs#() -> c_6() 7: a__repItems#(X) -> c_7() 8: a__repItems#(cons(X,XS)) -> c_8(mark#(X)) 9: a__repItems#(nil()) -> c_9() 10: a__tail#(X) -> c_10() 11: a__tail#(cons(X,XS)) -> c_11(mark#(XS)) 12: a__take#(X1,X2) -> c_12() 13: a__take#(0(),XS) -> c_13() 14: a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)) 15: a__zip#(X,nil()) -> c_15() 16: a__zip#(X1,X2) -> c_16() 17: a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)) 18: a__zip#(nil(),XS) -> c_18() 19: mark#(0()) -> c_19() 20: mark#(cons(X1,X2)) -> c_20(mark#(X1)) 21: mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)) 22: mark#(nil()) -> c_22() 23: mark#(oddNs()) -> c_23(a__oddNs#()) 24: mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)) 25: mark#(pairNs()) -> c_25(a__pairNs#()) 26: mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)) 27: mark#(s(X)) -> c_27(mark#(X)) 28: mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)) 29: mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 30: mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__incr#(cons(X,XS)) -> c_2(mark#(X)) a__oddNs#() -> c_3(a__incr#(a__pairNs()),a__pairNs#()) a__repItems#(cons(X,XS)) -> c_8(mark#(X)) a__tail#(cons(X,XS)) -> c_11(mark#(XS)) a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)) a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)) mark#(cons(X1,X2)) -> c_20(mark#(X1)) mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)) mark#(oddNs()) -> c_23(a__oddNs#()) mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)) mark#(pairNs()) -> c_25(a__pairNs#()) mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)) mark#(s(X)) -> c_27(mark#(X)) mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)) mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak DPs: a__incr#(X) -> c_1() a__oddNs#() -> c_4() a__pairNs#() -> c_5() a__pairNs#() -> c_6() a__repItems#(X) -> c_7() a__repItems#(nil()) -> c_9() a__tail#(X) -> c_10() a__take#(X1,X2) -> c_12() a__take#(0(),XS) -> c_13() a__zip#(X,nil()) -> c_15() a__zip#(X1,X2) -> c_16() a__zip#(nil(),XS) -> c_18() mark#(0()) -> c_19() mark#(nil()) -> c_22() - Weak TRS: a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__oddNs() -> a__incr(a__pairNs()) a__oddNs() -> oddNs() a__pairNs() -> cons(0(),incr(oddNs())) a__pairNs() -> pairNs() a__repItems(X) -> repItems(X) a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS))) a__repItems(nil()) -> nil() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) a__take(X1,X2) -> take(X1,X2) a__take(0(),XS) -> nil() a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS)) a__zip(X,nil()) -> nil() a__zip(X1,X2) -> zip(X1,X2) a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS)) a__zip(nil(),XS) -> nil() mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(incr(X)) -> a__incr(mark(X)) mark(nil()) -> nil() mark(oddNs()) -> a__oddNs() mark(pair(X1,X2)) -> pair(mark(X1),mark(X2)) mark(pairNs()) -> a__pairNs() mark(repItems(X)) -> a__repItems(mark(X)) mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2)) - Signature: {a__incr/1,a__oddNs/0,a__pairNs/0,a__repItems/1,a__tail/1,a__take/2,a__zip/2,mark/1,a__incr#/1,a__oddNs#/0 ,a__pairNs#/0,a__repItems#/1,a__tail#/1,a__take#/2,a__zip#/2,mark#/1} / {0/0,cons/2,incr/1,nil/0,oddNs/0 ,pair/2,pairNs/0,repItems/1,s/1,tail/1,take/2,zip/2,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/2,c_18/0,c_19/0,c_20/1,c_21/2,c_22/0,c_23/1,c_24/2 ,c_25/1,c_26/2,c_27/1,c_28/2,c_29/3,c_30/3} - Obligation: innermost runtime complexity wrt. defined symbols {a__incr#,a__oddNs#,a__pairNs#,a__repItems#,a__tail# ,a__take#,a__zip#,mark#} and constructors {0,cons,incr,nil,oddNs,pair,pairNs,repItems,s,tail,take,zip} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {11} by application of Pre({11}) = {1,3,4,5,6,7,8,10,12,13,14,15,16}. Here rules are labelled as follows: 1: a__incr#(cons(X,XS)) -> c_2(mark#(X)) 2: a__oddNs#() -> c_3(a__incr#(a__pairNs()),a__pairNs#()) 3: a__repItems#(cons(X,XS)) -> c_8(mark#(X)) 4: a__tail#(cons(X,XS)) -> c_11(mark#(XS)) 5: a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)) 6: a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)) 7: mark#(cons(X1,X2)) -> c_20(mark#(X1)) 8: mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)) 9: mark#(oddNs()) -> c_23(a__oddNs#()) 10: mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)) 11: mark#(pairNs()) -> c_25(a__pairNs#()) 12: mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)) 13: mark#(s(X)) -> c_27(mark#(X)) 14: mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)) 15: mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 16: mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 17: a__incr#(X) -> c_1() 18: a__oddNs#() -> c_4() 19: a__pairNs#() -> c_5() 20: a__pairNs#() -> c_6() 21: a__repItems#(X) -> c_7() 22: a__repItems#(nil()) -> c_9() 23: a__tail#(X) -> c_10() 24: a__take#(X1,X2) -> c_12() 25: a__take#(0(),XS) -> c_13() 26: a__zip#(X,nil()) -> c_15() 27: a__zip#(X1,X2) -> c_16() 28: a__zip#(nil(),XS) -> c_18() 29: mark#(0()) -> c_19() 30: mark#(nil()) -> c_22() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: a__incr#(cons(X,XS)) -> c_2(mark#(X)) a__oddNs#() -> c_3(a__incr#(a__pairNs()),a__pairNs#()) a__repItems#(cons(X,XS)) -> c_8(mark#(X)) a__tail#(cons(X,XS)) -> c_11(mark#(XS)) a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)) a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)) mark#(cons(X1,X2)) -> c_20(mark#(X1)) mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)) mark#(oddNs()) -> c_23(a__oddNs#()) mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)) mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)) mark#(s(X)) -> c_27(mark#(X)) mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)) mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak DPs: a__incr#(X) -> c_1() a__oddNs#() -> c_4() a__pairNs#() -> c_5() a__pairNs#() -> c_6() a__repItems#(X) -> c_7() a__repItems#(nil()) -> c_9() a__tail#(X) -> c_10() a__take#(X1,X2) -> c_12() a__take#(0(),XS) -> c_13() a__zip#(X,nil()) -> c_15() a__zip#(X1,X2) -> c_16() a__zip#(nil(),XS) -> c_18() mark#(0()) -> c_19() mark#(nil()) -> c_22() mark#(pairNs()) -> c_25(a__pairNs#()) - Weak TRS: a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__oddNs() -> a__incr(a__pairNs()) a__oddNs() -> oddNs() a__pairNs() -> cons(0(),incr(oddNs())) a__pairNs() -> pairNs() a__repItems(X) -> repItems(X) a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS))) a__repItems(nil()) -> nil() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) a__take(X1,X2) -> take(X1,X2) a__take(0(),XS) -> nil() a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS)) a__zip(X,nil()) -> nil() a__zip(X1,X2) -> zip(X1,X2) a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS)) a__zip(nil(),XS) -> nil() mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(incr(X)) -> a__incr(mark(X)) mark(nil()) -> nil() mark(oddNs()) -> a__oddNs() mark(pair(X1,X2)) -> pair(mark(X1),mark(X2)) mark(pairNs()) -> a__pairNs() mark(repItems(X)) -> a__repItems(mark(X)) mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2)) - Signature: {a__incr/1,a__oddNs/0,a__pairNs/0,a__repItems/1,a__tail/1,a__take/2,a__zip/2,mark/1,a__incr#/1,a__oddNs#/0 ,a__pairNs#/0,a__repItems#/1,a__tail#/1,a__take#/2,a__zip#/2,mark#/1} / {0/0,cons/2,incr/1,nil/0,oddNs/0 ,pair/2,pairNs/0,repItems/1,s/1,tail/1,take/2,zip/2,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/2,c_18/0,c_19/0,c_20/1,c_21/2,c_22/0,c_23/1,c_24/2 ,c_25/1,c_26/2,c_27/1,c_28/2,c_29/3,c_30/3} - Obligation: innermost runtime complexity wrt. defined symbols {a__incr#,a__oddNs#,a__pairNs#,a__repItems#,a__tail# ,a__take#,a__zip#,mark#} and constructors {0,cons,incr,nil,oddNs,pair,pairNs,repItems,s,tail,take,zip} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:a__incr#(cons(X,XS)) -> c_2(mark#(X)) -->_1 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 mark#(nil()) -> c_22():29 -->_1 mark#(0()) -> c_19():28 2:S:a__oddNs#() -> c_3(a__incr#(a__pairNs()),a__pairNs#()) -->_2 a__pairNs#() -> c_6():19 -->_2 a__pairNs#() -> c_5():18 -->_1 a__incr#(X) -> c_1():16 -->_1 a__incr#(cons(X,XS)) -> c_2(mark#(X)):1 3:S:a__repItems#(cons(X,XS)) -> c_8(mark#(X)) -->_1 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 mark#(nil()) -> c_22():29 -->_1 mark#(0()) -> c_19():28 4:S:a__tail#(cons(X,XS)) -> c_11(mark#(XS)) -->_1 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 mark#(nil()) -> c_22():29 -->_1 mark#(0()) -> c_19():28 5:S:a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)) -->_1 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 mark#(nil()) -> c_22():29 -->_1 mark#(0()) -> c_19():28 6:S:a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)) -->_2 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_1 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_2 mark#(nil()) -> c_22():29 -->_1 mark#(nil()) -> c_22():29 -->_2 mark#(0()) -> c_19():28 -->_1 mark#(0()) -> c_19():28 7:S:mark#(cons(X1,X2)) -> c_20(mark#(X1)) -->_1 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(nil()) -> c_22():29 -->_1 mark#(0()) -> c_19():28 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 8:S:mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)) -->_2 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(nil()) -> c_22():29 -->_2 mark#(0()) -> c_19():28 -->_1 a__incr#(X) -> c_1():16 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 a__incr#(cons(X,XS)) -> c_2(mark#(X)):1 9:S:mark#(oddNs()) -> c_23(a__oddNs#()) -->_1 a__oddNs#() -> c_4():17 -->_1 a__oddNs#() -> c_3(a__incr#(a__pairNs()),a__pairNs#()):2 10:S:mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)) -->_2 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_1 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(nil()) -> c_22():29 -->_1 mark#(nil()) -> c_22():29 -->_2 mark#(0()) -> c_19():28 -->_1 mark#(0()) -> c_19():28 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 11:S:mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)) -->_2 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(nil()) -> c_22():29 -->_2 mark#(0()) -> c_19():28 -->_1 a__repItems#(nil()) -> c_9():21 -->_1 a__repItems#(X) -> c_7():20 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 a__repItems#(cons(X,XS)) -> c_8(mark#(X)):3 12:S:mark#(s(X)) -> c_27(mark#(X)) -->_1 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(nil()) -> c_22():29 -->_1 mark#(0()) -> c_19():28 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 13:S:mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)) -->_2 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(nil()) -> c_22():29 -->_2 mark#(0()) -> c_19():28 -->_1 a__tail#(X) -> c_10():22 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 a__tail#(cons(X,XS)) -> c_11(mark#(XS)):4 14:S:mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_2 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_3 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(nil()) -> c_22():29 -->_2 mark#(nil()) -> c_22():29 -->_3 mark#(0()) -> c_19():28 -->_2 mark#(0()) -> c_19():28 -->_1 a__take#(0(),XS) -> c_13():24 -->_1 a__take#(X1,X2) -> c_12():23 -->_3 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_3 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_3 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_3 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_3 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_3 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_3 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_3 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)):5 15:S:mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_2 mark#(pairNs()) -> c_25(a__pairNs#()):30 -->_3 mark#(nil()) -> c_22():29 -->_2 mark#(nil()) -> c_22():29 -->_3 mark#(0()) -> c_19():28 -->_2 mark#(0()) -> c_19():28 -->_1 a__zip#(nil(),XS) -> c_18():27 -->_1 a__zip#(X1,X2) -> c_16():26 -->_1 a__zip#(X,nil()) -> c_15():25 -->_3 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_3 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_3 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_3 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_3 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_3 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_3 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_3 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)):6 16:W:a__incr#(X) -> c_1() 17:W:a__oddNs#() -> c_4() 18:W:a__pairNs#() -> c_5() 19:W:a__pairNs#() -> c_6() 20:W:a__repItems#(X) -> c_7() 21:W:a__repItems#(nil()) -> c_9() 22:W:a__tail#(X) -> c_10() 23:W:a__take#(X1,X2) -> c_12() 24:W:a__take#(0(),XS) -> c_13() 25:W:a__zip#(X,nil()) -> c_15() 26:W:a__zip#(X1,X2) -> c_16() 27:W:a__zip#(nil(),XS) -> c_18() 28:W:mark#(0()) -> c_19() 29:W:mark#(nil()) -> c_22() 30:W:mark#(pairNs()) -> c_25(a__pairNs#()) -->_1 a__pairNs#() -> c_6():19 -->_1 a__pairNs#() -> c_5():18 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 16: a__incr#(X) -> c_1() 17: a__oddNs#() -> c_4() 20: a__repItems#(X) -> c_7() 21: a__repItems#(nil()) -> c_9() 22: a__tail#(X) -> c_10() 23: a__take#(X1,X2) -> c_12() 24: a__take#(0(),XS) -> c_13() 25: a__zip#(X,nil()) -> c_15() 26: a__zip#(X1,X2) -> c_16() 27: a__zip#(nil(),XS) -> c_18() 28: mark#(0()) -> c_19() 29: mark#(nil()) -> c_22() 30: mark#(pairNs()) -> c_25(a__pairNs#()) 18: a__pairNs#() -> c_5() 19: a__pairNs#() -> c_6() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: a__incr#(cons(X,XS)) -> c_2(mark#(X)) a__oddNs#() -> c_3(a__incr#(a__pairNs()),a__pairNs#()) a__repItems#(cons(X,XS)) -> c_8(mark#(X)) a__tail#(cons(X,XS)) -> c_11(mark#(XS)) a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)) a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)) mark#(cons(X1,X2)) -> c_20(mark#(X1)) mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)) mark#(oddNs()) -> c_23(a__oddNs#()) mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)) mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)) mark#(s(X)) -> c_27(mark#(X)) mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)) mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak TRS: a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__oddNs() -> a__incr(a__pairNs()) a__oddNs() -> oddNs() a__pairNs() -> cons(0(),incr(oddNs())) a__pairNs() -> pairNs() a__repItems(X) -> repItems(X) a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS))) a__repItems(nil()) -> nil() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) a__take(X1,X2) -> take(X1,X2) a__take(0(),XS) -> nil() a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS)) a__zip(X,nil()) -> nil() a__zip(X1,X2) -> zip(X1,X2) a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS)) a__zip(nil(),XS) -> nil() mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(incr(X)) -> a__incr(mark(X)) mark(nil()) -> nil() mark(oddNs()) -> a__oddNs() mark(pair(X1,X2)) -> pair(mark(X1),mark(X2)) mark(pairNs()) -> a__pairNs() mark(repItems(X)) -> a__repItems(mark(X)) mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2)) - Signature: {a__incr/1,a__oddNs/0,a__pairNs/0,a__repItems/1,a__tail/1,a__take/2,a__zip/2,mark/1,a__incr#/1,a__oddNs#/0 ,a__pairNs#/0,a__repItems#/1,a__tail#/1,a__take#/2,a__zip#/2,mark#/1} / {0/0,cons/2,incr/1,nil/0,oddNs/0 ,pair/2,pairNs/0,repItems/1,s/1,tail/1,take/2,zip/2,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/2,c_18/0,c_19/0,c_20/1,c_21/2,c_22/0,c_23/1,c_24/2 ,c_25/1,c_26/2,c_27/1,c_28/2,c_29/3,c_30/3} - Obligation: innermost runtime complexity wrt. defined symbols {a__incr#,a__oddNs#,a__pairNs#,a__repItems#,a__tail# ,a__take#,a__zip#,mark#} and constructors {0,cons,incr,nil,oddNs,pair,pairNs,repItems,s,tail,take,zip} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:a__incr#(cons(X,XS)) -> c_2(mark#(X)) -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 2:S:a__oddNs#() -> c_3(a__incr#(a__pairNs()),a__pairNs#()) -->_1 a__incr#(cons(X,XS)) -> c_2(mark#(X)):1 3:S:a__repItems#(cons(X,XS)) -> c_8(mark#(X)) -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 4:S:a__tail#(cons(X,XS)) -> c_11(mark#(XS)) -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 5:S:a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)) -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 6:S:a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)) -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 7:S:mark#(cons(X1,X2)) -> c_20(mark#(X1)) -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 8:S:mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)) -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 a__incr#(cons(X,XS)) -> c_2(mark#(X)):1 9:S:mark#(oddNs()) -> c_23(a__oddNs#()) -->_1 a__oddNs#() -> c_3(a__incr#(a__pairNs()),a__pairNs#()):2 10:S:mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)) -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 11:S:mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)) -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 a__repItems#(cons(X,XS)) -> c_8(mark#(X)):3 12:S:mark#(s(X)) -> c_27(mark#(X)) -->_1 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_1 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_1 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_1 mark#(s(X)) -> c_27(mark#(X)):12 -->_1 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_1 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_1 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_1 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_1 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 13:S:mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)) -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 a__tail#(cons(X,XS)) -> c_11(mark#(XS)):4 14:S:mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_3 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_3 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_3 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_3 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_3 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_3 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_3 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)):5 15:S:mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_2 mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):15 -->_3 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_2 mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):14 -->_3 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_2 mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)):13 -->_3 mark#(s(X)) -> c_27(mark#(X)):12 -->_2 mark#(s(X)) -> c_27(mark#(X)):12 -->_3 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_2 mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)):11 -->_3 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_2 mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)):10 -->_3 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_2 mark#(oddNs()) -> c_23(a__oddNs#()):9 -->_3 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_2 mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)):8 -->_3 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_2 mark#(cons(X1,X2)) -> c_20(mark#(X1)):7 -->_1 a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)):6 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: a__oddNs#() -> c_3(a__incr#(a__pairNs())) * Step 6: Failure MAYBE + Considered Problem: - Strict DPs: a__incr#(cons(X,XS)) -> c_2(mark#(X)) a__oddNs#() -> c_3(a__incr#(a__pairNs())) a__repItems#(cons(X,XS)) -> c_8(mark#(X)) a__tail#(cons(X,XS)) -> c_11(mark#(XS)) a__take#(s(N),cons(X,XS)) -> c_14(mark#(X)) a__zip#(cons(X,XS),cons(Y,YS)) -> c_17(mark#(X),mark#(Y)) mark#(cons(X1,X2)) -> c_20(mark#(X1)) mark#(incr(X)) -> c_21(a__incr#(mark(X)),mark#(X)) mark#(oddNs()) -> c_23(a__oddNs#()) mark#(pair(X1,X2)) -> c_24(mark#(X1),mark#(X2)) mark#(repItems(X)) -> c_26(a__repItems#(mark(X)),mark#(X)) mark#(s(X)) -> c_27(mark#(X)) mark#(tail(X)) -> c_28(a__tail#(mark(X)),mark#(X)) mark#(take(X1,X2)) -> c_29(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(zip(X1,X2)) -> c_30(a__zip#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak TRS: a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__oddNs() -> a__incr(a__pairNs()) a__oddNs() -> oddNs() a__pairNs() -> cons(0(),incr(oddNs())) a__pairNs() -> pairNs() a__repItems(X) -> repItems(X) a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS))) a__repItems(nil()) -> nil() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) a__take(X1,X2) -> take(X1,X2) a__take(0(),XS) -> nil() a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS)) a__zip(X,nil()) -> nil() a__zip(X1,X2) -> zip(X1,X2) a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS)) a__zip(nil(),XS) -> nil() mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(incr(X)) -> a__incr(mark(X)) mark(nil()) -> nil() mark(oddNs()) -> a__oddNs() mark(pair(X1,X2)) -> pair(mark(X1),mark(X2)) mark(pairNs()) -> a__pairNs() mark(repItems(X)) -> a__repItems(mark(X)) mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2)) - Signature: {a__incr/1,a__oddNs/0,a__pairNs/0,a__repItems/1,a__tail/1,a__take/2,a__zip/2,mark/1,a__incr#/1,a__oddNs#/0 ,a__pairNs#/0,a__repItems#/1,a__tail#/1,a__take#/2,a__zip#/2,mark#/1} / {0/0,cons/2,incr/1,nil/0,oddNs/0 ,pair/2,pairNs/0,repItems/1,s/1,tail/1,take/2,zip/2,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/0,c_16/0,c_17/2,c_18/0,c_19/0,c_20/1,c_21/2,c_22/0,c_23/1,c_24/2 ,c_25/1,c_26/2,c_27/1,c_28/2,c_29/3,c_30/3} - Obligation: innermost runtime complexity wrt. defined symbols {a__incr#,a__oddNs#,a__pairNs#,a__repItems#,a__tail# ,a__take#,a__zip#,mark#} and constructors {0,cons,incr,nil,oddNs,pair,pairNs,repItems,s,tail,take,zip} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE