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