MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a__add(X1,X2) -> add(X1,X2) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__fib(N) -> a__sel(mark(N),a__fib1(s(0()),s(0()))) a__fib(X) -> fib(X) a__fib1(X,Y) -> cons(mark(X),fib1(Y,add(X,Y))) a__fib1(X1,X2) -> fib1(X1,X2) a__sel(X1,X2) -> sel(X1,X2) a__sel(0(),cons(X,XS)) -> mark(X) a__sel(s(N),cons(X,XS)) -> a__sel(mark(N),mark(XS)) mark(0()) -> 0() mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(fib(X)) -> a__fib(mark(X)) mark(fib1(X1,X2)) -> a__fib1(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) - Signature: {a__add/2,a__fib/1,a__fib1/2,a__sel/2,mark/1} / {0/0,add/2,cons/2,fib/1,fib1/2,s/1,sel/2} - Obligation: innermost runtime complexity wrt. defined symbols {a__add,a__fib,a__fib1,a__sel,mark} and constructors {0 ,add,cons,fib,fib1,s,sel} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a__add#(X1,X2) -> c_1() a__add#(0(),X) -> c_2(mark#(X)) a__add#(s(X),Y) -> c_3(a__add#(mark(X),mark(Y)),mark#(X),mark#(Y)) a__fib#(N) -> c_4(a__sel#(mark(N),a__fib1(s(0()),s(0()))),mark#(N),a__fib1#(s(0()),s(0()))) a__fib#(X) -> c_5() a__fib1#(X,Y) -> c_6(mark#(X)) a__fib1#(X1,X2) -> c_7() a__sel#(X1,X2) -> c_8() a__sel#(0(),cons(X,XS)) -> c_9(mark#(X)) a__sel#(s(N),cons(X,XS)) -> c_10(a__sel#(mark(N),mark(XS)),mark#(N),mark#(XS)) mark#(0()) -> c_11() mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(cons(X1,X2)) -> c_13(mark#(X1)) mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)) mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(s(X)) -> c_16(mark#(X)) mark#(sel(X1,X2)) -> c_17(a__sel#(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__add#(X1,X2) -> c_1() a__add#(0(),X) -> c_2(mark#(X)) a__add#(s(X),Y) -> c_3(a__add#(mark(X),mark(Y)),mark#(X),mark#(Y)) a__fib#(N) -> c_4(a__sel#(mark(N),a__fib1(s(0()),s(0()))),mark#(N),a__fib1#(s(0()),s(0()))) a__fib#(X) -> c_5() a__fib1#(X,Y) -> c_6(mark#(X)) a__fib1#(X1,X2) -> c_7() a__sel#(X1,X2) -> c_8() a__sel#(0(),cons(X,XS)) -> c_9(mark#(X)) a__sel#(s(N),cons(X,XS)) -> c_10(a__sel#(mark(N),mark(XS)),mark#(N),mark#(XS)) mark#(0()) -> c_11() mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(cons(X1,X2)) -> c_13(mark#(X1)) mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)) mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(s(X)) -> c_16(mark#(X)) mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak TRS: a__add(X1,X2) -> add(X1,X2) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__fib(N) -> a__sel(mark(N),a__fib1(s(0()),s(0()))) a__fib(X) -> fib(X) a__fib1(X,Y) -> cons(mark(X),fib1(Y,add(X,Y))) a__fib1(X1,X2) -> fib1(X1,X2) a__sel(X1,X2) -> sel(X1,X2) a__sel(0(),cons(X,XS)) -> mark(X) a__sel(s(N),cons(X,XS)) -> a__sel(mark(N),mark(XS)) mark(0()) -> 0() mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(fib(X)) -> a__fib(mark(X)) mark(fib1(X1,X2)) -> a__fib1(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) - Signature: {a__add/2,a__fib/1,a__fib1/2,a__sel/2,mark/1,a__add#/2,a__fib#/1,a__fib1#/2,a__sel#/2,mark#/1} / {0/0,add/2 ,cons/2,fib/1,fib1/2,s/1,sel/2,c_1/0,c_2/1,c_3/3,c_4/3,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/3,c_11/0,c_12/3 ,c_13/1,c_14/2,c_15/3,c_16/1,c_17/3} - Obligation: innermost runtime complexity wrt. defined symbols {a__add#,a__fib#,a__fib1#,a__sel# ,mark#} and constructors {0,add,cons,fib,fib1,s,sel} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,5,7,8,11} by application of Pre({1,5,7,8,11}) = {2,3,4,6,9,10,12,13,14,15,16,17}. Here rules are labelled as follows: 1: a__add#(X1,X2) -> c_1() 2: a__add#(0(),X) -> c_2(mark#(X)) 3: a__add#(s(X),Y) -> c_3(a__add#(mark(X),mark(Y)),mark#(X),mark#(Y)) 4: a__fib#(N) -> c_4(a__sel#(mark(N),a__fib1(s(0()),s(0()))),mark#(N),a__fib1#(s(0()),s(0()))) 5: a__fib#(X) -> c_5() 6: a__fib1#(X,Y) -> c_6(mark#(X)) 7: a__fib1#(X1,X2) -> c_7() 8: a__sel#(X1,X2) -> c_8() 9: a__sel#(0(),cons(X,XS)) -> c_9(mark#(X)) 10: a__sel#(s(N),cons(X,XS)) -> c_10(a__sel#(mark(N),mark(XS)),mark#(N),mark#(XS)) 11: mark#(0()) -> c_11() 12: mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 13: mark#(cons(X1,X2)) -> c_13(mark#(X1)) 14: mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)) 15: mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 16: mark#(s(X)) -> c_16(mark#(X)) 17: mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: a__add#(0(),X) -> c_2(mark#(X)) a__add#(s(X),Y) -> c_3(a__add#(mark(X),mark(Y)),mark#(X),mark#(Y)) a__fib#(N) -> c_4(a__sel#(mark(N),a__fib1(s(0()),s(0()))),mark#(N),a__fib1#(s(0()),s(0()))) a__fib1#(X,Y) -> c_6(mark#(X)) a__sel#(0(),cons(X,XS)) -> c_9(mark#(X)) a__sel#(s(N),cons(X,XS)) -> c_10(a__sel#(mark(N),mark(XS)),mark#(N),mark#(XS)) mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(cons(X1,X2)) -> c_13(mark#(X1)) mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)) mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(s(X)) -> c_16(mark#(X)) mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak DPs: a__add#(X1,X2) -> c_1() a__fib#(X) -> c_5() a__fib1#(X1,X2) -> c_7() a__sel#(X1,X2) -> c_8() mark#(0()) -> c_11() - Weak TRS: a__add(X1,X2) -> add(X1,X2) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__fib(N) -> a__sel(mark(N),a__fib1(s(0()),s(0()))) a__fib(X) -> fib(X) a__fib1(X,Y) -> cons(mark(X),fib1(Y,add(X,Y))) a__fib1(X1,X2) -> fib1(X1,X2) a__sel(X1,X2) -> sel(X1,X2) a__sel(0(),cons(X,XS)) -> mark(X) a__sel(s(N),cons(X,XS)) -> a__sel(mark(N),mark(XS)) mark(0()) -> 0() mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(fib(X)) -> a__fib(mark(X)) mark(fib1(X1,X2)) -> a__fib1(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) - Signature: {a__add/2,a__fib/1,a__fib1/2,a__sel/2,mark/1,a__add#/2,a__fib#/1,a__fib1#/2,a__sel#/2,mark#/1} / {0/0,add/2 ,cons/2,fib/1,fib1/2,s/1,sel/2,c_1/0,c_2/1,c_3/3,c_4/3,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/3,c_11/0,c_12/3 ,c_13/1,c_14/2,c_15/3,c_16/1,c_17/3} - Obligation: innermost runtime complexity wrt. defined symbols {a__add#,a__fib#,a__fib1#,a__sel# ,mark#} and constructors {0,add,cons,fib,fib1,s,sel} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:a__add#(0(),X) -> c_2(mark#(X)) -->_1 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_1 mark#(s(X)) -> c_16(mark#(X)):11 -->_1 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_1 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_1 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_1 mark#(0()) -> c_11():17 2:S:a__add#(s(X),Y) -> c_3(a__add#(mark(X),mark(Y)),mark#(X),mark#(Y)) -->_3 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_2 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_3 mark#(s(X)) -> c_16(mark#(X)):11 -->_2 mark#(s(X)) -> c_16(mark#(X)):11 -->_3 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_2 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_3 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_2 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_3 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_2 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_3 mark#(0()) -> c_11():17 -->_2 mark#(0()) -> c_11():17 -->_1 a__add#(X1,X2) -> c_1():13 -->_1 a__add#(s(X),Y) -> c_3(a__add#(mark(X),mark(Y)),mark#(X),mark#(Y)):2 -->_1 a__add#(0(),X) -> c_2(mark#(X)):1 3:S:a__fib#(N) -> c_4(a__sel#(mark(N),a__fib1(s(0()),s(0()))),mark#(N),a__fib1#(s(0()),s(0()))) -->_2 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_2 mark#(s(X)) -> c_16(mark#(X)):11 -->_2 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_2 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_2 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_1 a__sel#(s(N),cons(X,XS)) -> c_10(a__sel#(mark(N),mark(XS)),mark#(N),mark#(XS)):6 -->_1 a__sel#(0(),cons(X,XS)) -> c_9(mark#(X)):5 -->_3 a__fib1#(X,Y) -> c_6(mark#(X)):4 -->_2 mark#(0()) -> c_11():17 -->_1 a__sel#(X1,X2) -> c_8():16 -->_3 a__fib1#(X1,X2) -> c_7():15 4:S:a__fib1#(X,Y) -> c_6(mark#(X)) -->_1 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_1 mark#(s(X)) -> c_16(mark#(X)):11 -->_1 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_1 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_1 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_1 mark#(0()) -> c_11():17 5:S:a__sel#(0(),cons(X,XS)) -> c_9(mark#(X)) -->_1 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_1 mark#(s(X)) -> c_16(mark#(X)):11 -->_1 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_1 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_1 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_1 mark#(0()) -> c_11():17 6:S:a__sel#(s(N),cons(X,XS)) -> c_10(a__sel#(mark(N),mark(XS)),mark#(N),mark#(XS)) -->_3 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_2 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_3 mark#(s(X)) -> c_16(mark#(X)):11 -->_2 mark#(s(X)) -> c_16(mark#(X)):11 -->_3 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_2 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_3 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_2 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_3 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_2 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_3 mark#(0()) -> c_11():17 -->_2 mark#(0()) -> c_11():17 -->_1 a__sel#(X1,X2) -> c_8():16 -->_1 a__sel#(s(N),cons(X,XS)) -> c_10(a__sel#(mark(N),mark(XS)),mark#(N),mark#(XS)):6 -->_1 a__sel#(0(),cons(X,XS)) -> c_9(mark#(X)):5 7:S:mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_2 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_3 mark#(s(X)) -> c_16(mark#(X)):11 -->_2 mark#(s(X)) -> c_16(mark#(X)):11 -->_3 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_2 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_3 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_2 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_3 mark#(0()) -> c_11():17 -->_2 mark#(0()) -> c_11():17 -->_1 a__add#(X1,X2) -> c_1():13 -->_3 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_2 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_1 a__add#(s(X),Y) -> c_3(a__add#(mark(X),mark(Y)),mark#(X),mark#(Y)):2 -->_1 a__add#(0(),X) -> c_2(mark#(X)):1 8:S:mark#(cons(X1,X2)) -> c_13(mark#(X1)) -->_1 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_1 mark#(s(X)) -> c_16(mark#(X)):11 -->_1 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_1 mark#(0()) -> c_11():17 -->_1 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_1 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 9:S:mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)) -->_2 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_2 mark#(s(X)) -> c_16(mark#(X)):11 -->_2 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(0()) -> c_11():17 -->_1 a__fib#(X) -> c_5():14 -->_2 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_2 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_2 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_1 a__fib#(N) -> c_4(a__sel#(mark(N),a__fib1(s(0()),s(0()))),mark#(N),a__fib1#(s(0()),s(0()))):3 10:S:mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_2 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_3 mark#(s(X)) -> c_16(mark#(X)):11 -->_2 mark#(s(X)) -> c_16(mark#(X)):11 -->_3 mark#(0()) -> c_11():17 -->_2 mark#(0()) -> c_11():17 -->_1 a__fib1#(X1,X2) -> c_7():15 -->_3 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_2 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_3 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_2 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_3 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_2 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_1 a__fib1#(X,Y) -> c_6(mark#(X)):4 11:S:mark#(s(X)) -> c_16(mark#(X)) -->_1 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_1 mark#(0()) -> c_11():17 -->_1 mark#(s(X)) -> c_16(mark#(X)):11 -->_1 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_1 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_1 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_1 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 12:S:mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(0()) -> c_11():17 -->_2 mark#(0()) -> c_11():17 -->_1 a__sel#(X1,X2) -> c_8():16 -->_3 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_2 mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):12 -->_3 mark#(s(X)) -> c_16(mark#(X)):11 -->_2 mark#(s(X)) -> c_16(mark#(X)):11 -->_3 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_2 mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):10 -->_3 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_2 mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)):9 -->_3 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_2 mark#(cons(X1,X2)) -> c_13(mark#(X1)):8 -->_3 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_2 mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):7 -->_1 a__sel#(s(N),cons(X,XS)) -> c_10(a__sel#(mark(N),mark(XS)),mark#(N),mark#(XS)):6 -->_1 a__sel#(0(),cons(X,XS)) -> c_9(mark#(X)):5 13:W:a__add#(X1,X2) -> c_1() 14:W:a__fib#(X) -> c_5() 15:W:a__fib1#(X1,X2) -> c_7() 16:W:a__sel#(X1,X2) -> c_8() 17:W:mark#(0()) -> c_11() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: a__add#(X1,X2) -> c_1() 14: a__fib#(X) -> c_5() 15: a__fib1#(X1,X2) -> c_7() 16: a__sel#(X1,X2) -> c_8() 17: mark#(0()) -> c_11() * Step 4: Failure MAYBE + Considered Problem: - Strict DPs: a__add#(0(),X) -> c_2(mark#(X)) a__add#(s(X),Y) -> c_3(a__add#(mark(X),mark(Y)),mark#(X),mark#(Y)) a__fib#(N) -> c_4(a__sel#(mark(N),a__fib1(s(0()),s(0()))),mark#(N),a__fib1#(s(0()),s(0()))) a__fib1#(X,Y) -> c_6(mark#(X)) a__sel#(0(),cons(X,XS)) -> c_9(mark#(X)) a__sel#(s(N),cons(X,XS)) -> c_10(a__sel#(mark(N),mark(XS)),mark#(N),mark#(XS)) mark#(add(X1,X2)) -> c_12(a__add#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(cons(X1,X2)) -> c_13(mark#(X1)) mark#(fib(X)) -> c_14(a__fib#(mark(X)),mark#(X)) mark#(fib1(X1,X2)) -> c_15(a__fib1#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(s(X)) -> c_16(mark#(X)) mark#(sel(X1,X2)) -> c_17(a__sel#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak TRS: a__add(X1,X2) -> add(X1,X2) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__fib(N) -> a__sel(mark(N),a__fib1(s(0()),s(0()))) a__fib(X) -> fib(X) a__fib1(X,Y) -> cons(mark(X),fib1(Y,add(X,Y))) a__fib1(X1,X2) -> fib1(X1,X2) a__sel(X1,X2) -> sel(X1,X2) a__sel(0(),cons(X,XS)) -> mark(X) a__sel(s(N),cons(X,XS)) -> a__sel(mark(N),mark(XS)) mark(0()) -> 0() mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(fib(X)) -> a__fib(mark(X)) mark(fib1(X1,X2)) -> a__fib1(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) - Signature: {a__add/2,a__fib/1,a__fib1/2,a__sel/2,mark/1,a__add#/2,a__fib#/1,a__fib1#/2,a__sel#/2,mark#/1} / {0/0,add/2 ,cons/2,fib/1,fib1/2,s/1,sel/2,c_1/0,c_2/1,c_3/3,c_4/3,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/3,c_11/0,c_12/3 ,c_13/1,c_14/2,c_15/3,c_16/1,c_17/3} - Obligation: innermost runtime complexity wrt. defined symbols {a__add#,a__fib#,a__fib1#,a__sel# ,mark#} and constructors {0,add,cons,fib,fib1,s,sel} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE