WORST_CASE(Omega(n^1),O(n^3))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^3))
+ Considered Problem:
- Strict TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
less_leaves(x,leaf()) -> false()
less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
less_leaves(leaf(),cons(w,z)) -> true()
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
quot(0(),s(y)) -> 0()
quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
shuffle(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0
,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,concat,less_leaves,minus,quot,reverse
,shuffle} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
less_leaves(x,leaf()) -> false()
less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
less_leaves(leaf(),cons(w,z)) -> true()
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
quot(0(),s(y)) -> 0()
quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
shuffle(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0
,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,concat,less_leaves,minus,quot,reverse
,shuffle} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
app(y,z){y -> add(x,y)} =
app(add(x,y),z) ->^+ add(x,app(y,z))
= C[app(y,z) = app(y,z){}]
** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
less_leaves(x,leaf()) -> false()
less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
less_leaves(leaf(),cons(w,z)) -> true()
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
quot(0(),s(y)) -> 0()
quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
shuffle(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0
,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,concat,less_leaves,minus,quot,reverse
,shuffle} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
app#(add(n,x),y) -> c_1(app#(x,y))
app#(nil(),y) -> c_2()
concat#(cons(u,v),y) -> c_3(concat#(v,y))
concat#(leaf(),y) -> c_4()
less_leaves#(x,leaf()) -> c_5()
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)),concat#(u,v),concat#(w,z))
less_leaves#(leaf(),cons(w,z)) -> c_7()
minus#(x,0()) -> c_8()
minus#(s(x),s(y)) -> c_9(minus#(x,y))
quot#(0(),s(y)) -> c_10()
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y))
reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
reverse#(nil()) -> c_13()
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x))
shuffle#(nil()) -> c_15()
Weak DPs
and mark the set of starting terms.
** Step 1.b:2: PredecessorEstimation WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
app#(add(n,x),y) -> c_1(app#(x,y))
app#(nil(),y) -> c_2()
concat#(cons(u,v),y) -> c_3(concat#(v,y))
concat#(leaf(),y) -> c_4()
less_leaves#(x,leaf()) -> c_5()
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)),concat#(u,v),concat#(w,z))
less_leaves#(leaf(),cons(w,z)) -> c_7()
minus#(x,0()) -> c_8()
minus#(s(x),s(y)) -> c_9(minus#(x,y))
quot#(0(),s(y)) -> c_10()
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y))
reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
reverse#(nil()) -> c_13()
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x))
shuffle#(nil()) -> c_15()
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
less_leaves(x,leaf()) -> false()
less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
less_leaves(leaf(),cons(w,z)) -> true()
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
quot(0(),s(y)) -> 0()
quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
shuffle(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2,4,5,7,8,10,13,15}
by application of
Pre({2,4,5,7,8,10,13,15}) = {1,3,6,9,11,12,14}.
Here rules are labelled as follows:
1: app#(add(n,x),y) -> c_1(app#(x,y))
2: app#(nil(),y) -> c_2()
3: concat#(cons(u,v),y) -> c_3(concat#(v,y))
4: concat#(leaf(),y) -> c_4()
5: less_leaves#(x,leaf()) -> c_5()
6: less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)),concat#(u,v),concat#(w,z))
7: less_leaves#(leaf(),cons(w,z)) -> c_7()
8: minus#(x,0()) -> c_8()
9: minus#(s(x),s(y)) -> c_9(minus#(x,y))
10: quot#(0(),s(y)) -> c_10()
11: quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y))
12: reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
13: reverse#(nil()) -> c_13()
14: shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x))
15: shuffle#(nil()) -> c_15()
** Step 1.b:3: RemoveWeakSuffixes WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
app#(add(n,x),y) -> c_1(app#(x,y))
concat#(cons(u,v),y) -> c_3(concat#(v,y))
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)),concat#(u,v),concat#(w,z))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y))
reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x))
- Weak DPs:
app#(nil(),y) -> c_2()
concat#(leaf(),y) -> c_4()
less_leaves#(x,leaf()) -> c_5()
less_leaves#(leaf(),cons(w,z)) -> c_7()
minus#(x,0()) -> c_8()
quot#(0(),s(y)) -> c_10()
reverse#(nil()) -> c_13()
shuffle#(nil()) -> c_15()
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
less_leaves(x,leaf()) -> false()
less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
less_leaves(leaf(),cons(w,z)) -> true()
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
quot(0(),s(y)) -> 0()
quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
shuffle(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:app#(add(n,x),y) -> c_1(app#(x,y))
-->_1 app#(nil(),y) -> c_2():8
-->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1
2:S:concat#(cons(u,v),y) -> c_3(concat#(v,y))
-->_1 concat#(leaf(),y) -> c_4():9
-->_1 concat#(cons(u,v),y) -> c_3(concat#(v,y)):2
3:S:less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z))
,concat#(u,v)
,concat#(w,z))
-->_1 less_leaves#(leaf(),cons(w,z)) -> c_7():11
-->_1 less_leaves#(x,leaf()) -> c_5():10
-->_3 concat#(leaf(),y) -> c_4():9
-->_2 concat#(leaf(),y) -> c_4():9
-->_1 less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z))
,concat#(u,v)
,concat#(w,z)):3
-->_3 concat#(cons(u,v),y) -> c_3(concat#(v,y)):2
-->_2 concat#(cons(u,v),y) -> c_3(concat#(v,y)):2
4:S:minus#(s(x),s(y)) -> c_9(minus#(x,y))
-->_1 minus#(x,0()) -> c_8():12
-->_1 minus#(s(x),s(y)) -> c_9(minus#(x,y)):4
5:S:quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y))
-->_1 quot#(0(),s(y)) -> c_10():13
-->_2 minus#(x,0()) -> c_8():12
-->_1 quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y)):5
-->_2 minus#(s(x),s(y)) -> c_9(minus#(x,y)):4
6:S:reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
-->_2 reverse#(nil()) -> c_13():14
-->_1 app#(nil(),y) -> c_2():8
-->_2 reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x)):6
-->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1
7:S:shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x))
-->_1 shuffle#(nil()) -> c_15():15
-->_2 reverse#(nil()) -> c_13():14
-->_1 shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x)):7
-->_2 reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x)):6
8:W:app#(nil(),y) -> c_2()
9:W:concat#(leaf(),y) -> c_4()
10:W:less_leaves#(x,leaf()) -> c_5()
11:W:less_leaves#(leaf(),cons(w,z)) -> c_7()
12:W:minus#(x,0()) -> c_8()
13:W:quot#(0(),s(y)) -> c_10()
14:W:reverse#(nil()) -> c_13()
15:W:shuffle#(nil()) -> c_15()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
15: shuffle#(nil()) -> c_15()
14: reverse#(nil()) -> c_13()
13: quot#(0(),s(y)) -> c_10()
12: minus#(x,0()) -> c_8()
10: less_leaves#(x,leaf()) -> c_5()
11: less_leaves#(leaf(),cons(w,z)) -> c_7()
9: concat#(leaf(),y) -> c_4()
8: app#(nil(),y) -> c_2()
** Step 1.b:4: UsableRules WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
app#(add(n,x),y) -> c_1(app#(x,y))
concat#(cons(u,v),y) -> c_3(concat#(v,y))
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)),concat#(u,v),concat#(w,z))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y))
reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
less_leaves(x,leaf()) -> false()
less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
less_leaves(leaf(),cons(w,z)) -> true()
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
quot(0(),s(y)) -> 0()
quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
shuffle(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
app#(add(n,x),y) -> c_1(app#(x,y))
concat#(cons(u,v),y) -> c_3(concat#(v,y))
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)),concat#(u,v),concat#(w,z))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y))
reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x))
** Step 1.b:5: DecomposeDG WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
app#(add(n,x),y) -> c_1(app#(x,y))
concat#(cons(u,v),y) -> c_3(concat#(v,y))
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)),concat#(u,v),concat#(w,z))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y))
reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
+ Details:
We decompose the input problem according to the dependency graph into the upper component
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)),concat#(u,v),concat#(w,z))
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y))
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x))
and a lower component
app#(add(n,x),y) -> c_1(app#(x,y))
concat#(cons(u,v),y) -> c_3(concat#(v,y))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
Further, following extension rules are added to the lower component.
less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
quot#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
*** Step 1.b:5.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)),concat#(u,v),concat#(w,z))
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y))
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z))
,concat#(u,v)
,concat#(w,z))
-->_1 less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z))
,concat#(u,v)
,concat#(w,z)):1
2:S:quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y))
-->_1 quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)),minus#(x,y)):2
3:S:shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x))
-->_1 shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)),reverse#(x)):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)))
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)))
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)))
*** Step 1.b:5.a:2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)))
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)))
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0,c_11/1,c_12/2,c_13/0,c_14/1,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, 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:
The following argument positions are considered usable:
uargs(add) = {2},
uargs(app) = {1},
uargs(cons) = {2},
uargs(less_leaves#) = {1,2},
uargs(quot#) = {1},
uargs(shuffle#) = {1},
uargs(c_6) = {1},
uargs(c_11) = {1},
uargs(c_14) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(add) = [1] x2 + [0]
p(app) = [1] x1 + [1] x2 + [0]
p(concat) = [1] x1 + [1] x2 + [0]
p(cons) = [1] x1 + [1] x2 + [1]
p(false) = [0]
p(leaf) = [0]
p(less_leaves) = [2] x2 + [1]
p(minus) = [1] x1 + [0]
p(nil) = [0]
p(quot) = [1] x1 + [2]
p(reverse) = [0]
p(s) = [1] x1 + [0]
p(shuffle) = [1] x1 + [0]
p(true) = [1]
p(app#) = [1] x1 + [0]
p(concat#) = [1] x1 + [2] x2 + [0]
p(less_leaves#) = [1] x1 + [1] x2 + [0]
p(minus#) = [2] x1 + [1] x2 + [1]
p(quot#) = [1] x1 + [0]
p(reverse#) = [4] x1 + [4]
p(shuffle#) = [1] x1 + [0]
p(c_1) = [1]
p(c_2) = [0]
p(c_3) = [1] x1 + [4]
p(c_4) = [0]
p(c_5) = [4]
p(c_6) = [1] x1 + [0]
p(c_7) = [1]
p(c_8) = [0]
p(c_9) = [1] x1 + [2]
p(c_10) = [0]
p(c_11) = [1] x1 + [3]
p(c_12) = [4] x1 + [4]
p(c_13) = [1]
p(c_14) = [1] x1 + [0]
p(c_15) = [0]
Following rules are strictly oriented:
less_leaves#(cons(u,v),cons(w,z)) = [1] u + [1] v + [1] w + [1] z + [2]
> [1] u + [1] v + [1] w + [1] z + [0]
= c_6(less_leaves#(concat(u,v),concat(w,z)))
Following rules are (at-least) weakly oriented:
quot#(s(x),s(y)) = [1] x + [0]
>= [1] x + [3]
= c_11(quot#(minus(x,y),s(y)))
shuffle#(add(n,x)) = [1] x + [0]
>= [0]
= c_14(shuffle#(reverse(x)))
app(add(n,x),y) = [1] x + [1] y + [0]
>= [1] x + [1] y + [0]
= add(n,app(x,y))
app(nil(),y) = [1] y + [0]
>= [1] y + [0]
= y
concat(cons(u,v),y) = [1] u + [1] v + [1] y + [1]
>= [1] u + [1] v + [1] y + [1]
= cons(u,concat(v,y))
concat(leaf(),y) = [1] y + [0]
>= [1] y + [0]
= y
minus(x,0()) = [1] x + [0]
>= [1] x + [0]
= x
minus(s(x),s(y)) = [1] x + [0]
>= [1] x + [0]
= minus(x,y)
reverse(add(n,x)) = [0]
>= [0]
= app(reverse(x),add(n,nil()))
reverse(nil()) = [0]
>= [0]
= nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 1.b:5.a:3: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)))
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)))
- Weak DPs:
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0,c_11/1,c_12/2,c_13/0,c_14/1,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, 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:
The following argument positions are considered usable:
uargs(add) = {2},
uargs(app) = {1},
uargs(cons) = {2},
uargs(less_leaves#) = {1,2},
uargs(quot#) = {1},
uargs(shuffle#) = {1},
uargs(c_6) = {1},
uargs(c_11) = {1},
uargs(c_14) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(add) = [1] x2 + [0]
p(app) = [1] x1 + [1] x2 + [0]
p(concat) = [1] x2 + [0]
p(cons) = [1] x2 + [0]
p(false) = [0]
p(leaf) = [0]
p(less_leaves) = [4] x1 + [0]
p(minus) = [1] x1 + [0]
p(nil) = [0]
p(quot) = [1]
p(reverse) = [0]
p(s) = [1] x1 + [1]
p(shuffle) = [1]
p(true) = [1]
p(app#) = [4] x2 + [1]
p(concat#) = [2] x1 + [1] x2 + [1]
p(less_leaves#) = [1] x1 + [1] x2 + [1]
p(minus#) = [1]
p(quot#) = [1] x1 + [4] x2 + [3]
p(reverse#) = [1]
p(shuffle#) = [1] x1 + [0]
p(c_1) = [1]
p(c_2) = [1]
p(c_3) = [4]
p(c_4) = [1]
p(c_5) = [0]
p(c_6) = [1] x1 + [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [2] x1 + [0]
p(c_10) = [0]
p(c_11) = [1] x1 + [0]
p(c_12) = [4] x2 + [4]
p(c_13) = [0]
p(c_14) = [1] x1 + [4]
p(c_15) = [0]
Following rules are strictly oriented:
quot#(s(x),s(y)) = [1] x + [4] y + [8]
> [1] x + [4] y + [7]
= c_11(quot#(minus(x,y),s(y)))
Following rules are (at-least) weakly oriented:
less_leaves#(cons(u,v),cons(w,z)) = [1] v + [1] z + [1]
>= [1] v + [1] z + [1]
= c_6(less_leaves#(concat(u,v),concat(w,z)))
shuffle#(add(n,x)) = [1] x + [0]
>= [4]
= c_14(shuffle#(reverse(x)))
app(add(n,x),y) = [1] x + [1] y + [0]
>= [1] x + [1] y + [0]
= add(n,app(x,y))
app(nil(),y) = [1] y + [0]
>= [1] y + [0]
= y
concat(cons(u,v),y) = [1] y + [0]
>= [1] y + [0]
= cons(u,concat(v,y))
concat(leaf(),y) = [1] y + [0]
>= [1] y + [0]
= y
minus(x,0()) = [1] x + [0]
>= [1] x + [0]
= x
minus(s(x),s(y)) = [1] x + [1]
>= [1] x + [0]
= minus(x,y)
reverse(add(n,x)) = [0]
>= [0]
= app(reverse(x),add(n,nil()))
reverse(nil()) = [0]
>= [0]
= nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 1.b:5.a:4: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)))
- Weak DPs:
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)))
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0,c_11/1,c_12/2,c_13/0,c_14/1,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, 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:
The following argument positions are considered usable:
uargs(add) = {2},
uargs(app) = {1},
uargs(cons) = {2},
uargs(less_leaves#) = {1,2},
uargs(quot#) = {1},
uargs(shuffle#) = {1},
uargs(c_6) = {1},
uargs(c_11) = {1},
uargs(c_14) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(add) = [1] x2 + [1]
p(app) = [1] x1 + [1] x2 + [0]
p(concat) = [1] x1 + [1] x2 + [0]
p(cons) = [1] x1 + [1] x2 + [0]
p(false) = [0]
p(leaf) = [0]
p(less_leaves) = [0]
p(minus) = [1] x1 + [0]
p(nil) = [0]
p(quot) = [0]
p(reverse) = [1] x1 + [0]
p(s) = [1] x1 + [4]
p(shuffle) = [1]
p(true) = [0]
p(app#) = [0]
p(concat#) = [0]
p(less_leaves#) = [1] x1 + [1] x2 + [0]
p(minus#) = [0]
p(quot#) = [1] x1 + [7]
p(reverse#) = [0]
p(shuffle#) = [1] x1 + [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [1] x1 + [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [0]
p(c_10) = [0]
p(c_11) = [1] x1 + [4]
p(c_12) = [0]
p(c_13) = [0]
p(c_14) = [1] x1 + [0]
p(c_15) = [0]
Following rules are strictly oriented:
shuffle#(add(n,x)) = [1] x + [1]
> [1] x + [0]
= c_14(shuffle#(reverse(x)))
Following rules are (at-least) weakly oriented:
less_leaves#(cons(u,v),cons(w,z)) = [1] u + [1] v + [1] w + [1] z + [0]
>= [1] u + [1] v + [1] w + [1] z + [0]
= c_6(less_leaves#(concat(u,v),concat(w,z)))
quot#(s(x),s(y)) = [1] x + [11]
>= [1] x + [11]
= c_11(quot#(minus(x,y),s(y)))
app(add(n,x),y) = [1] x + [1] y + [1]
>= [1] x + [1] y + [1]
= add(n,app(x,y))
app(nil(),y) = [1] y + [0]
>= [1] y + [0]
= y
concat(cons(u,v),y) = [1] u + [1] v + [1] y + [0]
>= [1] u + [1] v + [1] y + [0]
= cons(u,concat(v,y))
concat(leaf(),y) = [1] y + [0]
>= [1] y + [0]
= y
minus(x,0()) = [1] x + [0]
>= [1] x + [0]
= x
minus(s(x),s(y)) = [1] x + [4]
>= [1] x + [0]
= minus(x,y)
reverse(add(n,x)) = [1] x + [1]
>= [1] x + [1]
= app(reverse(x),add(n,nil()))
reverse(nil()) = [0]
>= [0]
= nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** Step 1.b:5.a:5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
less_leaves#(cons(u,v),cons(w,z)) -> c_6(less_leaves#(concat(u,v),concat(w,z)))
quot#(s(x),s(y)) -> c_11(quot#(minus(x,y),s(y)))
shuffle#(add(n,x)) -> c_14(shuffle#(reverse(x)))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0,c_11/1,c_12/2,c_13/0,c_14/1,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
*** Step 1.b:5.b:1: DecomposeDG WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
app#(add(n,x),y) -> c_1(app#(x,y))
concat#(cons(u,v),y) -> c_3(concat#(v,y))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
- Weak DPs:
less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
quot#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
+ Details:
We decompose the input problem according to the dependency graph into the upper component
concat#(cons(u,v),y) -> c_3(concat#(v,y))
less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
quot#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
and a lower component
app#(add(n,x),y) -> c_1(app#(x,y))
Further, following extension rules are added to the lower component.
concat#(cons(u,v),y) -> concat#(v,y)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
minus#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
reverse#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
**** Step 1.b:5.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
concat#(cons(u,v),y) -> c_3(concat#(v,y))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
- Weak DPs:
less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
quot#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:concat#(cons(u,v),y) -> c_3(concat#(v,y))
-->_1 concat#(cons(u,v),y) -> c_3(concat#(v,y)):1
2:S:minus#(s(x),s(y)) -> c_9(minus#(x,y))
-->_1 minus#(s(x),s(y)) -> c_9(minus#(x,y)):2
3:S:reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x))
-->_2 reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x)):3
4:W:less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
-->_1 concat#(cons(u,v),y) -> c_3(concat#(v,y)):1
5:W:less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
-->_1 concat#(cons(u,v),y) -> c_3(concat#(v,y)):1
6:W:less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
-->_1 less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z)):6
-->_1 less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z):5
-->_1 less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v):4
7:W:quot#(s(x),s(y)) -> minus#(x,y)
-->_1 minus#(s(x),s(y)) -> c_9(minus#(x,y)):2
8:W:quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
-->_1 quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)):8
-->_1 quot#(s(x),s(y)) -> minus#(x,y):7
9:W:shuffle#(add(n,x)) -> reverse#(x)
-->_1 reverse#(add(n,x)) -> c_12(app#(reverse(x),add(n,nil())),reverse#(x)):3
10:W:shuffle#(add(n,x)) -> shuffle#(reverse(x))
-->_1 shuffle#(add(n,x)) -> shuffle#(reverse(x)):10
-->_1 shuffle#(add(n,x)) -> reverse#(x):9
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
reverse#(add(n,x)) -> c_12(reverse#(x))
**** Step 1.b:5.b:1.a:2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
concat#(cons(u,v),y) -> c_3(concat#(v,y))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
reverse#(add(n,x)) -> c_12(reverse#(x))
- Weak DPs:
less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
quot#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, 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:
The following argument positions are considered usable:
uargs(add) = {2},
uargs(app) = {1},
uargs(cons) = {2},
uargs(less_leaves#) = {1,2},
uargs(quot#) = {1},
uargs(shuffle#) = {1},
uargs(c_3) = {1},
uargs(c_9) = {1},
uargs(c_12) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(add) = [1] x2 + [4]
p(app) = [1] x1 + [1] x2 + [0]
p(concat) = [1] x1 + [1] x2 + [0]
p(cons) = [1] x1 + [1] x2 + [4]
p(false) = [0]
p(leaf) = [1]
p(less_leaves) = [4] x2 + [1]
p(minus) = [1] x1 + [0]
p(nil) = [0]
p(quot) = [1] x1 + [4] x2 + [1]
p(reverse) = [1] x1 + [0]
p(s) = [1] x1 + [0]
p(shuffle) = [1] x1 + [0]
p(true) = [1]
p(app#) = [0]
p(concat#) = [0]
p(less_leaves#) = [1] x1 + [1] x2 + [0]
p(minus#) = [0]
p(quot#) = [1] x1 + [0]
p(reverse#) = [1] x1 + [3]
p(shuffle#) = [1] x1 + [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [1] x1 + [5]
p(c_4) = [0]
p(c_5) = [1]
p(c_6) = [1] x1 + [4]
p(c_7) = [1]
p(c_8) = [0]
p(c_9) = [1] x1 + [1]
p(c_10) = [0]
p(c_11) = [1] x1 + [1]
p(c_12) = [1] x1 + [3]
p(c_13) = [1]
p(c_14) = [4] x1 + [2] x2 + [0]
p(c_15) = [1]
Following rules are strictly oriented:
reverse#(add(n,x)) = [1] x + [7]
> [1] x + [6]
= c_12(reverse#(x))
Following rules are (at-least) weakly oriented:
concat#(cons(u,v),y) = [0]
>= [5]
= c_3(concat#(v,y))
less_leaves#(cons(u,v),cons(w,z)) = [1] u + [1] v + [1] w + [1] z + [8]
>= [0]
= concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) = [1] u + [1] v + [1] w + [1] z + [8]
>= [0]
= concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) = [1] u + [1] v + [1] w + [1] z + [8]
>= [1] u + [1] v + [1] w + [1] z + [0]
= less_leaves#(concat(u,v),concat(w,z))
minus#(s(x),s(y)) = [0]
>= [1]
= c_9(minus#(x,y))
quot#(s(x),s(y)) = [1] x + [0]
>= [0]
= minus#(x,y)
quot#(s(x),s(y)) = [1] x + [0]
>= [1] x + [0]
= quot#(minus(x,y),s(y))
shuffle#(add(n,x)) = [1] x + [4]
>= [1] x + [3]
= reverse#(x)
shuffle#(add(n,x)) = [1] x + [4]
>= [1] x + [0]
= shuffle#(reverse(x))
app(add(n,x),y) = [1] x + [1] y + [4]
>= [1] x + [1] y + [4]
= add(n,app(x,y))
app(nil(),y) = [1] y + [0]
>= [1] y + [0]
= y
concat(cons(u,v),y) = [1] u + [1] v + [1] y + [4]
>= [1] u + [1] v + [1] y + [4]
= cons(u,concat(v,y))
concat(leaf(),y) = [1] y + [1]
>= [1] y + [0]
= y
minus(x,0()) = [1] x + [0]
>= [1] x + [0]
= x
minus(s(x),s(y)) = [1] x + [0]
>= [1] x + [0]
= minus(x,y)
reverse(add(n,x)) = [1] x + [4]
>= [1] x + [4]
= app(reverse(x),add(n,nil()))
reverse(nil()) = [0]
>= [0]
= nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
**** Step 1.b:5.b:1.a:3: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
concat#(cons(u,v),y) -> c_3(concat#(v,y))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
- Weak DPs:
less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
quot#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
reverse#(add(n,x)) -> c_12(reverse#(x))
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, 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:
The following argument positions are considered usable:
uargs(add) = {2},
uargs(app) = {1},
uargs(cons) = {2},
uargs(less_leaves#) = {1,2},
uargs(quot#) = {1},
uargs(shuffle#) = {1},
uargs(c_3) = {1},
uargs(c_9) = {1},
uargs(c_12) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(add) = [1] x2 + [0]
p(app) = [1] x1 + [4] x2 + [0]
p(concat) = [1] x1 + [1] x2 + [0]
p(cons) = [1] x1 + [1] x2 + [0]
p(false) = [0]
p(leaf) = [0]
p(less_leaves) = [0]
p(minus) = [1] x1 + [0]
p(nil) = [0]
p(quot) = [0]
p(reverse) = [0]
p(s) = [1] x1 + [4]
p(shuffle) = [0]
p(true) = [0]
p(app#) = [0]
p(concat#) = [1] x2 + [0]
p(less_leaves#) = [1] x1 + [1] x2 + [2]
p(minus#) = [1] x2 + [4]
p(quot#) = [1] x1 + [1] x2 + [0]
p(reverse#) = [0]
p(shuffle#) = [1] x1 + [2]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [1] x1 + [0]
p(c_10) = [0]
p(c_11) = [0]
p(c_12) = [1] x1 + [0]
p(c_13) = [4]
p(c_14) = [0]
p(c_15) = [2]
Following rules are strictly oriented:
minus#(s(x),s(y)) = [1] y + [8]
> [1] y + [4]
= c_9(minus#(x,y))
Following rules are (at-least) weakly oriented:
concat#(cons(u,v),y) = [1] y + [0]
>= [1] y + [0]
= c_3(concat#(v,y))
less_leaves#(cons(u,v),cons(w,z)) = [1] u + [1] v + [1] w + [1] z + [2]
>= [1] v + [0]
= concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) = [1] u + [1] v + [1] w + [1] z + [2]
>= [1] z + [0]
= concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) = [1] u + [1] v + [1] w + [1] z + [2]
>= [1] u + [1] v + [1] w + [1] z + [2]
= less_leaves#(concat(u,v),concat(w,z))
quot#(s(x),s(y)) = [1] x + [1] y + [8]
>= [1] y + [4]
= minus#(x,y)
quot#(s(x),s(y)) = [1] x + [1] y + [8]
>= [1] x + [1] y + [4]
= quot#(minus(x,y),s(y))
reverse#(add(n,x)) = [0]
>= [0]
= c_12(reverse#(x))
shuffle#(add(n,x)) = [1] x + [2]
>= [0]
= reverse#(x)
shuffle#(add(n,x)) = [1] x + [2]
>= [2]
= shuffle#(reverse(x))
app(add(n,x),y) = [1] x + [4] y + [0]
>= [1] x + [4] y + [0]
= add(n,app(x,y))
app(nil(),y) = [4] y + [0]
>= [1] y + [0]
= y
concat(cons(u,v),y) = [1] u + [1] v + [1] y + [0]
>= [1] u + [1] v + [1] y + [0]
= cons(u,concat(v,y))
concat(leaf(),y) = [1] y + [0]
>= [1] y + [0]
= y
minus(x,0()) = [1] x + [0]
>= [1] x + [0]
= x
minus(s(x),s(y)) = [1] x + [4]
>= [1] x + [0]
= minus(x,y)
reverse(add(n,x)) = [0]
>= [0]
= app(reverse(x),add(n,nil()))
reverse(nil()) = [0]
>= [0]
= nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
**** Step 1.b:5.b:1.a:4: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
concat#(cons(u,v),y) -> c_3(concat#(v,y))
- Weak DPs:
less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
quot#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
reverse#(add(n,x)) -> c_12(reverse#(x))
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_3) = {1},
uargs(c_9) = {1},
uargs(c_12) = {1}
Following symbols are considered usable:
{concat,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#}
TcT has computed the following interpretation:
p(0) = [0]
p(add) = [1] x1 + [1] x2 + [0]
p(app) = [3] x1 + [0]
p(concat) = [1] x1 + [1] x2 + [0]
p(cons) = [1] x1 + [1] x2 + [1]
p(false) = [0]
p(leaf) = [6]
p(less_leaves) = [0]
p(minus) = [0]
p(nil) = [4]
p(quot) = [0]
p(reverse) = [5]
p(s) = [1] x1 + [0]
p(shuffle) = [0]
p(true) = [0]
p(app#) = [0]
p(concat#) = [1] x1 + [0]
p(less_leaves#) = [6] x1 + [1] x2 + [4]
p(minus#) = [0]
p(quot#) = [3]
p(reverse#) = [0]
p(shuffle#) = [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [4] x1 + [2] x2 + [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [4] x1 + [0]
p(c_10) = [0]
p(c_11) = [1] x1 + [0]
p(c_12) = [1] x1 + [0]
p(c_13) = [0]
p(c_14) = [2] x1 + [2] x2 + [0]
p(c_15) = [0]
Following rules are strictly oriented:
concat#(cons(u,v),y) = [1] u + [1] v + [1]
> [1] v + [0]
= c_3(concat#(v,y))
Following rules are (at-least) weakly oriented:
less_leaves#(cons(u,v),cons(w,z)) = [6] u + [6] v + [1] w + [1] z + [11]
>= [1] u + [0]
= concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) = [6] u + [6] v + [1] w + [1] z + [11]
>= [1] w + [0]
= concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) = [6] u + [6] v + [1] w + [1] z + [11]
>= [6] u + [6] v + [1] w + [1] z + [4]
= less_leaves#(concat(u,v),concat(w,z))
minus#(s(x),s(y)) = [0]
>= [0]
= c_9(minus#(x,y))
quot#(s(x),s(y)) = [3]
>= [0]
= minus#(x,y)
quot#(s(x),s(y)) = [3]
>= [3]
= quot#(minus(x,y),s(y))
reverse#(add(n,x)) = [0]
>= [0]
= c_12(reverse#(x))
shuffle#(add(n,x)) = [0]
>= [0]
= reverse#(x)
shuffle#(add(n,x)) = [0]
>= [0]
= shuffle#(reverse(x))
concat(cons(u,v),y) = [1] u + [1] v + [1] y + [1]
>= [1] u + [1] v + [1] y + [1]
= cons(u,concat(v,y))
concat(leaf(),y) = [1] y + [6]
>= [1] y + [0]
= y
**** Step 1.b:5.b:1.a:5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
concat#(cons(u,v),y) -> c_3(concat#(v,y))
less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
minus#(s(x),s(y)) -> c_9(minus#(x,y))
quot#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
reverse#(add(n,x)) -> c_12(reverse#(x))
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/1,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
**** Step 1.b:5.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
app#(add(n,x),y) -> c_1(app#(x,y))
- Weak DPs:
concat#(cons(u,v),y) -> concat#(v,y)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
minus#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> minus#(x,y)
quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
reverse#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:app#(add(n,x),y) -> c_1(app#(x,y))
-->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1
2:W:concat#(cons(u,v),y) -> concat#(v,y)
-->_1 concat#(cons(u,v),y) -> concat#(v,y):2
3:W:less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
-->_1 concat#(cons(u,v),y) -> concat#(v,y):2
4:W:less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
-->_1 concat#(cons(u,v),y) -> concat#(v,y):2
5:W:less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
-->_1 less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z)):5
-->_1 less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z):4
-->_1 less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v):3
6:W:minus#(s(x),s(y)) -> minus#(x,y)
-->_1 minus#(s(x),s(y)) -> minus#(x,y):6
7:W:quot#(s(x),s(y)) -> minus#(x,y)
-->_1 minus#(s(x),s(y)) -> minus#(x,y):6
8:W:quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
-->_1 quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)):8
-->_1 quot#(s(x),s(y)) -> minus#(x,y):7
9:W:reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
-->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1
10:W:reverse#(add(n,x)) -> reverse#(x)
-->_1 reverse#(add(n,x)) -> reverse#(x):10
-->_1 reverse#(add(n,x)) -> app#(reverse(x),add(n,nil())):9
11:W:shuffle#(add(n,x)) -> reverse#(x)
-->_1 reverse#(add(n,x)) -> reverse#(x):10
-->_1 reverse#(add(n,x)) -> app#(reverse(x),add(n,nil())):9
12:W:shuffle#(add(n,x)) -> shuffle#(reverse(x))
-->_1 shuffle#(add(n,x)) -> shuffle#(reverse(x)):12
-->_1 shuffle#(add(n,x)) -> reverse#(x):11
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
8: quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
7: quot#(s(x),s(y)) -> minus#(x,y)
6: minus#(s(x),s(y)) -> minus#(x,y)
5: less_leaves#(cons(u,v),cons(w,z)) -> less_leaves#(concat(u,v),concat(w,z))
4: less_leaves#(cons(u,v),cons(w,z)) -> concat#(w,z)
3: less_leaves#(cons(u,v),cons(w,z)) -> concat#(u,v)
2: concat#(cons(u,v),y) -> concat#(v,y)
**** Step 1.b:5.b:1.b:2: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
app#(add(n,x),y) -> c_1(app#(x,y))
- Weak DPs:
reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
reverse#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
concat(leaf(),y) -> y
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
app#(add(n,x),y) -> c_1(app#(x,y))
reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
reverse#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
**** Step 1.b:5.b:1.b:3: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
app#(add(n,x),y) -> c_1(app#(x,y))
- Weak DPs:
reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
reverse#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_1) = {1}
Following symbols are considered usable:
{app,reverse,app#,concat#,less_leaves#,minus#,quot#,reverse#,shuffle#}
TcT has computed the following interpretation:
p(0) = [0]
p(add) = [1] x1 + [1] x2 + [1]
p(app) = [1] x1 + [1] x2 + [0]
p(concat) = [0]
p(cons) = [1] x1 + [0]
p(false) = [0]
p(leaf) = [0]
p(less_leaves) = [1] x2 + [0]
p(minus) = [1] x1 + [0]
p(nil) = [0]
p(quot) = [0]
p(reverse) = [1] x1 + [0]
p(s) = [0]
p(shuffle) = [2] x1 + [1]
p(true) = [0]
p(app#) = [8] x1 + [8] x2 + [0]
p(concat#) = [8] x1 + [8] x2 + [0]
p(less_leaves#) = [1] x1 + [1] x2 + [1]
p(minus#) = [1] x2 + [8]
p(quot#) = [1] x1 + [2]
p(reverse#) = [8] x1 + [0]
p(shuffle#) = [11] x1 + [9]
p(c_1) = [1] x1 + [4]
p(c_2) = [1]
p(c_3) = [0]
p(c_4) = [1]
p(c_5) = [0]
p(c_6) = [1] x3 + [8]
p(c_7) = [1]
p(c_8) = [0]
p(c_9) = [1]
p(c_10) = [1]
p(c_11) = [2] x2 + [0]
p(c_12) = [4] x1 + [0]
p(c_13) = [2]
p(c_14) = [0]
p(c_15) = [1]
Following rules are strictly oriented:
app#(add(n,x),y) = [8] n + [8] x + [8] y + [8]
> [8] x + [8] y + [4]
= c_1(app#(x,y))
Following rules are (at-least) weakly oriented:
reverse#(add(n,x)) = [8] n + [8] x + [8]
>= [8] n + [8] x + [8]
= app#(reverse(x),add(n,nil()))
reverse#(add(n,x)) = [8] n + [8] x + [8]
>= [8] x + [0]
= reverse#(x)
shuffle#(add(n,x)) = [11] n + [11] x + [20]
>= [8] x + [0]
= reverse#(x)
shuffle#(add(n,x)) = [11] n + [11] x + [20]
>= [11] x + [9]
= shuffle#(reverse(x))
app(add(n,x),y) = [1] n + [1] x + [1] y + [1]
>= [1] n + [1] x + [1] y + [1]
= add(n,app(x,y))
app(nil(),y) = [1] y + [0]
>= [1] y + [0]
= y
reverse(add(n,x)) = [1] n + [1] x + [1]
>= [1] n + [1] x + [1]
= app(reverse(x),add(n,nil()))
reverse(nil()) = [0]
>= [0]
= nil()
**** Step 1.b:5.b:1.b:4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
app#(add(n,x),y) -> c_1(app#(x,y))
reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
reverse#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> reverse#(x)
shuffle#(add(n,x)) -> shuffle#(reverse(x))
- Weak TRS:
app(add(n,x),y) -> add(n,app(x,y))
app(nil(),y) -> y
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
reverse(nil()) -> nil()
- Signature:
{app/2,concat/2,less_leaves/2,minus/2,quot/2,reverse/1,shuffle/1,app#/2,concat#/2,less_leaves#/2,minus#/2
,quot#/2,reverse#/1,shuffle#/1} / {0/0,add/2,cons/2,false/0,leaf/0,nil/0,s/1,true/0,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/2,c_13/0,c_14/2,c_15/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,concat#,less_leaves#,minus#,quot#,reverse#
,shuffle#} and constructors {0,add,cons,false,leaf,nil,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^3))