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