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