MAYBE
* Step 1: InnermostRuleRemoval MAYBE
+ Considered Problem:
- Strict TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
fcons(X,Z) -> cons(X,Z)
first(X1,X2) -> n__first(X1,X2)
first(0(),Z) -> nil()
first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z)))
first1(0(),Z) -> nil1()
first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z)))
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
quote(n__0()) -> 01()
quote(n__s(X)) -> s1(quote(activate(X)))
quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z))
quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z)))
quote1(n__first(X,Z)) -> first1(activate(X),activate(Z))
quote1(n__nil()) -> nil1()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
sel(0(),cons(X,Z)) -> X
sel(s(X),cons(Y,Z)) -> sel(X,activate(Z))
sel1(0(),cons(X,Z)) -> quote(X)
sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z))
unquote(01()) -> 0()
unquote(s1(X)) -> s(unquote(X))
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
unquote1(nil1()) -> nil()
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0,n__s/1,n__sel/2,nil1/0,s1/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0,activate,cons,fcons,first,first1,from,nil,quote,quote1
,s,sel,sel1,unquote,unquote1} and constructors {01,cons1,n__0,n__cons,n__first,n__from,n__nil,n__s,n__sel
,nil1,s1}
+ Applied Processor:
InnermostRuleRemoval
+ Details:
Arguments of following rules are not normal-forms.
first(0(),Z) -> nil()
first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z)))
first1(0(),Z) -> nil1()
first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z)))
sel(0(),cons(X,Z)) -> X
sel(s(X),cons(Y,Z)) -> sel(X,activate(Z))
sel1(0(),cons(X,Z)) -> quote(X)
sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z))
All above mentioned rules can be savely removed.
* Step 2: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
fcons(X,Z) -> cons(X,Z)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
quote(n__0()) -> 01()
quote(n__s(X)) -> s1(quote(activate(X)))
quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z))
quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z)))
quote1(n__first(X,Z)) -> first1(activate(X),activate(Z))
quote1(n__nil()) -> nil1()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
unquote(01()) -> 0()
unquote(s1(X)) -> s(unquote(X))
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
unquote1(nil1()) -> nil()
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0,n__s/1,n__sel/2,nil1/0,s1/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0,activate,cons,fcons,first,first1,from,nil,quote,quote1
,s,sel,sel1,unquote,unquote1} and constructors {01,cons1,n__0,n__cons,n__first,n__from,n__nil,n__s,n__sel
,nil1,s1}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
0#() -> c_1()
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
activate#(n__from(X)) -> c_6(from#(X))
activate#(n__nil()) -> c_7(nil#())
activate#(n__s(X)) -> c_8(s#(X))
activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
cons#(X1,X2) -> c_10()
fcons#(X,Z) -> c_11(cons#(X,Z))
first#(X1,X2) -> c_12()
from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
from#(X) -> c_14()
nil#() -> c_15()
quote#(n__0()) -> c_16()
quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__nil()) -> c_21()
s#(X) -> c_22()
sel#(X1,X2) -> c_23()
unquote#(01()) -> c_24(0#())
unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
unquote1#(nil1()) -> c_27(nil#())
Weak DPs
and mark the set of starting terms.
* Step 3: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
0#() -> c_1()
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
activate#(n__from(X)) -> c_6(from#(X))
activate#(n__nil()) -> c_7(nil#())
activate#(n__s(X)) -> c_8(s#(X))
activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
cons#(X1,X2) -> c_10()
fcons#(X,Z) -> c_11(cons#(X,Z))
first#(X1,X2) -> c_12()
from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
from#(X) -> c_14()
nil#() -> c_15()
quote#(n__0()) -> c_16()
quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__nil()) -> c_21()
s#(X) -> c_22()
sel#(X1,X2) -> c_23()
unquote#(01()) -> c_24(0#())
unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
unquote1#(nil1()) -> c_27(nil#())
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
fcons(X,Z) -> cons(X,Z)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
quote(n__0()) -> 01()
quote(n__s(X)) -> s1(quote(activate(X)))
quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z))
quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z)))
quote1(n__first(X,Z)) -> first1(activate(X),activate(Z))
quote1(n__nil()) -> nil1()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
unquote(01()) -> 0()
unquote(s1(X)) -> s(unquote(X))
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
unquote1(nil1()) -> nil()
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
fcons(X,Z) -> cons(X,Z)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
unquote(01()) -> 0()
unquote(s1(X)) -> s(unquote(X))
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
unquote1(nil1()) -> nil()
0#() -> c_1()
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
activate#(n__from(X)) -> c_6(from#(X))
activate#(n__nil()) -> c_7(nil#())
activate#(n__s(X)) -> c_8(s#(X))
activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
cons#(X1,X2) -> c_10()
fcons#(X,Z) -> c_11(cons#(X,Z))
first#(X1,X2) -> c_12()
from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
from#(X) -> c_14()
nil#() -> c_15()
quote#(n__0()) -> c_16()
quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__nil()) -> c_21()
s#(X) -> c_22()
sel#(X1,X2) -> c_23()
unquote#(01()) -> c_24(0#())
unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
unquote1#(nil1()) -> c_27(nil#())
* Step 4: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
0#() -> c_1()
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
activate#(n__from(X)) -> c_6(from#(X))
activate#(n__nil()) -> c_7(nil#())
activate#(n__s(X)) -> c_8(s#(X))
activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
cons#(X1,X2) -> c_10()
fcons#(X,Z) -> c_11(cons#(X,Z))
first#(X1,X2) -> c_12()
from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
from#(X) -> c_14()
nil#() -> c_15()
quote#(n__0()) -> c_16()
quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__nil()) -> c_21()
s#(X) -> c_22()
sel#(X1,X2) -> c_23()
unquote#(01()) -> c_24(0#())
unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
unquote1#(nil1()) -> c_27(nil#())
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
fcons(X,Z) -> cons(X,Z)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
unquote(01()) -> 0()
unquote(s1(X)) -> s(unquote(X))
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
unquote1(nil1()) -> nil()
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,2,10,12,14,15,16,21,22,23}
by application of
Pre({1,2,10,12,14,15,16,21,22,23}) = {3,4,5,6,7,8,9,11,13,17,18,19,20,24,25,27}.
Here rules are labelled as follows:
1: 0#() -> c_1()
2: activate#(X) -> c_2()
3: activate#(n__0()) -> c_3(0#())
4: activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
5: activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
6: activate#(n__from(X)) -> c_6(from#(X))
7: activate#(n__nil()) -> c_7(nil#())
8: activate#(n__s(X)) -> c_8(s#(X))
9: activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
10: cons#(X1,X2) -> c_10()
11: fcons#(X,Z) -> c_11(cons#(X,Z))
12: first#(X1,X2) -> c_12()
13: from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
14: from#(X) -> c_14()
15: nil#() -> c_15()
16: quote#(n__0()) -> c_16()
17: quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
18: quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
19: quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
20: quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
21: quote1#(n__nil()) -> c_21()
22: s#(X) -> c_22()
23: sel#(X1,X2) -> c_23()
24: unquote#(01()) -> c_24(0#())
25: unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
26: unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
27: unquote1#(nil1()) -> c_27(nil#())
* Step 5: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
activate#(n__0()) -> c_3(0#())
activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
activate#(n__from(X)) -> c_6(from#(X))
activate#(n__nil()) -> c_7(nil#())
activate#(n__s(X)) -> c_8(s#(X))
activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
fcons#(X,Z) -> c_11(cons#(X,Z))
from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
unquote#(01()) -> c_24(0#())
unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
unquote1#(nil1()) -> c_27(nil#())
- Weak DPs:
0#() -> c_1()
activate#(X) -> c_2()
cons#(X1,X2) -> c_10()
first#(X1,X2) -> c_12()
from#(X) -> c_14()
nil#() -> c_15()
quote#(n__0()) -> c_16()
quote1#(n__nil()) -> c_21()
s#(X) -> c_22()
sel#(X1,X2) -> c_23()
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
fcons(X,Z) -> cons(X,Z)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
unquote(01()) -> 0()
unquote(s1(X)) -> s(unquote(X))
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
unquote1(nil1()) -> nil()
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,2,3,5,6,7,8,9,14,17}
by application of
Pre({1,2,3,5,6,7,8,9,14,17}) = {4,10,11,12,13,15,16}.
Here rules are labelled as follows:
1: activate#(n__0()) -> c_3(0#())
2: activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
3: activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
4: activate#(n__from(X)) -> c_6(from#(X))
5: activate#(n__nil()) -> c_7(nil#())
6: activate#(n__s(X)) -> c_8(s#(X))
7: activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
8: fcons#(X,Z) -> c_11(cons#(X,Z))
9: from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
10: quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
11: quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
12: quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
13: quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
14: unquote#(01()) -> c_24(0#())
15: unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
16: unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
17: unquote1#(nil1()) -> c_27(nil#())
18: 0#() -> c_1()
19: activate#(X) -> c_2()
20: cons#(X1,X2) -> c_10()
21: first#(X1,X2) -> c_12()
22: from#(X) -> c_14()
23: nil#() -> c_15()
24: quote#(n__0()) -> c_16()
25: quote1#(n__nil()) -> c_21()
26: s#(X) -> c_22()
27: sel#(X1,X2) -> c_23()
* Step 6: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
activate#(n__from(X)) -> c_6(from#(X))
quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
- Weak DPs:
0#() -> c_1()
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
activate#(n__nil()) -> c_7(nil#())
activate#(n__s(X)) -> c_8(s#(X))
activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
cons#(X1,X2) -> c_10()
fcons#(X,Z) -> c_11(cons#(X,Z))
first#(X1,X2) -> c_12()
from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
from#(X) -> c_14()
nil#() -> c_15()
quote#(n__0()) -> c_16()
quote1#(n__nil()) -> c_21()
s#(X) -> c_22()
sel#(X1,X2) -> c_23()
unquote#(01()) -> c_24(0#())
unquote1#(nil1()) -> c_27(nil#())
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
fcons(X,Z) -> cons(X,Z)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
unquote(01()) -> 0()
unquote(s1(X)) -> s(unquote(X))
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
unquote1(nil1()) -> nil()
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1}
by application of
Pre({1}) = {2,3,4,5}.
Here rules are labelled as follows:
1: activate#(n__from(X)) -> c_6(from#(X))
2: quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
3: quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
4: quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
5: quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
6: unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
7: unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
8: 0#() -> c_1()
9: activate#(X) -> c_2()
10: activate#(n__0()) -> c_3(0#())
11: activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
12: activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
13: activate#(n__nil()) -> c_7(nil#())
14: activate#(n__s(X)) -> c_8(s#(X))
15: activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
16: cons#(X1,X2) -> c_10()
17: fcons#(X,Z) -> c_11(cons#(X,Z))
18: first#(X1,X2) -> c_12()
19: from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
20: from#(X) -> c_14()
21: nil#() -> c_15()
22: quote#(n__0()) -> c_16()
23: quote1#(n__nil()) -> c_21()
24: s#(X) -> c_22()
25: sel#(X1,X2) -> c_23()
26: unquote#(01()) -> c_24(0#())
27: unquote1#(nil1()) -> c_27(nil#())
* Step 7: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
- Weak DPs:
0#() -> c_1()
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
activate#(n__from(X)) -> c_6(from#(X))
activate#(n__nil()) -> c_7(nil#())
activate#(n__s(X)) -> c_8(s#(X))
activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
cons#(X1,X2) -> c_10()
fcons#(X,Z) -> c_11(cons#(X,Z))
first#(X1,X2) -> c_12()
from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
from#(X) -> c_14()
nil#() -> c_15()
quote#(n__0()) -> c_16()
quote1#(n__nil()) -> c_21()
s#(X) -> c_22()
sel#(X1,X2) -> c_23()
unquote#(01()) -> c_24(0#())
unquote1#(nil1()) -> c_27(nil#())
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
fcons(X,Z) -> cons(X,Z)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
unquote(01()) -> 0()
unquote(s1(X)) -> s(unquote(X))
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
unquote1(nil1()) -> nil()
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2,4}
by application of
Pre({2,4}) = {1,3}.
Here rules are labelled as follows:
1: quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
2: quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
3: quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
4: quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
5: unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
6: unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
7: 0#() -> c_1()
8: activate#(X) -> c_2()
9: activate#(n__0()) -> c_3(0#())
10: activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
11: activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
12: activate#(n__from(X)) -> c_6(from#(X))
13: activate#(n__nil()) -> c_7(nil#())
14: activate#(n__s(X)) -> c_8(s#(X))
15: activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
16: cons#(X1,X2) -> c_10()
17: fcons#(X,Z) -> c_11(cons#(X,Z))
18: first#(X1,X2) -> c_12()
19: from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
20: from#(X) -> c_14()
21: nil#() -> c_15()
22: quote#(n__0()) -> c_16()
23: quote1#(n__nil()) -> c_21()
24: s#(X) -> c_22()
25: sel#(X1,X2) -> c_23()
26: unquote#(01()) -> c_24(0#())
27: unquote1#(nil1()) -> c_27(nil#())
* Step 8: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
- Weak DPs:
0#() -> c_1()
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
activate#(n__from(X)) -> c_6(from#(X))
activate#(n__nil()) -> c_7(nil#())
activate#(n__s(X)) -> c_8(s#(X))
activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
cons#(X1,X2) -> c_10()
fcons#(X,Z) -> c_11(cons#(X,Z))
first#(X1,X2) -> c_12()
from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
from#(X) -> c_14()
nil#() -> c_15()
quote#(n__0()) -> c_16()
quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
quote1#(n__nil()) -> c_21()
s#(X) -> c_22()
sel#(X1,X2) -> c_23()
unquote#(01()) -> c_24(0#())
unquote1#(nil1()) -> c_27(nil#())
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
fcons(X,Z) -> cons(X,Z)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
unquote(01()) -> 0()
unquote(s1(X)) -> s(unquote(X))
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
unquote1(nil1()) -> nil()
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
-->_1 quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)):21
-->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13
-->_2 activate#(n__s(X)) -> c_8(s#(X)):12
-->_2 activate#(n__nil()) -> c_7(nil#()):11
-->_2 activate#(n__from(X)) -> c_6(from#(X)):10
-->_2 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9
-->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8
-->_2 activate#(n__0()) -> c_3(0#()):7
-->_1 quote#(n__0()) -> c_16():20
-->_2 activate#(X) -> c_2():6
-->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):1
2:S:quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
-->_3 quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)):22
-->_1 quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)):21
-->_4 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13
-->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13
-->_4 activate#(n__s(X)) -> c_8(s#(X)):12
-->_2 activate#(n__s(X)) -> c_8(s#(X)):12
-->_4 activate#(n__nil()) -> c_7(nil#()):11
-->_2 activate#(n__nil()) -> c_7(nil#()):11
-->_4 activate#(n__from(X)) -> c_6(from#(X)):10
-->_2 activate#(n__from(X)) -> c_6(from#(X)):10
-->_4 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9
-->_2 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9
-->_4 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8
-->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8
-->_4 activate#(n__0()) -> c_3(0#()):7
-->_2 activate#(n__0()) -> c_3(0#()):7
-->_3 quote1#(n__nil()) -> c_21():23
-->_1 quote#(n__0()) -> c_16():20
-->_4 activate#(X) -> c_2():6
-->_2 activate#(X) -> c_2():6
-->_3 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)):2
-->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):1
3:S:unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
-->_2 unquote#(01()) -> c_24(0#()):26
-->_1 s#(X) -> c_22():24
-->_2 unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)):3
4:S:unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
-->_3 unquote1#(nil1()) -> c_27(nil#()):27
-->_2 unquote#(01()) -> c_24(0#()):26
-->_1 fcons#(X,Z) -> c_11(cons#(X,Z)):15
-->_3 unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)):4
-->_2 unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)):3
5:W:0#() -> c_1()
6:W:activate#(X) -> c_2()
7:W:activate#(n__0()) -> c_3(0#())
-->_1 0#() -> c_1():5
8:W:activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
-->_1 cons#(X1,X2) -> c_10():14
9:W:activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
-->_1 first#(X1,X2) -> c_12():16
10:W:activate#(n__from(X)) -> c_6(from#(X))
-->_1 from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)):17
-->_1 from#(X) -> c_14():18
11:W:activate#(n__nil()) -> c_7(nil#())
-->_1 nil#() -> c_15():19
12:W:activate#(n__s(X)) -> c_8(s#(X))
-->_1 s#(X) -> c_22():24
13:W:activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
-->_1 sel#(X1,X2) -> c_23():25
14:W:cons#(X1,X2) -> c_10()
15:W:fcons#(X,Z) -> c_11(cons#(X,Z))
-->_1 cons#(X1,X2) -> c_10():14
16:W:first#(X1,X2) -> c_12()
17:W:from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
-->_2 s#(X) -> c_22():24
-->_1 cons#(X1,X2) -> c_10():14
18:W:from#(X) -> c_14()
19:W:nil#() -> c_15()
20:W:quote#(n__0()) -> c_16()
21:W:quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
-->_3 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13
-->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13
-->_3 activate#(n__s(X)) -> c_8(s#(X)):12
-->_2 activate#(n__s(X)) -> c_8(s#(X)):12
-->_3 activate#(n__nil()) -> c_7(nil#()):11
-->_2 activate#(n__nil()) -> c_7(nil#()):11
-->_3 activate#(n__from(X)) -> c_6(from#(X)):10
-->_2 activate#(n__from(X)) -> c_6(from#(X)):10
-->_3 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9
-->_2 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9
-->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8
-->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8
-->_3 activate#(n__0()) -> c_3(0#()):7
-->_2 activate#(n__0()) -> c_3(0#()):7
-->_3 activate#(X) -> c_2():6
-->_2 activate#(X) -> c_2():6
22:W:quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
-->_3 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13
-->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13
-->_3 activate#(n__s(X)) -> c_8(s#(X)):12
-->_2 activate#(n__s(X)) -> c_8(s#(X)):12
-->_3 activate#(n__nil()) -> c_7(nil#()):11
-->_2 activate#(n__nil()) -> c_7(nil#()):11
-->_3 activate#(n__from(X)) -> c_6(from#(X)):10
-->_2 activate#(n__from(X)) -> c_6(from#(X)):10
-->_3 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9
-->_2 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9
-->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8
-->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8
-->_3 activate#(n__0()) -> c_3(0#()):7
-->_2 activate#(n__0()) -> c_3(0#()):7
-->_3 activate#(X) -> c_2():6
-->_2 activate#(X) -> c_2():6
23:W:quote1#(n__nil()) -> c_21()
24:W:s#(X) -> c_22()
25:W:sel#(X1,X2) -> c_23()
26:W:unquote#(01()) -> c_24(0#())
-->_1 0#() -> c_1():5
27:W:unquote1#(nil1()) -> c_27(nil#())
-->_1 nil#() -> c_15():19
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
15: fcons#(X,Z) -> c_11(cons#(X,Z))
27: unquote1#(nil1()) -> c_27(nil#())
26: unquote#(01()) -> c_24(0#())
23: quote1#(n__nil()) -> c_21()
22: quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z))
20: quote#(n__0()) -> c_16()
21: quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z))
6: activate#(X) -> c_2()
7: activate#(n__0()) -> c_3(0#())
5: 0#() -> c_1()
8: activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2))
9: activate#(n__first(X1,X2)) -> c_5(first#(X1,X2))
16: first#(X1,X2) -> c_12()
10: activate#(n__from(X)) -> c_6(from#(X))
18: from#(X) -> c_14()
17: from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X))
14: cons#(X1,X2) -> c_10()
11: activate#(n__nil()) -> c_7(nil#())
19: nil#() -> c_15()
12: activate#(n__s(X)) -> c_8(s#(X))
24: s#(X) -> c_22()
13: activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2))
25: sel#(X1,X2) -> c_23()
* Step 9: SimplifyRHS MAYBE
+ Considered Problem:
- Strict DPs:
quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
fcons(X,Z) -> cons(X,Z)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
unquote(01()) -> 0()
unquote(s1(X)) -> s(unquote(X))
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
unquote1(nil1()) -> nil()
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X))
-->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):1
2:S:quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z))
-->_3 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)):2
-->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):1
3:S:unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X))
-->_2 unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)):3
4:S:unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z))
-->_3 unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)):4
-->_2 unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
quote#(n__s(X)) -> c_17(quote#(activate(X)))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
* Step 10: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
quote#(n__s(X)) -> c_17(quote#(activate(X)))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
fcons(X,Z) -> cons(X,Z)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
unquote(01()) -> 0()
unquote(s1(X)) -> s(unquote(X))
unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z))
unquote1(nil1()) -> nil()
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/2,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
quote#(n__s(X)) -> c_17(quote#(activate(X)))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
* Step 11: Decompose MAYBE
+ Considered Problem:
- Strict DPs:
quote#(n__s(X)) -> c_17(quote#(activate(X)))
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/2,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
+ Details:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
- Strict DPs:
quote#(n__s(X)) -> c_17(quote#(activate(X)))
- Weak DPs:
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/2,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
Problem (S)
- Strict DPs:
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak DPs:
quote#(n__s(X)) -> c_17(quote#(activate(X)))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/2,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
** Step 11.a:1: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
quote#(n__s(X)) -> c_17(quote#(activate(X)))
- Weak DPs:
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/2,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:quote#(n__s(X)) -> c_17(quote#(activate(X)))
-->_1 quote#(n__s(X)) -> c_17(quote#(activate(X))):1
2:W:quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
-->_1 quote#(n__s(X)) -> c_17(quote#(activate(X))):1
-->_2 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))):2
3:W:unquote#(s1(X)) -> c_25(unquote#(X))
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):3
4:W:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):3
-->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):4
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
4: unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
3: unquote#(s1(X)) -> c_25(unquote#(X))
** Step 11.a:2: Failure MAYBE
+ Considered Problem:
- Strict DPs:
quote#(n__s(X)) -> c_17(quote#(activate(X)))
- Weak DPs:
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/2,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
** Step 11.b:1: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak DPs:
quote#(n__s(X)) -> c_17(quote#(activate(X)))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/2,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
-->_1 quote#(n__s(X)) -> c_17(quote#(activate(X))):4
-->_2 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))):1
2:S:unquote#(s1(X)) -> c_25(unquote#(X))
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2
3:S:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
-->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):3
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2
4:W:quote#(n__s(X)) -> c_17(quote#(activate(X)))
-->_1 quote#(n__s(X)) -> c_17(quote#(activate(X))):4
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
4: quote#(n__s(X)) -> c_17(quote#(activate(X)))
** Step 11.b:2: SimplifyRHS MAYBE
+ Considered Problem:
- Strict DPs:
quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/2,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z)))
-->_2 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))):1
2:S:unquote#(s1(X)) -> c_25(unquote#(X))
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2
3:S:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
-->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):3
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z)))
** Step 11.b:3: Decompose MAYBE
+ Considered Problem:
- Strict DPs:
quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z)))
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
+ Details:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
- Strict DPs:
quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z)))
- Weak DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
Problem (S)
- Strict DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak DPs:
quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z)))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
*** Step 11.b:3.a:1: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z)))
- Weak DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z)))
-->_1 quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z))):1
2:W:unquote#(s1(X)) -> c_25(unquote#(X))
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2
3:W:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2
-->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):3
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
2: unquote#(s1(X)) -> c_25(unquote#(X))
*** Step 11.b:3.a:2: Failure MAYBE
+ Considered Problem:
- Strict DPs:
quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z)))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
*** Step 11.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak DPs:
quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z)))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:unquote#(s1(X)) -> c_25(unquote#(X))
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):1
2:S:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
-->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):2
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):1
3:W:quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z)))
-->_1 quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z))):3
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z)))
*** Step 11.b:3.b:2: Decompose WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
+ Details:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
- Strict DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
- Weak DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
Problem (S)
- Strict DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
**** Step 11.b:3.b:2.a:1: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
- Weak DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
**** Step 11.b:3.b:2.a:2: PredecessorEstimationCP WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
- Weak DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: unquote#(s1(X)) -> c_25(unquote#(X))
The strictly oriented rules are moved into the weak component.
***** Step 11.b:3.b:2.a:2.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
- Weak DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_25) = {1},
uargs(c_26) = {1,2}
Following symbols are considered usable:
{0#,activate#,cons#,fcons#,first#,first1#,from#,nil#,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#}
TcT has computed the following interpretation:
p(0) = [0]
p(01) = [0]
p(activate) = [0]
p(cons) = [0]
p(cons1) = [1] x1 + [1] x2 + [3]
p(fcons) = [0]
p(first) = [0]
p(first1) = [0]
p(from) = [0]
p(n__0) = [0]
p(n__cons) = [1] x1 + [1] x2 + [0]
p(n__first) = [1] x1 + [1] x2 + [0]
p(n__from) = [1] x1 + [0]
p(n__nil) = [0]
p(n__s) = [0]
p(n__sel) = [1] x1 + [1]
p(nil) = [0]
p(nil1) = [1]
p(quote) = [1]
p(quote1) = [1] x1 + [8]
p(s) = [1]
p(s1) = [1] x1 + [2]
p(sel) = [2] x1 + [2] x2 + [0]
p(sel1) = [0]
p(unquote) = [8]
p(unquote1) = [8] x1 + [1]
p(0#) = [0]
p(activate#) = [1] x1 + [8]
p(cons#) = [0]
p(fcons#) = [2]
p(first#) = [0]
p(first1#) = [1] x1 + [1] x2 + [0]
p(from#) = [0]
p(nil#) = [2]
p(quote#) = [1] x1 + [1]
p(quote1#) = [8] x1 + [0]
p(s#) = [1] x1 + [1]
p(sel#) = [1] x1 + [1]
p(sel1#) = [2]
p(unquote#) = [2] x1 + [2]
p(unquote1#) = [8] x1 + [0]
p(c_1) = [0]
p(c_2) = [1]
p(c_3) = [8] x1 + [1]
p(c_4) = [1] x1 + [1]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x1 + [0]
p(c_7) = [1] x1 + [0]
p(c_8) = [1] x1 + [0]
p(c_9) = [0]
p(c_10) = [2]
p(c_11) = [0]
p(c_12) = [0]
p(c_13) = [4] x1 + [1] x2 + [1]
p(c_14) = [1]
p(c_15) = [2]
p(c_16) = [0]
p(c_17) = [1]
p(c_18) = [1] x3 + [1]
p(c_19) = [0]
p(c_20) = [4] x1 + [4] x2 + [1] x3 + [0]
p(c_21) = [1]
p(c_22) = [0]
p(c_23) = [4]
p(c_24) = [0]
p(c_25) = [1] x1 + [2]
p(c_26) = [4] x1 + [1] x2 + [11]
p(c_27) = [1] x1 + [0]
Following rules are strictly oriented:
unquote#(s1(X)) = [2] X + [6]
> [2] X + [4]
= c_25(unquote#(X))
Following rules are (at-least) weakly oriented:
unquote1#(cons1(X,Z)) = [8] X + [8] Z + [24]
>= [8] X + [8] Z + [19]
= c_26(unquote#(X),unquote1#(Z))
***** Step 11.b:3.b:2.a:2.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
***** Step 11.b:3.b:2.a:2.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:unquote#(s1(X)) -> c_25(unquote#(X))
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):1
2:W:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
-->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):2
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
2: unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
1: unquote#(s1(X)) -> c_25(unquote#(X))
***** Step 11.b:3.b:2.a:2.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
**** Step 11.b:3.b:2.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak DPs:
unquote#(s1(X)) -> c_25(unquote#(X))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2
-->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):1
2:W:unquote#(s1(X)) -> c_25(unquote#(X))
-->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
2: unquote#(s1(X)) -> c_25(unquote#(X))
**** Step 11.b:3.b:2.b:2: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z))
-->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z))
**** Step 11.b:3.b:2.b:3: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__cons(X1,X2)) -> cons(X1,X2)
activate(n__first(X1,X2)) -> first(X1,X2)
activate(n__from(X)) -> from(X)
activate(n__nil()) -> nil()
activate(n__s(X)) -> s(X)
activate(n__sel(X1,X2)) -> sel(X1,X2)
cons(X1,X2) -> n__cons(X1,X2)
first(X1,X2) -> n__first(X1,X2)
from(X) -> cons(X,n__from(s(X)))
from(X) -> n__from(X)
nil() -> n__nil()
s(X) -> n__s(X)
sel(X1,X2) -> n__sel(X1,X2)
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z))
**** Step 11.b:3.b:2.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z))
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z))
The strictly oriented rules are moved into the weak component.
***** Step 11.b:3.b:2.b:4.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z))
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_26) = {1}
Following symbols are considered usable:
{0#,activate#,cons#,fcons#,first#,first1#,from#,nil#,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#}
TcT has computed the following interpretation:
p(0) = [0]
p(01) = [0]
p(activate) = [0]
p(cons) = [0]
p(cons1) = [1] x2 + [8]
p(fcons) = [0]
p(first) = [0]
p(first1) = [0]
p(from) = [0]
p(n__0) = [1]
p(n__cons) = [1] x1 + [1] x2 + [1]
p(n__first) = [1]
p(n__from) = [1] x1 + [1]
p(n__nil) = [2]
p(n__s) = [0]
p(n__sel) = [2]
p(nil) = [1]
p(nil1) = [0]
p(quote) = [1] x1 + [2]
p(quote1) = [1]
p(s) = [1]
p(s1) = [1] x1 + [2]
p(sel) = [1]
p(sel1) = [0]
p(unquote) = [0]
p(unquote1) = [0]
p(0#) = [0]
p(activate#) = [0]
p(cons#) = [0]
p(fcons#) = [0]
p(first#) = [0]
p(first1#) = [0]
p(from#) = [0]
p(nil#) = [0]
p(quote#) = [0]
p(quote1#) = [0]
p(s#) = [0]
p(sel#) = [0]
p(sel1#) = [0]
p(unquote#) = [0]
p(unquote1#) = [1] x1 + [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [8] x1 + [0]
p(c_4) = [2] x1 + [0]
p(c_5) = [0]
p(c_6) = [0]
p(c_7) = [2] x1 + [0]
p(c_8) = [1] x1 + [4]
p(c_9) = [0]
p(c_10) = [2]
p(c_11) = [8]
p(c_12) = [1]
p(c_13) = [4]
p(c_14) = [2]
p(c_15) = [0]
p(c_16) = [0]
p(c_17) = [2] x1 + [1]
p(c_18) = [2] x1 + [1] x2 + [1]
p(c_19) = [2] x1 + [1]
p(c_20) = [1] x1 + [1] x2 + [1] x3 + [1]
p(c_21) = [0]
p(c_22) = [1]
p(c_23) = [1]
p(c_24) = [1]
p(c_25) = [2] x1 + [1]
p(c_26) = [1] x1 + [4]
p(c_27) = [1] x1 + [0]
Following rules are strictly oriented:
unquote1#(cons1(X,Z)) = [1] Z + [8]
> [1] Z + [4]
= c_26(unquote1#(Z))
Following rules are (at-least) weakly oriented:
***** Step 11.b:3.b:2.b:4.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z))
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
***** Step 11.b:3.b:2.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z))
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z))
-->_1 unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z))
***** Step 11.b:3.b:2.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Signature:
{0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1
,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1
,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0
,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0
,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,c_27/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#
,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from
,n__nil,n__s,n__sel,nil1,s1}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
MAYBE