MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) dbl1(0()) -> 01() dbl1(s(X)) -> s1(s1(dbl1(X))) dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) dbls(nil()) -> nil() from(X) -> cons(X,from(s(X))) indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) indx(nil(),X) -> nil() quote(0()) -> 01() quote(dbl(X)) -> dbl1(X) quote(s(X)) -> s1(quote(X)) quote(sel(X,Y)) -> sel1(X,Y) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) sel1(0(),cons(X,Y)) -> X sel1(s(X),cons(Y,Z)) -> sel1(X,Z) - Signature: {dbl/1,dbl1/1,dbls/1,from/1,indx/2,quote/1,sel/2,sel1/2} / {0/0,01/0,cons/2,nil/0,s/1,s1/1} - Obligation: innermost runtime complexity wrt. defined symbols {dbl,dbl1,dbls,from,indx,quote,sel ,sel1} and constructors {0,01,cons,nil,s,s1} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs dbl#(0()) -> c_1() dbl#(s(X)) -> c_2(dbl#(X)) dbl1#(0()) -> c_3() dbl1#(s(X)) -> c_4(dbl1#(X)) dbls#(cons(X,Y)) -> c_5(dbl#(X),dbls#(Y)) dbls#(nil()) -> c_6() from#(X) -> c_7(from#(s(X))) indx#(cons(X,Y),Z) -> c_8(sel#(X,Z),indx#(Y,Z)) indx#(nil(),X) -> c_9() quote#(0()) -> c_10() quote#(dbl(X)) -> c_11(dbl1#(X)) quote#(s(X)) -> c_12(quote#(X)) quote#(sel(X,Y)) -> c_13(sel1#(X,Y)) sel#(0(),cons(X,Y)) -> c_14() sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)) sel1#(0(),cons(X,Y)) -> c_16() sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: dbl#(0()) -> c_1() dbl#(s(X)) -> c_2(dbl#(X)) dbl1#(0()) -> c_3() dbl1#(s(X)) -> c_4(dbl1#(X)) dbls#(cons(X,Y)) -> c_5(dbl#(X),dbls#(Y)) dbls#(nil()) -> c_6() from#(X) -> c_7(from#(s(X))) indx#(cons(X,Y),Z) -> c_8(sel#(X,Z),indx#(Y,Z)) indx#(nil(),X) -> c_9() quote#(0()) -> c_10() quote#(dbl(X)) -> c_11(dbl1#(X)) quote#(s(X)) -> c_12(quote#(X)) quote#(sel(X,Y)) -> c_13(sel1#(X,Y)) sel#(0(),cons(X,Y)) -> c_14() sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)) sel1#(0(),cons(X,Y)) -> c_16() sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)) - Weak TRS: dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) dbl1(0()) -> 01() dbl1(s(X)) -> s1(s1(dbl1(X))) dbls(cons(X,Y)) -> cons(dbl(X),dbls(Y)) dbls(nil()) -> nil() from(X) -> cons(X,from(s(X))) indx(cons(X,Y),Z) -> cons(sel(X,Z),indx(Y,Z)) indx(nil(),X) -> nil() quote(0()) -> 01() quote(dbl(X)) -> dbl1(X) quote(s(X)) -> s1(quote(X)) quote(sel(X,Y)) -> sel1(X,Y) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) sel1(0(),cons(X,Y)) -> X sel1(s(X),cons(Y,Z)) -> sel1(X,Z) - Signature: {dbl/1,dbl1/1,dbls/1,from/1,indx/2,quote/1,sel/2,sel1/2,dbl#/1,dbl1#/1,dbls#/1,from#/1,indx#/2,quote#/1 ,sel#/2,sel1#/2} / {0/0,01/0,cons/2,nil/0,s/1,s1/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2,c_6/0,c_7/1,c_8/2,c_9/0 ,c_10/0,c_11/1,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {dbl#,dbl1#,dbls#,from#,indx#,quote#,sel# ,sel1#} and constructors {0,01,cons,nil,s,s1} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: dbl#(0()) -> c_1() dbl#(s(X)) -> c_2(dbl#(X)) dbl1#(0()) -> c_3() dbl1#(s(X)) -> c_4(dbl1#(X)) dbls#(cons(X,Y)) -> c_5(dbl#(X),dbls#(Y)) dbls#(nil()) -> c_6() from#(X) -> c_7(from#(s(X))) indx#(cons(X,Y),Z) -> c_8(sel#(X,Z),indx#(Y,Z)) indx#(nil(),X) -> c_9() quote#(0()) -> c_10() quote#(dbl(X)) -> c_11(dbl1#(X)) quote#(s(X)) -> c_12(quote#(X)) quote#(sel(X,Y)) -> c_13(sel1#(X,Y)) sel#(0(),cons(X,Y)) -> c_14() sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)) sel1#(0(),cons(X,Y)) -> c_16() sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: dbl#(0()) -> c_1() dbl#(s(X)) -> c_2(dbl#(X)) dbl1#(0()) -> c_3() dbl1#(s(X)) -> c_4(dbl1#(X)) dbls#(cons(X,Y)) -> c_5(dbl#(X),dbls#(Y)) dbls#(nil()) -> c_6() from#(X) -> c_7(from#(s(X))) indx#(cons(X,Y),Z) -> c_8(sel#(X,Z),indx#(Y,Z)) indx#(nil(),X) -> c_9() quote#(0()) -> c_10() quote#(dbl(X)) -> c_11(dbl1#(X)) quote#(s(X)) -> c_12(quote#(X)) quote#(sel(X,Y)) -> c_13(sel1#(X,Y)) sel#(0(),cons(X,Y)) -> c_14() sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)) sel1#(0(),cons(X,Y)) -> c_16() sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)) - Signature: {dbl/1,dbl1/1,dbls/1,from/1,indx/2,quote/1,sel/2,sel1/2,dbl#/1,dbl1#/1,dbls#/1,from#/1,indx#/2,quote#/1 ,sel#/2,sel1#/2} / {0/0,01/0,cons/2,nil/0,s/1,s1/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2,c_6/0,c_7/1,c_8/2,c_9/0 ,c_10/0,c_11/1,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {dbl#,dbl1#,dbls#,from#,indx#,quote#,sel# ,sel1#} and constructors {0,01,cons,nil,s,s1} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,6,9,10,14,16} by application of Pre({1,3,6,9,10,14,16}) = {2,4,5,8,11,12,13,15,17}. Here rules are labelled as follows: 1: dbl#(0()) -> c_1() 2: dbl#(s(X)) -> c_2(dbl#(X)) 3: dbl1#(0()) -> c_3() 4: dbl1#(s(X)) -> c_4(dbl1#(X)) 5: dbls#(cons(X,Y)) -> c_5(dbl#(X),dbls#(Y)) 6: dbls#(nil()) -> c_6() 7: from#(X) -> c_7(from#(s(X))) 8: indx#(cons(X,Y),Z) -> c_8(sel#(X,Z),indx#(Y,Z)) 9: indx#(nil(),X) -> c_9() 10: quote#(0()) -> c_10() 11: quote#(dbl(X)) -> c_11(dbl1#(X)) 12: quote#(s(X)) -> c_12(quote#(X)) 13: quote#(sel(X,Y)) -> c_13(sel1#(X,Y)) 14: sel#(0(),cons(X,Y)) -> c_14() 15: sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)) 16: sel1#(0(),cons(X,Y)) -> c_16() 17: sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: dbl#(s(X)) -> c_2(dbl#(X)) dbl1#(s(X)) -> c_4(dbl1#(X)) dbls#(cons(X,Y)) -> c_5(dbl#(X),dbls#(Y)) from#(X) -> c_7(from#(s(X))) indx#(cons(X,Y),Z) -> c_8(sel#(X,Z),indx#(Y,Z)) quote#(dbl(X)) -> c_11(dbl1#(X)) quote#(s(X)) -> c_12(quote#(X)) quote#(sel(X,Y)) -> c_13(sel1#(X,Y)) sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)) sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)) - Weak DPs: dbl#(0()) -> c_1() dbl1#(0()) -> c_3() dbls#(nil()) -> c_6() indx#(nil(),X) -> c_9() quote#(0()) -> c_10() sel#(0(),cons(X,Y)) -> c_14() sel1#(0(),cons(X,Y)) -> c_16() - Signature: {dbl/1,dbl1/1,dbls/1,from/1,indx/2,quote/1,sel/2,sel1/2,dbl#/1,dbl1#/1,dbls#/1,from#/1,indx#/2,quote#/1 ,sel#/2,sel1#/2} / {0/0,01/0,cons/2,nil/0,s/1,s1/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2,c_6/0,c_7/1,c_8/2,c_9/0 ,c_10/0,c_11/1,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {dbl#,dbl1#,dbls#,from#,indx#,quote#,sel# ,sel1#} and constructors {0,01,cons,nil,s,s1} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:dbl#(s(X)) -> c_2(dbl#(X)) -->_1 dbl#(0()) -> c_1():11 -->_1 dbl#(s(X)) -> c_2(dbl#(X)):1 2:S:dbl1#(s(X)) -> c_4(dbl1#(X)) -->_1 dbl1#(0()) -> c_3():12 -->_1 dbl1#(s(X)) -> c_4(dbl1#(X)):2 3:S:dbls#(cons(X,Y)) -> c_5(dbl#(X),dbls#(Y)) -->_2 dbls#(nil()) -> c_6():13 -->_1 dbl#(0()) -> c_1():11 -->_2 dbls#(cons(X,Y)) -> c_5(dbl#(X),dbls#(Y)):3 -->_1 dbl#(s(X)) -> c_2(dbl#(X)):1 4:S:from#(X) -> c_7(from#(s(X))) -->_1 from#(X) -> c_7(from#(s(X))):4 5:S:indx#(cons(X,Y),Z) -> c_8(sel#(X,Z),indx#(Y,Z)) -->_1 sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)):9 -->_1 sel#(0(),cons(X,Y)) -> c_14():16 -->_2 indx#(nil(),X) -> c_9():14 -->_2 indx#(cons(X,Y),Z) -> c_8(sel#(X,Z),indx#(Y,Z)):5 6:S:quote#(dbl(X)) -> c_11(dbl1#(X)) -->_1 dbl1#(0()) -> c_3():12 -->_1 dbl1#(s(X)) -> c_4(dbl1#(X)):2 7:S:quote#(s(X)) -> c_12(quote#(X)) -->_1 quote#(sel(X,Y)) -> c_13(sel1#(X,Y)):8 -->_1 quote#(0()) -> c_10():15 -->_1 quote#(s(X)) -> c_12(quote#(X)):7 -->_1 quote#(dbl(X)) -> c_11(dbl1#(X)):6 8:S:quote#(sel(X,Y)) -> c_13(sel1#(X,Y)) -->_1 sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)):10 -->_1 sel1#(0(),cons(X,Y)) -> c_16():17 9:S:sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)) -->_1 sel#(0(),cons(X,Y)) -> c_14():16 -->_1 sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)):9 10:S:sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)) -->_1 sel1#(0(),cons(X,Y)) -> c_16():17 -->_1 sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)):10 11:W:dbl#(0()) -> c_1() 12:W:dbl1#(0()) -> c_3() 13:W:dbls#(nil()) -> c_6() 14:W:indx#(nil(),X) -> c_9() 15:W:quote#(0()) -> c_10() 16:W:sel#(0(),cons(X,Y)) -> c_14() 17:W:sel1#(0(),cons(X,Y)) -> c_16() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 15: quote#(0()) -> c_10() 17: sel1#(0(),cons(X,Y)) -> c_16() 14: indx#(nil(),X) -> c_9() 16: sel#(0(),cons(X,Y)) -> c_14() 13: dbls#(nil()) -> c_6() 12: dbl1#(0()) -> c_3() 11: dbl#(0()) -> c_1() * Step 5: WeightGap MAYBE + Considered Problem: - Strict DPs: dbl#(s(X)) -> c_2(dbl#(X)) dbl1#(s(X)) -> c_4(dbl1#(X)) dbls#(cons(X,Y)) -> c_5(dbl#(X),dbls#(Y)) from#(X) -> c_7(from#(s(X))) indx#(cons(X,Y),Z) -> c_8(sel#(X,Z),indx#(Y,Z)) quote#(dbl(X)) -> c_11(dbl1#(X)) quote#(s(X)) -> c_12(quote#(X)) quote#(sel(X,Y)) -> c_13(sel1#(X,Y)) sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)) sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)) - Signature: {dbl/1,dbl1/1,dbls/1,from/1,indx/2,quote/1,sel/2,sel1/2,dbl#/1,dbl1#/1,dbls#/1,from#/1,indx#/2,quote#/1 ,sel#/2,sel1#/2} / {0/0,01/0,cons/2,nil/0,s/1,s1/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2,c_6/0,c_7/1,c_8/2,c_9/0 ,c_10/0,c_11/1,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {dbl#,dbl1#,dbls#,from#,indx#,quote#,sel# ,sel1#} and constructors {0,01,cons,nil,s,s1} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1,2}, uargs(c_7) = {1}, uargs(c_8) = {1,2}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_17) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(01) = [0] p(cons) = [0] p(dbl) = [0] p(dbl1) = [0] p(dbls) = [0] p(from) = [1] p(indx) = [0] p(nil) = [0] p(quote) = [0] p(s) = [1] p(s1) = [0] p(sel) = [0] p(sel1) = [1] x1 + [0] p(dbl#) = [9] p(dbl1#) = [1] p(dbls#) = [0] p(from#) = [13] x1 + [0] p(indx#) = [12] p(quote#) = [5] p(sel#) = [11] p(sel1#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [6] p(c_3) = [0] p(c_4) = [1] x1 + [5] p(c_5) = [1] x1 + [1] x2 + [8] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [1] x2 + [4] p(c_9) = [0] p(c_10) = [1] p(c_11) = [1] x1 + [5] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [3] p(c_14) = [0] p(c_15) = [1] x1 + [1] p(c_16) = [0] p(c_17) = [1] x1 + [0] Following rules are strictly oriented: quote#(sel(X,Y)) = [5] > [3] = c_13(sel1#(X,Y)) Following rules are (at-least) weakly oriented: dbl#(s(X)) = [9] >= [15] = c_2(dbl#(X)) dbl1#(s(X)) = [1] >= [6] = c_4(dbl1#(X)) dbls#(cons(X,Y)) = [0] >= [17] = c_5(dbl#(X),dbls#(Y)) from#(X) = [13] X + [0] >= [13] = c_7(from#(s(X))) indx#(cons(X,Y),Z) = [12] >= [27] = c_8(sel#(X,Z),indx#(Y,Z)) quote#(dbl(X)) = [5] >= [6] = c_11(dbl1#(X)) quote#(s(X)) = [5] >= [5] = c_12(quote#(X)) sel#(s(X),cons(Y,Z)) = [11] >= [12] = c_15(sel#(X,Z)) sel1#(s(X),cons(Y,Z)) = [0] >= [0] = c_17(sel1#(X,Z)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 6: WeightGap MAYBE + Considered Problem: - Strict DPs: dbl#(s(X)) -> c_2(dbl#(X)) dbl1#(s(X)) -> c_4(dbl1#(X)) dbls#(cons(X,Y)) -> c_5(dbl#(X),dbls#(Y)) from#(X) -> c_7(from#(s(X))) indx#(cons(X,Y),Z) -> c_8(sel#(X,Z),indx#(Y,Z)) quote#(dbl(X)) -> c_11(dbl1#(X)) quote#(s(X)) -> c_12(quote#(X)) sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)) sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)) - Weak DPs: quote#(sel(X,Y)) -> c_13(sel1#(X,Y)) - Signature: {dbl/1,dbl1/1,dbls/1,from/1,indx/2,quote/1,sel/2,sel1/2,dbl#/1,dbl1#/1,dbls#/1,from#/1,indx#/2,quote#/1 ,sel#/2,sel1#/2} / {0/0,01/0,cons/2,nil/0,s/1,s1/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2,c_6/0,c_7/1,c_8/2,c_9/0 ,c_10/0,c_11/1,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {dbl#,dbl1#,dbls#,from#,indx#,quote#,sel# ,sel1#} and constructors {0,01,cons,nil,s,s1} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1,2}, uargs(c_7) = {1}, uargs(c_8) = {1,2}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_17) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [2] p(01) = [1] p(cons) = [0] p(dbl) = [1] x1 + [0] p(dbl1) = [1] x1 + [1] p(dbls) = [2] p(from) = [1] x1 + [0] p(indx) = [4] x2 + [0] p(nil) = [1] p(quote) = [1] x1 + [0] p(s) = [13] p(s1) = [2] p(sel) = [1] x1 + [1] x2 + [1] p(sel1) = [8] p(dbl#) = [12] p(dbl1#) = [1] p(dbls#) = [8] p(from#) = [1] x1 + [0] p(indx#) = [3] x2 + [4] p(quote#) = [8] p(sel#) = [0] p(sel1#) = [4] p(c_1) = [1] p(c_2) = [1] x1 + [15] p(c_3) = [2] p(c_4) = [1] x1 + [1] p(c_5) = [1] x1 + [1] x2 + [8] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [1] x2 + [9] p(c_9) = [2] p(c_10) = [8] p(c_11) = [1] x1 + [3] p(c_12) = [1] x1 + [1] p(c_13) = [1] x1 + [4] p(c_14) = [1] p(c_15) = [1] x1 + [0] p(c_16) = [0] p(c_17) = [1] x1 + [4] Following rules are strictly oriented: quote#(dbl(X)) = [8] > [4] = c_11(dbl1#(X)) Following rules are (at-least) weakly oriented: dbl#(s(X)) = [12] >= [27] = c_2(dbl#(X)) dbl1#(s(X)) = [1] >= [2] = c_4(dbl1#(X)) dbls#(cons(X,Y)) = [8] >= [28] = c_5(dbl#(X),dbls#(Y)) from#(X) = [1] X + [0] >= [13] = c_7(from#(s(X))) indx#(cons(X,Y),Z) = [3] Z + [4] >= [3] Z + [13] = c_8(sel#(X,Z),indx#(Y,Z)) quote#(s(X)) = [8] >= [9] = c_12(quote#(X)) quote#(sel(X,Y)) = [8] >= [8] = c_13(sel1#(X,Y)) sel#(s(X),cons(Y,Z)) = [0] >= [0] = c_15(sel#(X,Z)) sel1#(s(X),cons(Y,Z)) = [4] >= [8] = c_17(sel1#(X,Z)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: dbl#(s(X)) -> c_2(dbl#(X)) dbl1#(s(X)) -> c_4(dbl1#(X)) dbls#(cons(X,Y)) -> c_5(dbl#(X),dbls#(Y)) from#(X) -> c_7(from#(s(X))) indx#(cons(X,Y),Z) -> c_8(sel#(X,Z),indx#(Y,Z)) quote#(s(X)) -> c_12(quote#(X)) sel#(s(X),cons(Y,Z)) -> c_15(sel#(X,Z)) sel1#(s(X),cons(Y,Z)) -> c_17(sel1#(X,Z)) - Weak DPs: quote#(dbl(X)) -> c_11(dbl1#(X)) quote#(sel(X,Y)) -> c_13(sel1#(X,Y)) - Signature: {dbl/1,dbl1/1,dbls/1,from/1,indx/2,quote/1,sel/2,sel1/2,dbl#/1,dbl1#/1,dbls#/1,from#/1,indx#/2,quote#/1 ,sel#/2,sel1#/2} / {0/0,01/0,cons/2,nil/0,s/1,s1/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2,c_6/0,c_7/1,c_8/2,c_9/0 ,c_10/0,c_11/1,c_12/1,c_13/1,c_14/0,c_15/1,c_16/0,c_17/1} - Obligation: innermost runtime complexity wrt. defined symbols {dbl#,dbl1#,dbls#,from#,indx#,quote#,sel# ,sel1#} and constructors {0,01,cons,nil,s,s1} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE