WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
append(cons(x,xs),ys) -> cons(x,append(xs,ys))
append(nil(),ys) -> ys
attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
attach(x,nil()) -> nil()
pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
pairs(nil()) -> nil()
- Signature:
{append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
append#(nil(),ys) -> c_2()
attach#(x,cons(y,ys)) -> c_3(attach#(x,ys))
attach#(x,nil()) -> c_4()
pairs#(cons(x,xs)) -> c_5(append#(attach(x,xs),pairs(xs)),attach#(x,xs),pairs#(xs))
pairs#(nil()) -> c_6()
Weak DPs
and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
append#(nil(),ys) -> c_2()
attach#(x,cons(y,ys)) -> c_3(attach#(x,ys))
attach#(x,nil()) -> c_4()
pairs#(cons(x,xs)) -> c_5(append#(attach(x,xs),pairs(xs)),attach#(x,xs),pairs#(xs))
pairs#(nil()) -> c_6()
- Weak TRS:
append(cons(x,xs),ys) -> cons(x,append(xs,ys))
append(nil(),ys) -> ys
attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
attach(x,nil()) -> nil()
pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
pairs(nil()) -> nil()
- Signature:
{append/2,attach/2,pairs/1,append#/2,attach#/2,pairs#/1} / {cons/2,nil/0,pair/2,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/3,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,attach#,pairs#} and constructors {cons,nil,pair}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2,4,6}
by application of
Pre({2,4,6}) = {1,3,5}.
Here rules are labelled as follows:
1: append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
2: append#(nil(),ys) -> c_2()
3: attach#(x,cons(y,ys)) -> c_3(attach#(x,ys))
4: attach#(x,nil()) -> c_4()
5: pairs#(cons(x,xs)) -> c_5(append#(attach(x,xs),pairs(xs)),attach#(x,xs),pairs#(xs))
6: pairs#(nil()) -> c_6()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
attach#(x,cons(y,ys)) -> c_3(attach#(x,ys))
pairs#(cons(x,xs)) -> c_5(append#(attach(x,xs),pairs(xs)),attach#(x,xs),pairs#(xs))
- Weak DPs:
append#(nil(),ys) -> c_2()
attach#(x,nil()) -> c_4()
pairs#(nil()) -> c_6()
- Weak TRS:
append(cons(x,xs),ys) -> cons(x,append(xs,ys))
append(nil(),ys) -> ys
attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
attach(x,nil()) -> nil()
pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
pairs(nil()) -> nil()
- Signature:
{append/2,attach/2,pairs/1,append#/2,attach#/2,pairs#/1} / {cons/2,nil/0,pair/2,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/3,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,attach#,pairs#} and constructors {cons,nil,pair}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
-->_1 append#(nil(),ys) -> c_2():4
-->_1 append#(cons(x,xs),ys) -> c_1(append#(xs,ys)):1
2:S:attach#(x,cons(y,ys)) -> c_3(attach#(x,ys))
-->_1 attach#(x,nil()) -> c_4():5
-->_1 attach#(x,cons(y,ys)) -> c_3(attach#(x,ys)):2
3:S:pairs#(cons(x,xs)) -> c_5(append#(attach(x,xs),pairs(xs)),attach#(x,xs),pairs#(xs))
-->_3 pairs#(nil()) -> c_6():6
-->_2 attach#(x,nil()) -> c_4():5
-->_1 append#(nil(),ys) -> c_2():4
-->_3 pairs#(cons(x,xs)) -> c_5(append#(attach(x,xs),pairs(xs)),attach#(x,xs),pairs#(xs)):3
-->_2 attach#(x,cons(y,ys)) -> c_3(attach#(x,ys)):2
-->_1 append#(cons(x,xs),ys) -> c_1(append#(xs,ys)):1
4:W:append#(nil(),ys) -> c_2()
5:W:attach#(x,nil()) -> c_4()
6:W:pairs#(nil()) -> c_6()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
6: pairs#(nil()) -> c_6()
5: attach#(x,nil()) -> c_4()
4: append#(nil(),ys) -> c_2()
* Step 4: DecomposeDG WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
attach#(x,cons(y,ys)) -> c_3(attach#(x,ys))
pairs#(cons(x,xs)) -> c_5(append#(attach(x,xs),pairs(xs)),attach#(x,xs),pairs#(xs))
- Weak TRS:
append(cons(x,xs),ys) -> cons(x,append(xs,ys))
append(nil(),ys) -> ys
attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
attach(x,nil()) -> nil()
pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
pairs(nil()) -> nil()
- Signature:
{append/2,attach/2,pairs/1,append#/2,attach#/2,pairs#/1} / {cons/2,nil/0,pair/2,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/3,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,attach#,pairs#} and constructors {cons,nil,pair}
+ 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
pairs#(cons(x,xs)) -> c_5(append#(attach(x,xs),pairs(xs)),attach#(x,xs),pairs#(xs))
and a lower component
append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
attach#(x,cons(y,ys)) -> c_3(attach#(x,ys))
Further, following extension rules are added to the lower component.
pairs#(cons(x,xs)) -> append#(attach(x,xs),pairs(xs))
pairs#(cons(x,xs)) -> attach#(x,xs)
pairs#(cons(x,xs)) -> pairs#(xs)
** Step 4.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
pairs#(cons(x,xs)) -> c_5(append#(attach(x,xs),pairs(xs)),attach#(x,xs),pairs#(xs))
- Weak TRS:
append(cons(x,xs),ys) -> cons(x,append(xs,ys))
append(nil(),ys) -> ys
attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
attach(x,nil()) -> nil()
pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
pairs(nil()) -> nil()
- Signature:
{append/2,attach/2,pairs/1,append#/2,attach#/2,pairs#/1} / {cons/2,nil/0,pair/2,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/3,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,attach#,pairs#} and constructors {cons,nil,pair}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:pairs#(cons(x,xs)) -> c_5(append#(attach(x,xs),pairs(xs)),attach#(x,xs),pairs#(xs))
-->_3 pairs#(cons(x,xs)) -> c_5(append#(attach(x,xs),pairs(xs)),attach#(x,xs),pairs#(xs)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
pairs#(cons(x,xs)) -> c_5(pairs#(xs))
** Step 4.a:2: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
pairs#(cons(x,xs)) -> c_5(pairs#(xs))
- Weak TRS:
append(cons(x,xs),ys) -> cons(x,append(xs,ys))
append(nil(),ys) -> ys
attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
attach(x,nil()) -> nil()
pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
pairs(nil()) -> nil()
- Signature:
{append/2,attach/2,pairs/1,append#/2,attach#/2,pairs#/1} / {cons/2,nil/0,pair/2,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/1,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,attach#,pairs#} and constructors {cons,nil,pair}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
pairs#(cons(x,xs)) -> c_5(pairs#(xs))
** Step 4.a:3: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
pairs#(cons(x,xs)) -> c_5(pairs#(xs))
- Signature:
{append/2,attach/2,pairs/1,append#/2,attach#/2,pairs#/1} / {cons/2,nil/0,pair/2,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/1,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,attach#,pairs#} and constructors {cons,nil,pair}
+ 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(c_5) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(append) = [2] x1 + [1] x2 + [1]
p(attach) = [2] x1 + [1]
p(cons) = [1] x2 + [1]
p(nil) = [2]
p(pair) = [1] x2 + [2]
p(pairs) = [1]
p(append#) = [4]
p(attach#) = [1] x2 + [1]
p(pairs#) = [1] x1 + [0]
p(c_1) = [1]
p(c_2) = [0]
p(c_3) = [1] x1 + [1]
p(c_4) = [8]
p(c_5) = [1] x1 + [0]
p(c_6) = [2]
Following rules are strictly oriented:
pairs#(cons(x,xs)) = [1] xs + [1]
> [1] xs + [0]
= c_5(pairs#(xs))
Following rules are (at-least) weakly oriented:
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 4.a:4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
pairs#(cons(x,xs)) -> c_5(pairs#(xs))
- Signature:
{append/2,attach/2,pairs/1,append#/2,attach#/2,pairs#/1} / {cons/2,nil/0,pair/2,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/1,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,attach#,pairs#} and constructors {cons,nil,pair}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
** Step 4.b:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
attach#(x,cons(y,ys)) -> c_3(attach#(x,ys))
- Weak DPs:
pairs#(cons(x,xs)) -> append#(attach(x,xs),pairs(xs))
pairs#(cons(x,xs)) -> attach#(x,xs)
pairs#(cons(x,xs)) -> pairs#(xs)
- Weak TRS:
append(cons(x,xs),ys) -> cons(x,append(xs,ys))
append(nil(),ys) -> ys
attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
attach(x,nil()) -> nil()
pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
pairs(nil()) -> nil()
- Signature:
{append/2,attach/2,pairs/1,append#/2,attach#/2,pairs#/1} / {cons/2,nil/0,pair/2,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/3,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,attach#,pairs#} and constructors {cons,nil,pair}
+ 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},
uargs(c_3) = {1}
Following symbols are considered usable:
{append#,attach#,pairs#}
TcT has computed the following interpretation:
p(append) = [1] x1 + [9]
p(attach) = [4] x1 + [9]
p(cons) = [1] x1 + [1] x2 + [8]
p(nil) = [0]
p(pair) = [1] x1 + [4]
p(pairs) = [0]
p(append#) = [0]
p(attach#) = [2] x2 + [1]
p(pairs#) = [2] x1 + [0]
p(c_1) = [4] x1 + [0]
p(c_2) = [1]
p(c_3) = [1] x1 + [14]
p(c_4) = [1]
p(c_5) = [1] x1 + [1] x3 + [1]
p(c_6) = [0]
Following rules are strictly oriented:
attach#(x,cons(y,ys)) = [2] y + [2] ys + [17]
> [2] ys + [15]
= c_3(attach#(x,ys))
Following rules are (at-least) weakly oriented:
append#(cons(x,xs),ys) = [0]
>= [0]
= c_1(append#(xs,ys))
pairs#(cons(x,xs)) = [2] x + [2] xs + [16]
>= [0]
= append#(attach(x,xs),pairs(xs))
pairs#(cons(x,xs)) = [2] x + [2] xs + [16]
>= [2] xs + [1]
= attach#(x,xs)
pairs#(cons(x,xs)) = [2] x + [2] xs + [16]
>= [2] xs + [0]
= pairs#(xs)
** Step 4.b:2: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
- Weak DPs:
attach#(x,cons(y,ys)) -> c_3(attach#(x,ys))
pairs#(cons(x,xs)) -> append#(attach(x,xs),pairs(xs))
pairs#(cons(x,xs)) -> attach#(x,xs)
pairs#(cons(x,xs)) -> pairs#(xs)
- Weak TRS:
append(cons(x,xs),ys) -> cons(x,append(xs,ys))
append(nil(),ys) -> ys
attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
attach(x,nil()) -> nil()
pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
pairs(nil()) -> nil()
- Signature:
{append/2,attach/2,pairs/1,append#/2,attach#/2,pairs#/1} / {cons/2,nil/0,pair/2,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/3,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,attach#,pairs#} and constructors {cons,nil,pair}
+ 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},
uargs(c_3) = {1}
Following symbols are considered usable:
{attach,append#,attach#,pairs#}
TcT has computed the following interpretation:
p(append) = [4]
p(attach) = [8] x2 + [8]
p(cons) = [1] x2 + [1]
p(nil) = [0]
p(pair) = [1]
p(pairs) = [8]
p(append#) = [1] x1 + [0]
p(attach#) = [4] x2 + [0]
p(pairs#) = [8] x1 + [0]
p(c_1) = [1] x1 + [0]
p(c_2) = [1]
p(c_3) = [1] x1 + [1]
p(c_4) = [0]
p(c_5) = [1] x1 + [1] x3 + [0]
p(c_6) = [8]
Following rules are strictly oriented:
append#(cons(x,xs),ys) = [1] xs + [1]
> [1] xs + [0]
= c_1(append#(xs,ys))
Following rules are (at-least) weakly oriented:
attach#(x,cons(y,ys)) = [4] ys + [4]
>= [4] ys + [1]
= c_3(attach#(x,ys))
pairs#(cons(x,xs)) = [8] xs + [8]
>= [8] xs + [8]
= append#(attach(x,xs),pairs(xs))
pairs#(cons(x,xs)) = [8] xs + [8]
>= [4] xs + [0]
= attach#(x,xs)
pairs#(cons(x,xs)) = [8] xs + [8]
>= [8] xs + [0]
= pairs#(xs)
attach(x,cons(y,ys)) = [8] ys + [16]
>= [8] ys + [9]
= cons(pair(x,y),attach(x,ys))
attach(x,nil()) = [8]
>= [0]
= nil()
** Step 4.b:3: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
attach#(x,cons(y,ys)) -> c_3(attach#(x,ys))
pairs#(cons(x,xs)) -> append#(attach(x,xs),pairs(xs))
pairs#(cons(x,xs)) -> attach#(x,xs)
pairs#(cons(x,xs)) -> pairs#(xs)
- Weak TRS:
append(cons(x,xs),ys) -> cons(x,append(xs,ys))
append(nil(),ys) -> ys
attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys))
attach(x,nil()) -> nil()
pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs))
pairs(nil()) -> nil()
- Signature:
{append/2,attach/2,pairs/1,append#/2,attach#/2,pairs#/1} / {cons/2,nil/0,pair/2,c_1/1,c_2/0,c_3/1,c_4/0
,c_5/3,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,attach#,pairs#} and constructors {cons,nil,pair}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))