MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a__head(X) -> head(X) a__head(cons(X,XS)) -> mark(X) a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__nats() -> cons(0(),incr(nats())) a__nats() -> nats() a__odds() -> a__incr(a__pairs()) a__odds() -> odds() a__pairs() -> cons(0(),incr(odds())) a__pairs() -> pairs() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(head(X)) -> a__head(mark(X)) mark(incr(X)) -> a__incr(mark(X)) mark(nats()) -> a__nats() mark(odds()) -> a__odds() mark(pairs()) -> a__pairs() mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) - Signature: {a__head/1,a__incr/1,a__nats/0,a__odds/0,a__pairs/0,a__tail/1,mark/1} / {0/0,cons/2,head/1,incr/1,nats/0 ,odds/0,pairs/0,s/1,tail/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__head,a__incr,a__nats,a__odds,a__pairs,a__tail ,mark} and constructors {0,cons,head,incr,nats,odds,pairs,s,tail} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a__head#(X) -> c_1() a__head#(cons(X,XS)) -> c_2(mark#(X)) a__incr#(X) -> c_3() a__incr#(cons(X,XS)) -> c_4(mark#(X)) a__nats#() -> c_5() a__nats#() -> c_6() a__odds#() -> c_7(a__incr#(a__pairs()),a__pairs#()) a__odds#() -> c_8() a__pairs#() -> c_9() a__pairs#() -> c_10() a__tail#(X) -> c_11() a__tail#(cons(X,XS)) -> c_12(mark#(XS)) mark#(0()) -> c_13() mark#(cons(X1,X2)) -> c_14(mark#(X1)) mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)) mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)) mark#(nats()) -> c_17(a__nats#()) mark#(odds()) -> c_18(a__odds#()) mark#(pairs()) -> c_19(a__pairs#()) mark#(s(X)) -> c_20(mark#(X)) mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__head#(X) -> c_1() a__head#(cons(X,XS)) -> c_2(mark#(X)) a__incr#(X) -> c_3() a__incr#(cons(X,XS)) -> c_4(mark#(X)) a__nats#() -> c_5() a__nats#() -> c_6() a__odds#() -> c_7(a__incr#(a__pairs()),a__pairs#()) a__odds#() -> c_8() a__pairs#() -> c_9() a__pairs#() -> c_10() a__tail#(X) -> c_11() a__tail#(cons(X,XS)) -> c_12(mark#(XS)) mark#(0()) -> c_13() mark#(cons(X1,X2)) -> c_14(mark#(X1)) mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)) mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)) mark#(nats()) -> c_17(a__nats#()) mark#(odds()) -> c_18(a__odds#()) mark#(pairs()) -> c_19(a__pairs#()) mark#(s(X)) -> c_20(mark#(X)) mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)) - Weak TRS: a__head(X) -> head(X) a__head(cons(X,XS)) -> mark(X) a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__nats() -> cons(0(),incr(nats())) a__nats() -> nats() a__odds() -> a__incr(a__pairs()) a__odds() -> odds() a__pairs() -> cons(0(),incr(odds())) a__pairs() -> pairs() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(head(X)) -> a__head(mark(X)) mark(incr(X)) -> a__incr(mark(X)) mark(nats()) -> a__nats() mark(odds()) -> a__odds() mark(pairs()) -> a__pairs() mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) - Signature: {a__head/1,a__incr/1,a__nats/0,a__odds/0,a__pairs/0,a__tail/1,mark/1,a__head#/1,a__incr#/1,a__nats#/0 ,a__odds#/0,a__pairs#/0,a__tail#/1,mark#/1} / {0/0,cons/2,head/1,incr/1,nats/0,odds/0,pairs/0,s/1,tail/1 ,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1,c_15/2,c_16/2 ,c_17/1,c_18/1,c_19/1,c_20/1,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__head#,a__incr#,a__nats#,a__odds#,a__pairs#,a__tail# ,mark#} and constructors {0,cons,head,incr,nats,odds,pairs,s,tail} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,5,6,8,9,10,11,13} by application of Pre({1,3,5,6,8,9,10,11,13}) = {2,4,7,12,14,15,16,17,18,19,20,21}. Here rules are labelled as follows: 1: a__head#(X) -> c_1() 2: a__head#(cons(X,XS)) -> c_2(mark#(X)) 3: a__incr#(X) -> c_3() 4: a__incr#(cons(X,XS)) -> c_4(mark#(X)) 5: a__nats#() -> c_5() 6: a__nats#() -> c_6() 7: a__odds#() -> c_7(a__incr#(a__pairs()),a__pairs#()) 8: a__odds#() -> c_8() 9: a__pairs#() -> c_9() 10: a__pairs#() -> c_10() 11: a__tail#(X) -> c_11() 12: a__tail#(cons(X,XS)) -> c_12(mark#(XS)) 13: mark#(0()) -> c_13() 14: mark#(cons(X1,X2)) -> c_14(mark#(X1)) 15: mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)) 16: mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)) 17: mark#(nats()) -> c_17(a__nats#()) 18: mark#(odds()) -> c_18(a__odds#()) 19: mark#(pairs()) -> c_19(a__pairs#()) 20: mark#(s(X)) -> c_20(mark#(X)) 21: mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__head#(cons(X,XS)) -> c_2(mark#(X)) a__incr#(cons(X,XS)) -> c_4(mark#(X)) a__odds#() -> c_7(a__incr#(a__pairs()),a__pairs#()) a__tail#(cons(X,XS)) -> c_12(mark#(XS)) mark#(cons(X1,X2)) -> c_14(mark#(X1)) mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)) mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)) mark#(nats()) -> c_17(a__nats#()) mark#(odds()) -> c_18(a__odds#()) mark#(pairs()) -> c_19(a__pairs#()) mark#(s(X)) -> c_20(mark#(X)) mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)) - Weak DPs: a__head#(X) -> c_1() a__incr#(X) -> c_3() a__nats#() -> c_5() a__nats#() -> c_6() a__odds#() -> c_8() a__pairs#() -> c_9() a__pairs#() -> c_10() a__tail#(X) -> c_11() mark#(0()) -> c_13() - Weak TRS: a__head(X) -> head(X) a__head(cons(X,XS)) -> mark(X) a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__nats() -> cons(0(),incr(nats())) a__nats() -> nats() a__odds() -> a__incr(a__pairs()) a__odds() -> odds() a__pairs() -> cons(0(),incr(odds())) a__pairs() -> pairs() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(head(X)) -> a__head(mark(X)) mark(incr(X)) -> a__incr(mark(X)) mark(nats()) -> a__nats() mark(odds()) -> a__odds() mark(pairs()) -> a__pairs() mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) - Signature: {a__head/1,a__incr/1,a__nats/0,a__odds/0,a__pairs/0,a__tail/1,mark/1,a__head#/1,a__incr#/1,a__nats#/0 ,a__odds#/0,a__pairs#/0,a__tail#/1,mark#/1} / {0/0,cons/2,head/1,incr/1,nats/0,odds/0,pairs/0,s/1,tail/1 ,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1,c_15/2,c_16/2 ,c_17/1,c_18/1,c_19/1,c_20/1,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__head#,a__incr#,a__nats#,a__odds#,a__pairs#,a__tail# ,mark#} and constructors {0,cons,head,incr,nats,odds,pairs,s,tail} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {8,10} by application of Pre({8,10}) = {1,2,4,5,6,7,11,12}. Here rules are labelled as follows: 1: a__head#(cons(X,XS)) -> c_2(mark#(X)) 2: a__incr#(cons(X,XS)) -> c_4(mark#(X)) 3: a__odds#() -> c_7(a__incr#(a__pairs()),a__pairs#()) 4: a__tail#(cons(X,XS)) -> c_12(mark#(XS)) 5: mark#(cons(X1,X2)) -> c_14(mark#(X1)) 6: mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)) 7: mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)) 8: mark#(nats()) -> c_17(a__nats#()) 9: mark#(odds()) -> c_18(a__odds#()) 10: mark#(pairs()) -> c_19(a__pairs#()) 11: mark#(s(X)) -> c_20(mark#(X)) 12: mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)) 13: a__head#(X) -> c_1() 14: a__incr#(X) -> c_3() 15: a__nats#() -> c_5() 16: a__nats#() -> c_6() 17: a__odds#() -> c_8() 18: a__pairs#() -> c_9() 19: a__pairs#() -> c_10() 20: a__tail#(X) -> c_11() 21: mark#(0()) -> c_13() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: a__head#(cons(X,XS)) -> c_2(mark#(X)) a__incr#(cons(X,XS)) -> c_4(mark#(X)) a__odds#() -> c_7(a__incr#(a__pairs()),a__pairs#()) a__tail#(cons(X,XS)) -> c_12(mark#(XS)) mark#(cons(X1,X2)) -> c_14(mark#(X1)) mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)) mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)) mark#(odds()) -> c_18(a__odds#()) mark#(s(X)) -> c_20(mark#(X)) mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)) - Weak DPs: a__head#(X) -> c_1() a__incr#(X) -> c_3() a__nats#() -> c_5() a__nats#() -> c_6() a__odds#() -> c_8() a__pairs#() -> c_9() a__pairs#() -> c_10() a__tail#(X) -> c_11() mark#(0()) -> c_13() mark#(nats()) -> c_17(a__nats#()) mark#(pairs()) -> c_19(a__pairs#()) - Weak TRS: a__head(X) -> head(X) a__head(cons(X,XS)) -> mark(X) a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__nats() -> cons(0(),incr(nats())) a__nats() -> nats() a__odds() -> a__incr(a__pairs()) a__odds() -> odds() a__pairs() -> cons(0(),incr(odds())) a__pairs() -> pairs() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(head(X)) -> a__head(mark(X)) mark(incr(X)) -> a__incr(mark(X)) mark(nats()) -> a__nats() mark(odds()) -> a__odds() mark(pairs()) -> a__pairs() mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) - Signature: {a__head/1,a__incr/1,a__nats/0,a__odds/0,a__pairs/0,a__tail/1,mark/1,a__head#/1,a__incr#/1,a__nats#/0 ,a__odds#/0,a__pairs#/0,a__tail#/1,mark#/1} / {0/0,cons/2,head/1,incr/1,nats/0,odds/0,pairs/0,s/1,tail/1 ,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1,c_15/2,c_16/2 ,c_17/1,c_18/1,c_19/1,c_20/1,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__head#,a__incr#,a__nats#,a__odds#,a__pairs#,a__tail# ,mark#} and constructors {0,cons,head,incr,nats,odds,pairs,s,tail} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:a__head#(cons(X,XS)) -> c_2(mark#(X)) -->_1 mark#(pairs()) -> c_19(a__pairs#()):21 -->_1 mark#(nats()) -> c_17(a__nats#()):20 -->_1 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_1 mark#(s(X)) -> c_20(mark#(X)):9 -->_1 mark#(odds()) -> c_18(a__odds#()):8 -->_1 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_1 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_1 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 -->_1 mark#(0()) -> c_13():19 2:S:a__incr#(cons(X,XS)) -> c_4(mark#(X)) -->_1 mark#(pairs()) -> c_19(a__pairs#()):21 -->_1 mark#(nats()) -> c_17(a__nats#()):20 -->_1 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_1 mark#(s(X)) -> c_20(mark#(X)):9 -->_1 mark#(odds()) -> c_18(a__odds#()):8 -->_1 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_1 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_1 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 -->_1 mark#(0()) -> c_13():19 3:S:a__odds#() -> c_7(a__incr#(a__pairs()),a__pairs#()) -->_2 a__pairs#() -> c_10():17 -->_2 a__pairs#() -> c_9():16 -->_1 a__incr#(X) -> c_3():12 -->_1 a__incr#(cons(X,XS)) -> c_4(mark#(X)):2 4:S:a__tail#(cons(X,XS)) -> c_12(mark#(XS)) -->_1 mark#(pairs()) -> c_19(a__pairs#()):21 -->_1 mark#(nats()) -> c_17(a__nats#()):20 -->_1 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_1 mark#(s(X)) -> c_20(mark#(X)):9 -->_1 mark#(odds()) -> c_18(a__odds#()):8 -->_1 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_1 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_1 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 -->_1 mark#(0()) -> c_13():19 5:S:mark#(cons(X1,X2)) -> c_14(mark#(X1)) -->_1 mark#(pairs()) -> c_19(a__pairs#()):21 -->_1 mark#(nats()) -> c_17(a__nats#()):20 -->_1 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_1 mark#(s(X)) -> c_20(mark#(X)):9 -->_1 mark#(odds()) -> c_18(a__odds#()):8 -->_1 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_1 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_1 mark#(0()) -> c_13():19 -->_1 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 6:S:mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)) -->_2 mark#(pairs()) -> c_19(a__pairs#()):21 -->_2 mark#(nats()) -> c_17(a__nats#()):20 -->_2 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_2 mark#(s(X)) -> c_20(mark#(X)):9 -->_2 mark#(odds()) -> c_18(a__odds#()):8 -->_2 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_2 mark#(0()) -> c_13():19 -->_1 a__head#(X) -> c_1():11 -->_2 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_2 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 -->_1 a__head#(cons(X,XS)) -> c_2(mark#(X)):1 7:S:mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)) -->_2 mark#(pairs()) -> c_19(a__pairs#()):21 -->_2 mark#(nats()) -> c_17(a__nats#()):20 -->_2 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_2 mark#(s(X)) -> c_20(mark#(X)):9 -->_2 mark#(odds()) -> c_18(a__odds#()):8 -->_2 mark#(0()) -> c_13():19 -->_1 a__incr#(X) -> c_3():12 -->_2 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_2 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_2 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 -->_1 a__incr#(cons(X,XS)) -> c_4(mark#(X)):2 8:S:mark#(odds()) -> c_18(a__odds#()) -->_1 a__odds#() -> c_8():15 -->_1 a__odds#() -> c_7(a__incr#(a__pairs()),a__pairs#()):3 9:S:mark#(s(X)) -> c_20(mark#(X)) -->_1 mark#(pairs()) -> c_19(a__pairs#()):21 -->_1 mark#(nats()) -> c_17(a__nats#()):20 -->_1 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_1 mark#(0()) -> c_13():19 -->_1 mark#(s(X)) -> c_20(mark#(X)):9 -->_1 mark#(odds()) -> c_18(a__odds#()):8 -->_1 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_1 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_1 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 10:S:mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)) -->_2 mark#(pairs()) -> c_19(a__pairs#()):21 -->_2 mark#(nats()) -> c_17(a__nats#()):20 -->_2 mark#(0()) -> c_13():19 -->_1 a__tail#(X) -> c_11():18 -->_2 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_2 mark#(s(X)) -> c_20(mark#(X)):9 -->_2 mark#(odds()) -> c_18(a__odds#()):8 -->_2 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_2 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_2 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 -->_1 a__tail#(cons(X,XS)) -> c_12(mark#(XS)):4 11:W:a__head#(X) -> c_1() 12:W:a__incr#(X) -> c_3() 13:W:a__nats#() -> c_5() 14:W:a__nats#() -> c_6() 15:W:a__odds#() -> c_8() 16:W:a__pairs#() -> c_9() 17:W:a__pairs#() -> c_10() 18:W:a__tail#(X) -> c_11() 19:W:mark#(0()) -> c_13() 20:W:mark#(nats()) -> c_17(a__nats#()) -->_1 a__nats#() -> c_6():14 -->_1 a__nats#() -> c_5():13 21:W:mark#(pairs()) -> c_19(a__pairs#()) -->_1 a__pairs#() -> c_10():17 -->_1 a__pairs#() -> c_9():16 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 11: a__head#(X) -> c_1() 12: a__incr#(X) -> c_3() 15: a__odds#() -> c_8() 18: a__tail#(X) -> c_11() 19: mark#(0()) -> c_13() 20: mark#(nats()) -> c_17(a__nats#()) 13: a__nats#() -> c_5() 14: a__nats#() -> c_6() 21: mark#(pairs()) -> c_19(a__pairs#()) 16: a__pairs#() -> c_9() 17: a__pairs#() -> c_10() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: a__head#(cons(X,XS)) -> c_2(mark#(X)) a__incr#(cons(X,XS)) -> c_4(mark#(X)) a__odds#() -> c_7(a__incr#(a__pairs()),a__pairs#()) a__tail#(cons(X,XS)) -> c_12(mark#(XS)) mark#(cons(X1,X2)) -> c_14(mark#(X1)) mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)) mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)) mark#(odds()) -> c_18(a__odds#()) mark#(s(X)) -> c_20(mark#(X)) mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)) - Weak TRS: a__head(X) -> head(X) a__head(cons(X,XS)) -> mark(X) a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__nats() -> cons(0(),incr(nats())) a__nats() -> nats() a__odds() -> a__incr(a__pairs()) a__odds() -> odds() a__pairs() -> cons(0(),incr(odds())) a__pairs() -> pairs() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(head(X)) -> a__head(mark(X)) mark(incr(X)) -> a__incr(mark(X)) mark(nats()) -> a__nats() mark(odds()) -> a__odds() mark(pairs()) -> a__pairs() mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) - Signature: {a__head/1,a__incr/1,a__nats/0,a__odds/0,a__pairs/0,a__tail/1,mark/1,a__head#/1,a__incr#/1,a__nats#/0 ,a__odds#/0,a__pairs#/0,a__tail#/1,mark#/1} / {0/0,cons/2,head/1,incr/1,nats/0,odds/0,pairs/0,s/1,tail/1 ,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1,c_15/2,c_16/2 ,c_17/1,c_18/1,c_19/1,c_20/1,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__head#,a__incr#,a__nats#,a__odds#,a__pairs#,a__tail# ,mark#} and constructors {0,cons,head,incr,nats,odds,pairs,s,tail} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:a__head#(cons(X,XS)) -> c_2(mark#(X)) -->_1 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_1 mark#(s(X)) -> c_20(mark#(X)):9 -->_1 mark#(odds()) -> c_18(a__odds#()):8 -->_1 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_1 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_1 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 2:S:a__incr#(cons(X,XS)) -> c_4(mark#(X)) -->_1 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_1 mark#(s(X)) -> c_20(mark#(X)):9 -->_1 mark#(odds()) -> c_18(a__odds#()):8 -->_1 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_1 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_1 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 3:S:a__odds#() -> c_7(a__incr#(a__pairs()),a__pairs#()) -->_1 a__incr#(cons(X,XS)) -> c_4(mark#(X)):2 4:S:a__tail#(cons(X,XS)) -> c_12(mark#(XS)) -->_1 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_1 mark#(s(X)) -> c_20(mark#(X)):9 -->_1 mark#(odds()) -> c_18(a__odds#()):8 -->_1 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_1 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_1 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 5:S:mark#(cons(X1,X2)) -> c_14(mark#(X1)) -->_1 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_1 mark#(s(X)) -> c_20(mark#(X)):9 -->_1 mark#(odds()) -> c_18(a__odds#()):8 -->_1 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_1 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_1 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 6:S:mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)) -->_2 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_2 mark#(s(X)) -> c_20(mark#(X)):9 -->_2 mark#(odds()) -> c_18(a__odds#()):8 -->_2 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_2 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_2 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 -->_1 a__head#(cons(X,XS)) -> c_2(mark#(X)):1 7:S:mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)) -->_2 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_2 mark#(s(X)) -> c_20(mark#(X)):9 -->_2 mark#(odds()) -> c_18(a__odds#()):8 -->_2 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_2 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_2 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 -->_1 a__incr#(cons(X,XS)) -> c_4(mark#(X)):2 8:S:mark#(odds()) -> c_18(a__odds#()) -->_1 a__odds#() -> c_7(a__incr#(a__pairs()),a__pairs#()):3 9:S:mark#(s(X)) -> c_20(mark#(X)) -->_1 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_1 mark#(s(X)) -> c_20(mark#(X)):9 -->_1 mark#(odds()) -> c_18(a__odds#()):8 -->_1 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_1 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_1 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 10:S:mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)) -->_2 mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)):10 -->_2 mark#(s(X)) -> c_20(mark#(X)):9 -->_2 mark#(odds()) -> c_18(a__odds#()):8 -->_2 mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)):7 -->_2 mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)):6 -->_2 mark#(cons(X1,X2)) -> c_14(mark#(X1)):5 -->_1 a__tail#(cons(X,XS)) -> c_12(mark#(XS)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: a__odds#() -> c_7(a__incr#(a__pairs())) * Step 6: Failure MAYBE + Considered Problem: - Strict DPs: a__head#(cons(X,XS)) -> c_2(mark#(X)) a__incr#(cons(X,XS)) -> c_4(mark#(X)) a__odds#() -> c_7(a__incr#(a__pairs())) a__tail#(cons(X,XS)) -> c_12(mark#(XS)) mark#(cons(X1,X2)) -> c_14(mark#(X1)) mark#(head(X)) -> c_15(a__head#(mark(X)),mark#(X)) mark#(incr(X)) -> c_16(a__incr#(mark(X)),mark#(X)) mark#(odds()) -> c_18(a__odds#()) mark#(s(X)) -> c_20(mark#(X)) mark#(tail(X)) -> c_21(a__tail#(mark(X)),mark#(X)) - Weak TRS: a__head(X) -> head(X) a__head(cons(X,XS)) -> mark(X) a__incr(X) -> incr(X) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__nats() -> cons(0(),incr(nats())) a__nats() -> nats() a__odds() -> a__incr(a__pairs()) a__odds() -> odds() a__pairs() -> cons(0(),incr(odds())) a__pairs() -> pairs() a__tail(X) -> tail(X) a__tail(cons(X,XS)) -> mark(XS) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(head(X)) -> a__head(mark(X)) mark(incr(X)) -> a__incr(mark(X)) mark(nats()) -> a__nats() mark(odds()) -> a__odds() mark(pairs()) -> a__pairs() mark(s(X)) -> s(mark(X)) mark(tail(X)) -> a__tail(mark(X)) - Signature: {a__head/1,a__incr/1,a__nats/0,a__odds/0,a__pairs/0,a__tail/1,mark/1,a__head#/1,a__incr#/1,a__nats#/0 ,a__odds#/0,a__pairs#/0,a__tail#/1,mark#/1} / {0/0,cons/2,head/1,incr/1,nats/0,odds/0,pairs/0,s/1,tail/1 ,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/0,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/1,c_15/2,c_16/2 ,c_17/1,c_18/1,c_19/1,c_20/1,c_21/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__head#,a__incr#,a__nats#,a__odds#,a__pairs#,a__tail# ,mark#} and constructors {0,cons,head,incr,nats,odds,pairs,s,tail} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE