tct
| Execution Time (secs) | 16.985 |
| Answer | YES(?,O(n^2)) |
| Input | flatten.raml |
YES(?,O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Weak Trs:
{ #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We add following dependency tuples
Strict DPs:
{ #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, append#1^#(nil(), @l2) -> c_4()
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(leaf()) -> c_6()
, flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsort#1^#(nil()) -> c_16()
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#1^#(nil(), @x) -> c_12()
, insert#2^#(#false(), @x, @y, @ys) -> c_13()
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak DPs:
{ #cklt^#(#EQ()) -> c_29()
, #cklt^#(#GT()) -> c_30()
, #cklt^#(#LT()) -> c_31()
, #compare^#(#0(), #0()) -> c_17()
, #compare^#(#0(), #neg(@y)) -> c_18()
, #compare^#(#0(), #pos(@y)) -> c_19()
, #compare^#(#0(), #s(@y)) -> c_20()
, #compare^#(#neg(@x), #0()) -> c_21()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_23()
, #compare^#(#pos(@x), #0()) -> c_24()
, #compare^#(#pos(@x), #neg(@y)) -> c_25()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_27()
, #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) }
and replace the set of basic marked basic terms accordingly.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, append#1^#(nil(), @l2) -> c_4()
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(leaf()) -> c_6()
, flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsort#1^#(nil()) -> c_16()
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#1^#(nil(), @x) -> c_12()
, insert#2^#(#false(), @x, @y, @ys) -> c_13()
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak DPs:
{ #cklt^#(#EQ()) -> c_29()
, #cklt^#(#GT()) -> c_30()
, #cklt^#(#LT()) -> c_31()
, #compare^#(#0(), #0()) -> c_17()
, #compare^#(#0(), #neg(@y)) -> c_18()
, #compare^#(#0(), #pos(@y)) -> c_19()
, #compare^#(#0(), #s(@y)) -> c_20()
, #compare^#(#neg(@x), #0()) -> c_21()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_23()
, #compare^#(#pos(@x), #0()) -> c_24()
, #compare^#(#pos(@x), #neg(@y)) -> c_25()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_27()
, #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the (estimated) dependency graph
1: #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
-->_2 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :31
-->_2 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :29
-->_2 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :25
-->_2 #compare^#(#s(@x), #0()) -> c_27() :30
-->_2 #compare^#(#pos(@x), #neg(@y)) -> c_25() :28
-->_2 #compare^#(#pos(@x), #0()) -> c_24() :27
-->_2 #compare^#(#neg(@x), #pos(@y)) -> c_23() :26
-->_2 #compare^#(#neg(@x), #0()) -> c_21() :24
-->_2 #compare^#(#0(), #s(@y)) -> c_20() :23
-->_2 #compare^#(#0(), #pos(@y)) -> c_19() :22
-->_2 #compare^#(#0(), #neg(@y)) -> c_18() :21
-->_2 #compare^#(#0(), #0()) -> c_17() :20
-->_1 #cklt^#(#LT()) -> c_31() :19
-->_1 #cklt^#(#GT()) -> c_30() :18
-->_1 #cklt^#(#EQ()) -> c_29() :17
2: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :3
-->_1 append#1^#(nil(), @l2) -> c_4() :4
3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :2
4: append#1^#(nil(), @l2) -> c_4()
5: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :7
-->_1 flatten#1^#(leaf()) -> c_6() :6
6: flatten#1^#(leaf()) -> c_6()
7: flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :5
-->_3 flatten^#(@t) -> flatten#1^#(@t) :5
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :2
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :2
8: flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :9
-->_2 flatten^#(@t) -> flatten#1^#(@t) :5
9: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :10
-->_1 insertionsort#1^#(nil()) -> c_16() :11
10: insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :12
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :9
11: insertionsort#1^#(nil()) -> c_16()
12: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :13
-->_1 insert#1^#(nil(), @x) -> c_12() :14
13: insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :16
-->_1 insert#2^#(#false(), @x, @y, @ys) -> c_13() :15
-->_2 #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) :1
14: insert#1^#(nil(), @x) -> c_12()
15: insert#2^#(#false(), @x, @y, @ys) -> c_13()
16: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :12
17: #cklt^#(#EQ()) -> c_29()
18: #cklt^#(#GT()) -> c_30()
19: #cklt^#(#LT()) -> c_31()
20: #compare^#(#0(), #0()) -> c_17()
21: #compare^#(#0(), #neg(@y)) -> c_18()
22: #compare^#(#0(), #pos(@y)) -> c_19()
23: #compare^#(#0(), #s(@y)) -> c_20()
24: #compare^#(#neg(@x), #0()) -> c_21()
25: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :31
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :29
-->_1 #compare^#(#s(@x), #0()) -> c_27() :30
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_25() :28
-->_1 #compare^#(#pos(@x), #0()) -> c_24() :27
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_23() :26
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :25
-->_1 #compare^#(#neg(@x), #0()) -> c_21() :24
-->_1 #compare^#(#0(), #s(@y)) -> c_20() :23
-->_1 #compare^#(#0(), #pos(@y)) -> c_19() :22
-->_1 #compare^#(#0(), #neg(@y)) -> c_18() :21
-->_1 #compare^#(#0(), #0()) -> c_17() :20
26: #compare^#(#neg(@x), #pos(@y)) -> c_23()
27: #compare^#(#pos(@x), #0()) -> c_24()
28: #compare^#(#pos(@x), #neg(@y)) -> c_25()
29: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :31
-->_1 #compare^#(#s(@x), #0()) -> c_27() :30
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :29
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_25() :28
-->_1 #compare^#(#pos(@x), #0()) -> c_24() :27
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_23() :26
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :25
-->_1 #compare^#(#neg(@x), #0()) -> c_21() :24
-->_1 #compare^#(#0(), #s(@y)) -> c_20() :23
-->_1 #compare^#(#0(), #pos(@y)) -> c_19() :22
-->_1 #compare^#(#0(), #neg(@y)) -> c_18() :21
-->_1 #compare^#(#0(), #0()) -> c_17() :20
30: #compare^#(#s(@x), #0()) -> c_27()
31: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :31
-->_1 #compare^#(#s(@x), #0()) -> c_27() :30
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :29
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_25() :28
-->_1 #compare^#(#pos(@x), #0()) -> c_24() :27
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_23() :26
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :25
-->_1 #compare^#(#neg(@x), #0()) -> c_21() :24
-->_1 #compare^#(#0(), #s(@y)) -> c_20() :23
-->_1 #compare^#(#0(), #pos(@y)) -> c_19() :22
-->_1 #compare^#(#0(), #neg(@y)) -> c_18() :21
-->_1 #compare^#(#0(), #0()) -> c_17() :20
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {11} and add Pre({11}) = {9} to the strict component.
- We remove {14} and add Pre({14}) = {12} to the strict component.
- We remove {15} and add Pre({15}) = {13} to the strict component.
- We remove {6} and add Pre({6}) = {5} to the strict component.
- We remove {4} and add Pre({4}) = {2} to the strict component.
- We remove {1} and add Pre({1}) = {13} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak DPs:
{ #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, #cklt^#(#EQ()) -> c_29()
, #cklt^#(#GT()) -> c_30()
, #cklt^#(#LT()) -> c_31()
, #compare^#(#0(), #0()) -> c_17()
, #compare^#(#0(), #neg(@y)) -> c_18()
, #compare^#(#0(), #pos(@y)) -> c_19()
, #compare^#(#0(), #s(@y)) -> c_20()
, #compare^#(#neg(@x), #0()) -> c_21()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_23()
, #compare^#(#pos(@x), #0()) -> c_24()
, #compare^#(#pos(@x), #neg(@y)) -> c_25()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_27()
, #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, append#1^#(nil(), @l2) -> c_4()
, flatten#1^#(leaf()) -> c_6()
, insertionsort#1^#(nil()) -> c_16()
, insert#1^#(nil(), @x) -> c_12()
, insert#2^#(#false(), @x, @y, @ys) -> c_13() }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the the dependency graph
->1:{5}
|
|->21:{3,4}
| |
| |->23:{1,2}
| | |
| | `->24:{27} Weak SCC
| |
| `->22:{28} Weak SCC
|
`->2:{6,7}
|
|->4:{8,10,9}
| |
| |->7:{11} Weak SCC
| | |
| | |->8:{12} Weak SCC
| | |
| | |->9:{13} Weak SCC
| | |
| | |->10:{14} Weak SCC
| | |
| | |->12:{15} Weak SCC
| | |
| | |->13:{16} Weak SCC
| | |
| | |->14:{17} Weak SCC
| | |
| | |->15:{18} Weak SCC
| | |
| | |->16:{19} Weak SCC
| | |
| | |->17:{21} Weak SCC
| | |
| | |->18:{22} Weak SCC
| | |
| | |->19:{23} Weak SCC
| | |
| | |->20:{25} Weak SCC
| | |
| | `->11:{26,24,20} Weak SCC
| | |
| | |->12:{15} Weak SCC
| | |
| | |->13:{16} Weak SCC
| | |
| | |->14:{17} Weak SCC
| | |
| | |->15:{18} Weak SCC
| | |
| | |->16:{19} Weak SCC
| | |
| | |->17:{21} Weak SCC
| | |
| | |->18:{22} Weak SCC
| | |
| | |->19:{23} Weak SCC
| | |
| | `->20:{25} Weak SCC
| |
| |->5:{30} Weak SCC
| |
| `->6:{31} Weak SCC
|
`->3:{29} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 3: flatten^#(@t) -> flatten#1^#(@t)
, 4: flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, 5: flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
, 6: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 7: insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, 8: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 9: insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, 10: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak DPs:
{ 11: #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, 12: #cklt^#(#EQ()) -> c_29()
, 13: #cklt^#(#GT()) -> c_30()
, 14: #cklt^#(#LT()) -> c_31()
, 15: #compare^#(#0(), #0()) -> c_17()
, 16: #compare^#(#0(), #neg(@y)) -> c_18()
, 17: #compare^#(#0(), #pos(@y)) -> c_19()
, 18: #compare^#(#0(), #s(@y)) -> c_20()
, 19: #compare^#(#neg(@x), #0()) -> c_21()
, 20: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, 21: #compare^#(#neg(@x), #pos(@y)) -> c_23()
, 22: #compare^#(#pos(@x), #0()) -> c_24()
, 23: #compare^#(#pos(@x), #neg(@y)) -> c_25()
, 24: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, 25: #compare^#(#s(@x), #0()) -> c_27()
, 26: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, 27: append#1^#(nil(), @l2) -> c_4()
, 28: flatten#1^#(leaf()) -> c_6()
, 29: insertionsort#1^#(nil()) -> c_16()
, 30: insert#1^#(nil(), @x) -> c_12()
, 31: insert#2^#(#false(), @x, @y, @ys) -> c_13() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 29: insertionsort#1^#(nil()) -> c_16()
, 30: insert#1^#(nil(), @x) -> c_12()
, 31: insert#2^#(#false(), @x, @y, @ys) -> c_13()
, 11: #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, 12: #cklt^#(#EQ()) -> c_29()
, 13: #cklt^#(#GT()) -> c_30()
, 14: #cklt^#(#LT()) -> c_31()
, 26: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, 24: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, 20: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, 15: #compare^#(#0(), #0()) -> c_17()
, 16: #compare^#(#0(), #neg(@y)) -> c_18()
, 17: #compare^#(#0(), #pos(@y)) -> c_19()
, 18: #compare^#(#0(), #s(@y)) -> c_20()
, 19: #compare^#(#neg(@x), #0()) -> c_21()
, 21: #compare^#(#neg(@x), #pos(@y)) -> c_23()
, 22: #compare^#(#pos(@x), #0()) -> c_24()
, 23: #compare^#(#pos(@x), #neg(@y)) -> c_25()
, 25: #compare^#(#s(@x), #0()) -> c_27()
, 28: flatten#1^#(leaf()) -> c_6()
, 27: append#1^#(nil(), @l2) -> c_4() }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the following dependency-graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :2
2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
3: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :4
4: flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :3
-->_3 flatten^#(@t) -> flatten#1^#(@t) :3
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :6
-->_2 flatten^#(@t) -> flatten#1^#(@t) :3
6: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :7
7: insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :8
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :6
8: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :9
9: insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :10
10: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :8
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We employ 'linear path analysis' using the following approximated
dependency graph:
->1:{5} [ ? ]
|
|->4:{3,4} [ ? ]
| |
| `->5:{1,2} [ YES(O(1),O(n^2)) ]
|
`->2:{6,7} [ ? ]
|
`->3:{8,10,9} [ YES(O(1),O(n^2)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 3: flatten^#(@t) -> flatten#1^#(@t)
, 4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, 5: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, 6: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 7: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, 8: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 9: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, 10: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
* Path 1:{5}->4:{3,4}->5:{1,2}: YES(O(1),O(n^2))
----------------------------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :2
2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
3: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :4
4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :3
-->_3 flatten^#(@t) -> flatten#1^#(@t) :3
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_2 flatten^#(@t) -> flatten#1^#(@t) :3
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
Weak DPs: { append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :5
2: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :3
3: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :2
-->_3 flatten^#(@t) -> flatten#1^#(@t) :2
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
4: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_2 flatten^#(@t) -> flatten#1^#(@t) :2
5: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {2} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :4
2: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :5
3: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_2 flatten^#(@t) -> flatten#1^#(@t) :2
4: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :2
-->_3 flatten^#(@t) -> flatten#1^#(@t) :2
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, flatten^#(@t) -> flatten#1^#(@t) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the following dependency-graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :3
2: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :4
3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :2
-->_3 flatten^#(@t) -> flatten#1^#(@t) :2
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_2 flatten^#(@t) -> flatten#1^#(@t) :2
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, flatten^#(@t) -> flatten#1^#(@t) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) -> flatten^#(@t) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, flatten^#(@t) -> flatten#1^#(@t) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) -> flatten^#(@t) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, 5: flattensort^#(@t) -> flatten^#(@t) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(append) = {}, Uargs(append#1) = {}, Uargs(::) = {},
Uargs(flatten) = {}, Uargs(flatten#1) = {}, Uargs(node) = {},
Uargs(#neg) = {}, Uargs(#pos) = {}, Uargs(#s) = {},
Uargs(#less^#) = {}, Uargs(#cklt^#) = {}, Uargs(#compare^#) = {},
Uargs(append^#) = {}, Uargs(append#1^#) = {},
Uargs(flatten^#) = {}, Uargs(flatten#1^#) = {},
Uargs(flattensort^#) = {}, Uargs(insertionsort^#) = {},
Uargs(insertionsort#1^#) = {}, Uargs(insert^#) = {},
Uargs(insert#1^#) = {}, Uargs(insert#2^#) = {},
Uargs(c_1) = {1, 2, 3, 4}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[append](x1, x2) = [0 0] x1 + [2 0] x2 + [0]
[0 1] [0 1] [0]
[append#1](x1, x2) = [0 0] x1 + [2 0] x2 + [0]
[0 1] [0 1] [0]
[::](x1, x2) = [1 0] x2 + [0]
[0 1] [2]
[nil] = [0]
[0]
[flatten](x1) = [0 0] x1 + [0]
[0 2] [0]
[flatten#1](x1) = [0 0] x1 + [0]
[0 2] [0]
[leaf] = [0]
[0]
[node](x1, x2, x3) = [0 3] x1 + [1 3] x2 + [1 0] x3 + [2]
[0 1] [0 1] [0 1] [0]
[#false] = [0]
[0]
[#true] = [0]
[0]
[#EQ] = [0]
[0]
[#GT] = [0]
[0]
[#LT] = [0]
[0]
[#0] = [0]
[0]
[#neg](x1) = [0]
[0]
[#pos](x1) = [0]
[0]
[#s](x1) = [1 1] x1 + [0]
[0 0] [0]
[#less^#](x1, x2) = [0]
[0]
[#cklt^#](x1) = [0]
[0]
[#compare^#](x1, x2) = [0]
[0]
[append^#](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[append#1^#](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[flatten^#](x1) = [1 0] x1 + [0]
[0 0] [1]
[flatten#1^#](x1) = [1 0] x1 + [0]
[0 0] [0]
[flattensort^#](x1) = [3 3] x1 + [3]
[3 3] [3]
[insertionsort^#](x1) = [0]
[0]
[insertionsort#1^#](x1) = [0]
[0]
[insert^#](x1, x2) = [0]
[0]
[insert#1^#](x1, x2) = [0]
[0]
[insert#2^#](x1, x2, x3, x4) = [0]
[0]
[c_1](x1, x2, x3, x4) = [2 1] x1 + [1 1] x2 + [1 0] x3 + [1
0] x4 + [1]
[0 0] [0 0] [0 0] [0
0] [0]
This order satisfies following ordering constraints
[append(@l1, @l2)] = [0 0] @l1 + [2 0] @l2 + [0]
[0 1] [0 1] [0]
>= [0 0] @l1 + [2 0] @l2 + [0]
[0 1] [0 1] [0]
= [append#1(@l1, @l2)]
[append#1(::(@x, @xs), @l2)] = [2 0] @l2 + [0 0] @xs + [0]
[0 1] [0 1] [2]
>= [2 0] @l2 + [0 0] @xs + [0]
[0 1] [0 1] [2]
= [::(@x, append(@xs, @l2))]
[append#1(nil(), @l2)] = [2 0] @l2 + [0]
[0 1] [0]
>= [1 0] @l2 + [0]
[0 1] [0]
= [@l2]
[flatten(@t)] = [0 0] @t + [0]
[0 2] [0]
>= [0 0] @t + [0]
[0 2] [0]
= [flatten#1(@t)]
[flatten#1(leaf())] = [0]
[0]
>= [0]
[0]
= [nil()]
[flatten#1(node(@l, @t1, @t2))] = [0 0] @l + [0 0] @t1 + [0 0] @t2 + [0]
[0 2] [0 2] [0 2] [0]
>= [0 0] @l + [0 0] @t1 + [0 0] @t2 + [0]
[0 1] [0 2] [0 2] [0]
= [append(@l, append(flatten(@t1), flatten(@t2)))]
[append^#(@l1, @l2)] = [0 1] @l1 + [0]
[0 0] [0]
>= [0 1] @l1 + [0]
[0 0] [0]
= [append#1^#(@l1, @l2)]
[append#1^#(::(@x, @xs), @l2)] = [0 1] @xs + [2]
[0 0] [0]
> [0 1] @xs + [0]
[0 0] [0]
= [append^#(@xs, @l2)]
[flatten^#(@t)] = [1 0] @t + [0]
[0 0] [1]
>= [1 0] @t + [0]
[0 0] [0]
= [flatten#1^#(@t)]
[flatten#1^#(node(@l, @t1, @t2))] = [0 3] @l + [1 3] @t1 + [1 0] @t2 + [2]
[0 0] [0 0] [0 0] [0]
> [0 2] @l + [1 2] @t1 + [1 0] @t2 + [1]
[0 0] [0 0] [0 0] [0]
= [c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))]
[flattensort^#(@t)] = [3 3] @t + [3]
[3 3] [3]
> [1 0] @t + [0]
[0 0] [1]
= [flatten^#(@t)]
Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^2)) on application of rules
{3,4,5}. Here rules are labeled according to the (estimated)
dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :3
2: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :4
3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :2
-->_3 flatten^#(@t) -> flatten#1^#(@t) :2
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: flattensort^#(@t) -> flatten^#(@t)
-->_1 flatten^#(@t) -> flatten#1^#(@t) :2
- The rules {3,4,5} have known complexity. These cover all
predecessors of {1,2}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4,5} is given by YES(?,O(n^2)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) -> flatten^#(@t) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{5} Weak SCC
|
`->2:{3,4} Weak SCC
|
`->3:{1,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 3: flatten^#(@t) -> flatten#1^#(@t)
, 4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, 5: flattensort^#(@t) -> flatten^#(@t) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 5: flattensort^#(@t) -> flatten^#(@t)
, 3: flatten^#(@t) -> flatten#1^#(@t)
, 4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) }
We apply the transformation 'usablerules' on the sub-problem:
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
* Path 1:{5}->2:{6,7}->3:{8,10,9}: YES(O(1),O(n^2))
-------------------------------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :3
3: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
4: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :5
5: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :6
6: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {6} and add Pre({6}) = {5} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) }
Weak DPs: { insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :3
3: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
4: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :5
5: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :6
6: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {5} and add Pre({5}) = {4} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :3
3: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
4: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :5
5: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :6
6: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {2} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :4
3: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :5
4: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :3
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
5: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :6
6: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :3
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {1} and add Pre({1}) = {} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insertionsort^#(@l) -> insertionsort#1^#(@l)
, insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the following dependency-graph
1: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :4
2: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :5
3: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
4: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :2
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
5: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :6
6: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :2
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insertionsort^#(@l) -> insertionsort#1^#(@l)
, insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insertionsort^#(@l) -> insertionsort#1^#(@l)
, insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We measure the number of applications of following selected rules
relative to the remaining rules.
Selected Rules (A):
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Remaining Rules (B):
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
The length of a single A-subderivation is expressed by the
following problem.
Problem (A):
------------
Strict DPs: { insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
The number of B-applications is expressed by the following problem.
Problem (B):
------------
Strict DPs:
{ insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak DPs: { flattensort^#(@t) -> insertionsort^#(flatten(@t)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
TcT answers on problem (B) YES(O(1),O(n^1)).
Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak DPs: { flattensort^#(@t) -> insertionsort^#(flatten(@t)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :2
2: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
3: flattensort^#(@t) -> insertionsort^#(flatten(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { insertionsort^#(@l) -> insertionsort#1^#(@l) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the following dependency-graph
1: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :3
2: flattensort^#(@t) -> insertionsort^#(flatten(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
3: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { insertionsort^#(@l) -> insertionsort#1^#(@l) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { insertionsort^#(@l) -> insertionsort#1^#(@l) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
Trs:
{ flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(#less) = {}, Uargs(#compare) = {}, Uargs(#cklt) = {},
Uargs(append) = {}, Uargs(append#1) = {}, Uargs(::) = {},
Uargs(flatten) = {}, Uargs(flatten#1) = {}, Uargs(node) = {},
Uargs(insertionsort) = {}, Uargs(insert) = {},
Uargs(insert#1) = {}, Uargs(insert#2) = {},
Uargs(insertionsort#1) = {}, Uargs(#neg) = {}, Uargs(#pos) = {},
Uargs(#s) = {}, Uargs(#less^#) = {}, Uargs(#cklt^#) = {},
Uargs(#compare^#) = {}, Uargs(append^#) = {},
Uargs(append#1^#) = {}, Uargs(flatten^#) = {},
Uargs(flatten#1^#) = {}, Uargs(flattensort^#) = {},
Uargs(insertionsort^#) = {}, Uargs(insertionsort#1^#) = {},
Uargs(insert^#) = {}, Uargs(insert#1^#) = {},
Uargs(insert#2^#) = {}, Uargs(c_1) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#less](x1, x2) = [0]
[#compare](x1, x2) = [0]
[#cklt](x1) = [0]
[append](x1, x2) = [1] x1 + [1] x2 + [0]
[append#1](x1, x2) = [1] x1 + [1] x2 + [0]
[::](x1, x2) = [1] x2 + [3]
[nil] = [0]
[flatten](x1) = [3] x1 + [0]
[flatten#1](x1) = [3] x1 + [0]
[leaf] = [0]
[node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [3]
[insertionsort](x1) = [0]
[insert](x1, x2) = [0]
[insert#1](x1, x2) = [0]
[insert#2](x1, x2, x3, x4) = [0]
[#false] = [0]
[#true] = [0]
[insertionsort#1](x1) = [0]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
[#0] = [0]
[#neg](x1) = [0]
[#pos](x1) = [0]
[#s](x1) = [0]
[#less^#](x1, x2) = [0]
[#cklt^#](x1) = [0]
[#compare^#](x1, x2) = [0]
[append^#](x1, x2) = [0]
[append#1^#](x1, x2) = [0]
[flatten^#](x1) = [0]
[flatten#1^#](x1) = [0]
[flattensort^#](x1) = [3] x1 + [3]
[insertionsort^#](x1) = [1] x1 + [3]
[insertionsort#1^#](x1) = [1] x1 + [3]
[insert^#](x1, x2) = [0]
[insert#1^#](x1, x2) = [0]
[insert#2^#](x1, x2, x3, x4) = [0]
[c_1](x1, x2) = [0]
[c] = [0]
This order satisfies following ordering constraints
[append(@l1, @l2)] = [1] @l1 + [1] @l2 + [0]
>= [1] @l1 + [1] @l2 + [0]
= [append#1(@l1, @l2)]
[append#1(::(@x, @xs), @l2)] = [1] @l2 + [1] @xs + [3]
>= [1] @l2 + [1] @xs + [3]
= [::(@x, append(@xs, @l2))]
[append#1(nil(), @l2)] = [1] @l2 + [0]
>= [1] @l2 + [0]
= [@l2]
[flatten(@t)] = [3] @t + [0]
>= [3] @t + [0]
= [flatten#1(@t)]
[flatten#1(leaf())] = [0]
>= [0]
= [nil()]
[flatten#1(node(@l, @t1, @t2))] = [3] @l + [3] @t1 + [3] @t2 + [9]
> [1] @l + [3] @t1 + [3] @t2 + [0]
= [append(@l, append(flatten(@t1), flatten(@t2)))]
[flattensort^#(@t)] = [3] @t + [3]
>= [3] @t + [3]
= [insertionsort^#(flatten(@t))]
[insertionsort^#(@l)] = [1] @l + [3]
>= [1] @l + [3]
= [insertionsort#1^#(@l)]
[insertionsort#1^#(::(@x, @xs))] = [1] @xs + [6]
> [1] @xs + [3]
= [insertionsort^#(@xs)]
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of rules {3}.
Here rules are labeled according to the (estimated) dependency
graph
1: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) :3
2: flattensort^#(@t) -> insertionsort^#(flatten(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
- The rules {3} have known complexity. These cover all predecessors
of {2}, their complexity is equally bounded.
- The rules {2,3} have known complexity. These cover all
predecessors of {1}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules {1,2,3}
is given by YES(?,O(n^1)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1} Weak SCC
|
`->2:{2,3} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: flattensort^#(@t) -> insertionsort^#(flatten(@t))
, 2: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 1: flattensort^#(@t) -> insertionsort^#(flatten(@t))
, 2: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
We apply the transformation 'usablerules' on the sub-problem:
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 2: flattensort^#(@t) -> insertionsort^#(flatten(@t))
, 4: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, 5: insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs)) }
Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, append#1(nil(), @l2) -> @l2
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertionsort#1(nil()) -> nil() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(#less) = {}, Uargs(#compare) = {}, Uargs(#cklt) = {},
Uargs(append) = {}, Uargs(append#1) = {}, Uargs(::) = {},
Uargs(flatten) = {}, Uargs(flatten#1) = {}, Uargs(node) = {},
Uargs(insertionsort) = {}, Uargs(insert) = {},
Uargs(insert#1) = {}, Uargs(insert#2) = {},
Uargs(insertionsort#1) = {}, Uargs(#neg) = {}, Uargs(#pos) = {},
Uargs(#s) = {}, Uargs(#less^#) = {}, Uargs(#cklt^#) = {},
Uargs(#compare^#) = {}, Uargs(append^#) = {},
Uargs(append#1^#) = {}, Uargs(flatten^#) = {},
Uargs(flatten#1^#) = {}, Uargs(flattensort^#) = {},
Uargs(insertionsort^#) = {}, Uargs(insertionsort#1^#) = {},
Uargs(insert^#) = {}, Uargs(insert#1^#) = {},
Uargs(insert#2^#) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#less](x1, x2) = [1]
[#compare](x1, x2) = [0]
[#cklt](x1) = [0]
[append](x1, x2) = [1] x1 + [1] x2 + [0]
[append#1](x1, x2) = [1] x1 + [1] x2 + [0]
[::](x1, x2) = [1] x2 + [1]
[nil] = [1]
[flatten](x1) = [1] x1 + [0]
[flatten#1](x1) = [1] x1 + [0]
[leaf] = [1]
[node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
[insertionsort](x1) = [2] x1 + [1]
[insert](x1, x2) = [1] x2 + [2]
[insert#1](x1, x2) = [1] x1 + [2]
[insert#2](x1, x2, x3, x4) = [1] x4 + [3]
[#false] = [0]
[#true] = [0]
[insertionsort#1](x1) = [2] x1 + [1]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
[#0] = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#s](x1) = [1] x1 + [0]
[#less^#](x1, x2) = [0]
[#cklt^#](x1) = [0]
[#compare^#](x1, x2) = [0]
[append^#](x1, x2) = [0]
[append#1^#](x1, x2) = [0]
[flatten^#](x1) = [0]
[flatten#1^#](x1) = [0]
[flattensort^#](x1) = [3] x1 + [3]
[insertionsort^#](x1) = [3] x1 + [2]
[insertionsort#1^#](x1) = [3] x1 + [2]
[insert^#](x1, x2) = [1] x2 + [3]
[insert#1^#](x1, x2) = [1] x1 + [2]
[insert#2^#](x1, x2, x3, x4) = [1] x4 + [3]
This order satisfies following ordering constraints
[#less(@x, @y)] = [1]
> [0]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [0]
>= [0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0]
>= [0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0]
>= [0]
= [#LT()]
[#compare(#0(), #s(@y))] = [0]
>= [0]
= [#LT()]
[#compare(#neg(@x), #0())] = [0]
>= [0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0]
>= [0]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [0]
>= [0]
= [#LT()]
[#compare(#pos(@x), #0())] = [0]
>= [0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0]
>= [0]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [0]
>= [0]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [0]
>= [0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0]
>= [0]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[append(@l1, @l2)] = [1] @l1 + [1] @l2 + [0]
>= [1] @l1 + [1] @l2 + [0]
= [append#1(@l1, @l2)]
[append#1(::(@x, @xs), @l2)] = [1] @l2 + [1] @xs + [1]
>= [1] @l2 + [1] @xs + [1]
= [::(@x, append(@xs, @l2))]
[append#1(nil(), @l2)] = [1] @l2 + [1]
> [1] @l2 + [0]
= [@l2]
[flatten(@t)] = [1] @t + [0]
>= [1] @t + [0]
= [flatten#1(@t)]
[flatten#1(leaf())] = [1]
>= [1]
= [nil()]
[flatten#1(node(@l, @t1, @t2))] = [1] @l + [1] @t1 + [1] @t2 + [1]
> [1] @l + [1] @t1 + [1] @t2 + [0]
= [append(@l, append(flatten(@t1), flatten(@t2)))]
[insertionsort(@l)] = [2] @l + [1]
>= [2] @l + [1]
= [insertionsort#1(@l)]
[insert(@x, @l)] = [1] @l + [2]
>= [1] @l + [2]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1] @ys + [3]
>= [1] @ys + [3]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [3]
> [2]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1] @ys + [3]
> [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1] @ys + [3]
>= [1] @ys + [3]
= [::(@y, insert(@x, @ys))]
[insertionsort#1(::(@x, @xs))] = [2] @xs + [3]
>= [2] @xs + [3]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [3]
> [1]
= [nil()]
[flattensort^#(@t)] = [3] @t + [3]
> [3] @t + [2]
= [insertionsort^#(flatten(@t))]
[insertionsort^#(@l)] = [3] @l + [2]
>= [3] @l + [2]
= [insertionsort#1^#(@l)]
[insertionsort#1^#(::(@x, @xs))] = [3] @xs + [5]
> [3] @xs + [2]
= [insertionsort^#(@xs)]
[insertionsort#1^#(::(@x, @xs))] = [3] @xs + [5]
> [2] @xs + [4]
= [insert^#(@x, insertionsort(@xs))]
[insert^#(@x, @l)] = [1] @l + [3]
> [1] @l + [2]
= [insert#1^#(@l, @x)]
[insert#1^#(::(@y, @ys), @x)] = [1] @ys + [3]
>= [1] @ys + [3]
= [insert#2^#(#less(@y, @x), @x, @y, @ys)]
[insert#2^#(#true(), @x, @y, @ys)] = [1] @ys + [3]
>= [1] @ys + [3]
= [insert^#(@x, @ys)]
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of rules
{1,2,4,5}. Here rules are labeled according to the (estimated)
dependency graph
1: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :6
2: flattensort^#(@t) -> insertionsort^#(flatten(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :3
3: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs)) :5
-->_1 insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) :4
4: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :3
5: insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
6: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :7
7: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
- The rules {1,2,4,5} have known complexity. These cover all
predecessors of {3,6}, their complexity is equally bounded.
- The rules {1,2,3,4,5,6} have known complexity. These cover all
predecessors of {7}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4,5,6,7} is given by YES(?,O(n^1)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1} Weak SCC
|
`->2:{2,3} Weak SCC
|
`->3:{4} Weak SCC
|
`->4:{5,7,6} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: flattensort^#(@t) -> insertionsort^#(flatten(@t))
, 2: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, 4: insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
, 5: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 6: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, 7: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 1: flattensort^#(@t) -> insertionsort^#(flatten(@t))
, 2: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, 4: insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
, 5: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 7: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 6: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) }
We apply the transformation 'usablerules' on the sub-problem:
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^2))
tct-popstar
| Execution Time (secs) | 17.493 |
| Answer | YES(?,O(n^2)) |
| Input | flatten.raml |
YES(?,O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Weak Trs:
{ #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We add following dependency tuples
Strict DPs:
{ #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, append#1^#(nil(), @l2) -> c_4()
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(leaf()) -> c_6()
, flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsort#1^#(nil()) -> c_16()
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#1^#(nil(), @x) -> c_12()
, insert#2^#(#false(), @x, @y, @ys) -> c_13()
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak DPs:
{ #cklt^#(#EQ()) -> c_29()
, #cklt^#(#GT()) -> c_30()
, #cklt^#(#LT()) -> c_31()
, #compare^#(#0(), #0()) -> c_17()
, #compare^#(#0(), #neg(@y)) -> c_18()
, #compare^#(#0(), #pos(@y)) -> c_19()
, #compare^#(#0(), #s(@y)) -> c_20()
, #compare^#(#neg(@x), #0()) -> c_21()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_23()
, #compare^#(#pos(@x), #0()) -> c_24()
, #compare^#(#pos(@x), #neg(@y)) -> c_25()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_27()
, #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) }
and replace the set of basic marked basic terms accordingly.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, append#1^#(nil(), @l2) -> c_4()
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(leaf()) -> c_6()
, flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsort#1^#(nil()) -> c_16()
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#1^#(nil(), @x) -> c_12()
, insert#2^#(#false(), @x, @y, @ys) -> c_13()
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak DPs:
{ #cklt^#(#EQ()) -> c_29()
, #cklt^#(#GT()) -> c_30()
, #cklt^#(#LT()) -> c_31()
, #compare^#(#0(), #0()) -> c_17()
, #compare^#(#0(), #neg(@y)) -> c_18()
, #compare^#(#0(), #pos(@y)) -> c_19()
, #compare^#(#0(), #s(@y)) -> c_20()
, #compare^#(#neg(@x), #0()) -> c_21()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_23()
, #compare^#(#pos(@x), #0()) -> c_24()
, #compare^#(#pos(@x), #neg(@y)) -> c_25()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_27()
, #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the (estimated) dependency graph
1: #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
-->_2 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :31
-->_2 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :29
-->_2 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :25
-->_2 #compare^#(#s(@x), #0()) -> c_27() :30
-->_2 #compare^#(#pos(@x), #neg(@y)) -> c_25() :28
-->_2 #compare^#(#pos(@x), #0()) -> c_24() :27
-->_2 #compare^#(#neg(@x), #pos(@y)) -> c_23() :26
-->_2 #compare^#(#neg(@x), #0()) -> c_21() :24
-->_2 #compare^#(#0(), #s(@y)) -> c_20() :23
-->_2 #compare^#(#0(), #pos(@y)) -> c_19() :22
-->_2 #compare^#(#0(), #neg(@y)) -> c_18() :21
-->_2 #compare^#(#0(), #0()) -> c_17() :20
-->_1 #cklt^#(#LT()) -> c_31() :19
-->_1 #cklt^#(#GT()) -> c_30() :18
-->_1 #cklt^#(#EQ()) -> c_29() :17
2: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :3
-->_1 append#1^#(nil(), @l2) -> c_4() :4
3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :2
4: append#1^#(nil(), @l2) -> c_4()
5: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :7
-->_1 flatten#1^#(leaf()) -> c_6() :6
6: flatten#1^#(leaf()) -> c_6()
7: flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :5
-->_3 flatten^#(@t) -> flatten#1^#(@t) :5
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :2
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :2
8: flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :9
-->_2 flatten^#(@t) -> flatten#1^#(@t) :5
9: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :10
-->_1 insertionsort#1^#(nil()) -> c_16() :11
10: insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :12
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :9
11: insertionsort#1^#(nil()) -> c_16()
12: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :13
-->_1 insert#1^#(nil(), @x) -> c_12() :14
13: insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :16
-->_1 insert#2^#(#false(), @x, @y, @ys) -> c_13() :15
-->_2 #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) :1
14: insert#1^#(nil(), @x) -> c_12()
15: insert#2^#(#false(), @x, @y, @ys) -> c_13()
16: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :12
17: #cklt^#(#EQ()) -> c_29()
18: #cklt^#(#GT()) -> c_30()
19: #cklt^#(#LT()) -> c_31()
20: #compare^#(#0(), #0()) -> c_17()
21: #compare^#(#0(), #neg(@y)) -> c_18()
22: #compare^#(#0(), #pos(@y)) -> c_19()
23: #compare^#(#0(), #s(@y)) -> c_20()
24: #compare^#(#neg(@x), #0()) -> c_21()
25: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :31
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :29
-->_1 #compare^#(#s(@x), #0()) -> c_27() :30
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_25() :28
-->_1 #compare^#(#pos(@x), #0()) -> c_24() :27
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_23() :26
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :25
-->_1 #compare^#(#neg(@x), #0()) -> c_21() :24
-->_1 #compare^#(#0(), #s(@y)) -> c_20() :23
-->_1 #compare^#(#0(), #pos(@y)) -> c_19() :22
-->_1 #compare^#(#0(), #neg(@y)) -> c_18() :21
-->_1 #compare^#(#0(), #0()) -> c_17() :20
26: #compare^#(#neg(@x), #pos(@y)) -> c_23()
27: #compare^#(#pos(@x), #0()) -> c_24()
28: #compare^#(#pos(@x), #neg(@y)) -> c_25()
29: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :31
-->_1 #compare^#(#s(@x), #0()) -> c_27() :30
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :29
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_25() :28
-->_1 #compare^#(#pos(@x), #0()) -> c_24() :27
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_23() :26
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :25
-->_1 #compare^#(#neg(@x), #0()) -> c_21() :24
-->_1 #compare^#(#0(), #s(@y)) -> c_20() :23
-->_1 #compare^#(#0(), #pos(@y)) -> c_19() :22
-->_1 #compare^#(#0(), #neg(@y)) -> c_18() :21
-->_1 #compare^#(#0(), #0()) -> c_17() :20
30: #compare^#(#s(@x), #0()) -> c_27()
31: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :31
-->_1 #compare^#(#s(@x), #0()) -> c_27() :30
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :29
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_25() :28
-->_1 #compare^#(#pos(@x), #0()) -> c_24() :27
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_23() :26
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :25
-->_1 #compare^#(#neg(@x), #0()) -> c_21() :24
-->_1 #compare^#(#0(), #s(@y)) -> c_20() :23
-->_1 #compare^#(#0(), #pos(@y)) -> c_19() :22
-->_1 #compare^#(#0(), #neg(@y)) -> c_18() :21
-->_1 #compare^#(#0(), #0()) -> c_17() :20
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {11} and add Pre({11}) = {9} to the strict component.
- We remove {14} and add Pre({14}) = {12} to the strict component.
- We remove {15} and add Pre({15}) = {13} to the strict component.
- We remove {6} and add Pre({6}) = {5} to the strict component.
- We remove {4} and add Pre({4}) = {2} to the strict component.
- We remove {1} and add Pre({1}) = {13} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak DPs:
{ #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, #cklt^#(#EQ()) -> c_29()
, #cklt^#(#GT()) -> c_30()
, #cklt^#(#LT()) -> c_31()
, #compare^#(#0(), #0()) -> c_17()
, #compare^#(#0(), #neg(@y)) -> c_18()
, #compare^#(#0(), #pos(@y)) -> c_19()
, #compare^#(#0(), #s(@y)) -> c_20()
, #compare^#(#neg(@x), #0()) -> c_21()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_23()
, #compare^#(#pos(@x), #0()) -> c_24()
, #compare^#(#pos(@x), #neg(@y)) -> c_25()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_27()
, #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, append#1^#(nil(), @l2) -> c_4()
, flatten#1^#(leaf()) -> c_6()
, insertionsort#1^#(nil()) -> c_16()
, insert#1^#(nil(), @x) -> c_12()
, insert#2^#(#false(), @x, @y, @ys) -> c_13() }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the the dependency graph
->1:{5}
|
|->21:{3,4}
| |
| |->23:{1,2}
| | |
| | `->24:{27} Weak SCC
| |
| `->22:{28} Weak SCC
|
`->2:{6,7}
|
|->4:{8,10,9}
| |
| |->7:{11} Weak SCC
| | |
| | |->8:{12} Weak SCC
| | |
| | |->9:{13} Weak SCC
| | |
| | |->10:{14} Weak SCC
| | |
| | |->12:{15} Weak SCC
| | |
| | |->13:{16} Weak SCC
| | |
| | |->14:{17} Weak SCC
| | |
| | |->15:{18} Weak SCC
| | |
| | |->16:{19} Weak SCC
| | |
| | |->17:{21} Weak SCC
| | |
| | |->18:{22} Weak SCC
| | |
| | |->19:{23} Weak SCC
| | |
| | |->20:{25} Weak SCC
| | |
| | `->11:{26,24,20} Weak SCC
| | |
| | |->12:{15} Weak SCC
| | |
| | |->13:{16} Weak SCC
| | |
| | |->14:{17} Weak SCC
| | |
| | |->15:{18} Weak SCC
| | |
| | |->16:{19} Weak SCC
| | |
| | |->17:{21} Weak SCC
| | |
| | |->18:{22} Weak SCC
| | |
| | |->19:{23} Weak SCC
| | |
| | `->20:{25} Weak SCC
| |
| |->5:{30} Weak SCC
| |
| `->6:{31} Weak SCC
|
`->3:{29} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 3: flatten^#(@t) -> flatten#1^#(@t)
, 4: flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, 5: flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
, 6: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 7: insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, 8: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 9: insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, 10: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak DPs:
{ 11: #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, 12: #cklt^#(#EQ()) -> c_29()
, 13: #cklt^#(#GT()) -> c_30()
, 14: #cklt^#(#LT()) -> c_31()
, 15: #compare^#(#0(), #0()) -> c_17()
, 16: #compare^#(#0(), #neg(@y)) -> c_18()
, 17: #compare^#(#0(), #pos(@y)) -> c_19()
, 18: #compare^#(#0(), #s(@y)) -> c_20()
, 19: #compare^#(#neg(@x), #0()) -> c_21()
, 20: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, 21: #compare^#(#neg(@x), #pos(@y)) -> c_23()
, 22: #compare^#(#pos(@x), #0()) -> c_24()
, 23: #compare^#(#pos(@x), #neg(@y)) -> c_25()
, 24: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, 25: #compare^#(#s(@x), #0()) -> c_27()
, 26: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, 27: append#1^#(nil(), @l2) -> c_4()
, 28: flatten#1^#(leaf()) -> c_6()
, 29: insertionsort#1^#(nil()) -> c_16()
, 30: insert#1^#(nil(), @x) -> c_12()
, 31: insert#2^#(#false(), @x, @y, @ys) -> c_13() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 29: insertionsort#1^#(nil()) -> c_16()
, 30: insert#1^#(nil(), @x) -> c_12()
, 31: insert#2^#(#false(), @x, @y, @ys) -> c_13()
, 11: #less^#(@x, @y) ->
c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, 12: #cklt^#(#EQ()) -> c_29()
, 13: #cklt^#(#GT()) -> c_30()
, 14: #cklt^#(#LT()) -> c_31()
, 26: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, 24: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, 20: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, 15: #compare^#(#0(), #0()) -> c_17()
, 16: #compare^#(#0(), #neg(@y)) -> c_18()
, 17: #compare^#(#0(), #pos(@y)) -> c_19()
, 18: #compare^#(#0(), #s(@y)) -> c_20()
, 19: #compare^#(#neg(@x), #0()) -> c_21()
, 21: #compare^#(#neg(@x), #pos(@y)) -> c_23()
, 22: #compare^#(#pos(@x), #0()) -> c_24()
, 23: #compare^#(#pos(@x), #neg(@y)) -> c_25()
, 25: #compare^#(#s(@x), #0()) -> c_27()
, 28: flatten#1^#(leaf()) -> c_6()
, 27: append#1^#(nil(), @l2) -> c_4() }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the following dependency-graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :2
2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
3: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :4
4: flatten#1^#(node(@l, @t1, @t2)) ->
c_7(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :3
-->_3 flatten^#(@t) -> flatten#1^#(@t) :3
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: flattensort^#(@t) ->
c_8(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :6
-->_2 flatten^#(@t) -> flatten#1^#(@t) :3
6: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :7
7: insertionsort#1^#(::(@x, @xs)) ->
c_15(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :8
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :6
8: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :9
9: insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :10
10: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :8
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ insert#1^#(::(@y, @ys), @x) ->
c_11(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We employ 'linear path analysis' using the following approximated
dependency graph:
->1:{5} [ ? ]
|
|->4:{3,4} [ ? ]
| |
| `->5:{1,2} [ YES(O(1),O(n^2)) ]
|
`->2:{6,7} [ ? ]
|
`->3:{8,10,9} [ YES(O(1),O(n^2)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 3: flatten^#(@t) -> flatten#1^#(@t)
, 4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, 5: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, 6: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 7: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, 8: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 9: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, 10: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
* Path 1:{5}->4:{3,4}->5:{1,2}: YES(O(1),O(n^2))
----------------------------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :2
2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
3: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :4
4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :3
-->_3 flatten^#(@t) -> flatten#1^#(@t) :3
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_2 flatten^#(@t) -> flatten#1^#(@t) :3
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
Weak DPs: { append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :5
2: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :3
3: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :2
-->_3 flatten^#(@t) -> flatten#1^#(@t) :2
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
4: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_2 flatten^#(@t) -> flatten#1^#(@t) :2
5: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {2} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :4
2: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :5
3: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_2 flatten^#(@t) -> flatten#1^#(@t) :2
4: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :2
-->_3 flatten^#(@t) -> flatten#1^#(@t) :2
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, flatten^#(@t) -> flatten#1^#(@t) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the following dependency-graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :3
2: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :4
3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :2
-->_3 flatten^#(@t) -> flatten#1^#(@t) :2
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_2 flatten^#(@t) -> flatten#1^#(@t) :2
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, flatten^#(@t) -> flatten#1^#(@t) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) -> flatten^#(@t) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, flatten^#(@t) -> flatten#1^#(@t) }
Weak DPs:
{ append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) -> flatten^#(@t) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, 5: flattensort^#(@t) -> flatten^#(@t) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(append) = {}, Uargs(append#1) = {}, Uargs(::) = {},
Uargs(flatten) = {}, Uargs(flatten#1) = {}, Uargs(node) = {},
Uargs(#neg) = {}, Uargs(#pos) = {}, Uargs(#s) = {},
Uargs(#less^#) = {}, Uargs(#cklt^#) = {}, Uargs(#compare^#) = {},
Uargs(append^#) = {}, Uargs(append#1^#) = {},
Uargs(flatten^#) = {}, Uargs(flatten#1^#) = {},
Uargs(flattensort^#) = {}, Uargs(insertionsort^#) = {},
Uargs(insertionsort#1^#) = {}, Uargs(insert^#) = {},
Uargs(insert#1^#) = {}, Uargs(insert#2^#) = {},
Uargs(c_1) = {1, 2, 3, 4}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[append](x1, x2) = [0 0] x1 + [2 0] x2 + [0]
[0 1] [0 1] [0]
[append#1](x1, x2) = [0 0] x1 + [2 0] x2 + [0]
[0 1] [0 1] [0]
[::](x1, x2) = [1 0] x2 + [0]
[0 1] [2]
[nil] = [0]
[0]
[flatten](x1) = [0 0] x1 + [0]
[0 2] [0]
[flatten#1](x1) = [0 0] x1 + [0]
[0 2] [0]
[leaf] = [0]
[0]
[node](x1, x2, x3) = [0 3] x1 + [1 3] x2 + [1 0] x3 + [2]
[0 1] [0 1] [0 1] [0]
[#false] = [0]
[0]
[#true] = [0]
[0]
[#EQ] = [0]
[0]
[#GT] = [0]
[0]
[#LT] = [0]
[0]
[#0] = [0]
[0]
[#neg](x1) = [0]
[0]
[#pos](x1) = [0]
[0]
[#s](x1) = [1 1] x1 + [0]
[0 0] [0]
[#less^#](x1, x2) = [0]
[0]
[#cklt^#](x1) = [0]
[0]
[#compare^#](x1, x2) = [0]
[0]
[append^#](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[append#1^#](x1, x2) = [0 1] x1 + [0]
[0 0] [0]
[flatten^#](x1) = [1 0] x1 + [0]
[0 0] [1]
[flatten#1^#](x1) = [1 0] x1 + [0]
[0 0] [0]
[flattensort^#](x1) = [3 3] x1 + [3]
[3 3] [3]
[insertionsort^#](x1) = [0]
[0]
[insertionsort#1^#](x1) = [0]
[0]
[insert^#](x1, x2) = [0]
[0]
[insert#1^#](x1, x2) = [0]
[0]
[insert#2^#](x1, x2, x3, x4) = [0]
[0]
[c_1](x1, x2, x3, x4) = [2 1] x1 + [1 1] x2 + [1 0] x3 + [1
0] x4 + [1]
[0 0] [0 0] [0 0] [0
0] [0]
This order satisfies following ordering constraints
[append(@l1, @l2)] = [0 0] @l1 + [2 0] @l2 + [0]
[0 1] [0 1] [0]
>= [0 0] @l1 + [2 0] @l2 + [0]
[0 1] [0 1] [0]
= [append#1(@l1, @l2)]
[append#1(::(@x, @xs), @l2)] = [2 0] @l2 + [0 0] @xs + [0]
[0 1] [0 1] [2]
>= [2 0] @l2 + [0 0] @xs + [0]
[0 1] [0 1] [2]
= [::(@x, append(@xs, @l2))]
[append#1(nil(), @l2)] = [2 0] @l2 + [0]
[0 1] [0]
>= [1 0] @l2 + [0]
[0 1] [0]
= [@l2]
[flatten(@t)] = [0 0] @t + [0]
[0 2] [0]
>= [0 0] @t + [0]
[0 2] [0]
= [flatten#1(@t)]
[flatten#1(leaf())] = [0]
[0]
>= [0]
[0]
= [nil()]
[flatten#1(node(@l, @t1, @t2))] = [0 0] @l + [0 0] @t1 + [0 0] @t2 + [0]
[0 2] [0 2] [0 2] [0]
>= [0 0] @l + [0 0] @t1 + [0 0] @t2 + [0]
[0 1] [0 2] [0 2] [0]
= [append(@l, append(flatten(@t1), flatten(@t2)))]
[append^#(@l1, @l2)] = [0 1] @l1 + [0]
[0 0] [0]
>= [0 1] @l1 + [0]
[0 0] [0]
= [append#1^#(@l1, @l2)]
[append#1^#(::(@x, @xs), @l2)] = [0 1] @xs + [2]
[0 0] [0]
> [0 1] @xs + [0]
[0 0] [0]
= [append^#(@xs, @l2)]
[flatten^#(@t)] = [1 0] @t + [0]
[0 0] [1]
>= [1 0] @t + [0]
[0 0] [0]
= [flatten#1^#(@t)]
[flatten#1^#(node(@l, @t1, @t2))] = [0 3] @l + [1 3] @t1 + [1 0] @t2 + [2]
[0 0] [0 0] [0 0] [0]
> [0 2] @l + [1 2] @t1 + [1 0] @t2 + [1]
[0 0] [0 0] [0 0] [0]
= [c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))]
[flattensort^#(@t)] = [3 3] @t + [3]
[3 3] [3]
> [1 0] @t + [0]
[0 0] [1]
= [flatten^#(@t)]
Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^2)) on application of rules
{3,4,5}. Here rules are labeled according to the (estimated)
dependency graph
1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
-->_1 append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) :3
2: flatten^#(@t) -> flatten#1^#(@t)
-->_1 flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2)) :4
3: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
-->_4 flatten^#(@t) -> flatten#1^#(@t) :2
-->_3 flatten^#(@t) -> flatten#1^#(@t) :2
-->_2 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
-->_1 append^#(@l1, @l2) -> append#1^#(@l1, @l2) :1
5: flattensort^#(@t) -> flatten^#(@t)
-->_1 flatten^#(@t) -> flatten#1^#(@t) :2
- The rules {3,4,5} have known complexity. These cover all
predecessors of {1,2}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4,5} is given by YES(?,O(n^2)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, flatten^#(@t) -> flatten#1^#(@t)
, flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, flattensort^#(@t) -> flatten^#(@t) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{5} Weak SCC
|
`->2:{3,4} Weak SCC
|
`->3:{1,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2)
, 3: flatten^#(@t) -> flatten#1^#(@t)
, 4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, 5: flattensort^#(@t) -> flatten^#(@t) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 5: flattensort^#(@t) -> flatten^#(@t)
, 3: flatten^#(@t) -> flatten#1^#(@t)
, 4: flatten#1^#(node(@l, @t1, @t2)) ->
c_1(append^#(@l, append(flatten(@t1), flatten(@t2))),
append^#(flatten(@t1), flatten(@t2)),
flatten^#(@t1),
flatten^#(@t2))
, 1: append^#(@l1, @l2) -> append#1^#(@l1, @l2)
, 2: append#1^#(::(@x, @xs), @l2) -> append^#(@xs, @l2) }
We apply the transformation 'usablerules' on the sub-problem:
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
* Path 1:{5}->2:{6,7}->3:{8,10,9}: YES(O(1),O(n^2))
-------------------------------------------------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :3
3: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
4: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :5
5: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :6
6: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {6} and add Pre({6}) = {5} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) }
Weak DPs: { insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :3
3: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
4: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :5
5: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :6
6: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {5} and add Pre({5}) = {4} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :3
3: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
4: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :5
5: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :6
6: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :4
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {3} and add Pre({3}) = {2} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :4
3: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :5
4: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :3
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
5: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :6
6: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :3
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {1} and add Pre({1}) = {} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insertionsort^#(@l) -> insertionsort#1^#(@l)
, insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
, insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the following dependency-graph
1: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :4
2: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :5
3: flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
4: insertionsort#1^#(::(@x, @xs)) ->
c_3(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :2
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
5: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :6
6: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :2
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ flattensort^#(@t) ->
c_2(insertionsort^#(flatten(@t)), flatten^#(@t)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insertionsort^#(@l) -> insertionsort#1^#(@l)
, insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, flattensort(@t) -> insertionsort(flatten(@t))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insertionsort^#(@l) -> insertionsort#1^#(@l)
, insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We measure the number of applications of following selected rules
relative to the remaining rules.
Selected Rules (A):
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Remaining Rules (B):
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
The length of a single A-subderivation is expressed by the
following problem.
Problem (A):
------------
Strict DPs: { insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
The number of B-applications is expressed by the following problem.
Problem (B):
------------
Strict DPs:
{ insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak DPs: { flattensort^#(@t) -> insertionsort^#(flatten(@t)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
TcT answers on problem (B) YES(O(1),O(n^1)).
Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak DPs: { flattensort^#(@t) -> insertionsort^#(flatten(@t)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the (estimated) dependency graph
1: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :2
2: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
3: flattensort^#(@t) -> insertionsort^#(flatten(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { insertionsort^#(@l) -> insertionsort#1^#(@l) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We consider the following dependency-graph
1: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :3
2: flattensort^#(@t) -> insertionsort^#(flatten(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
3: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { insertionsort^#(@l) -> insertionsort#1^#(@l) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We replace strict/weak-rules by the corresponding usable rules:
Weak Usable Rules:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { insertionsort^#(@l) -> insertionsort#1^#(@l) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
Trs:
{ flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(#less) = {}, Uargs(#compare) = {}, Uargs(#cklt) = {},
Uargs(append) = {}, Uargs(append#1) = {}, Uargs(::) = {},
Uargs(flatten) = {}, Uargs(flatten#1) = {}, Uargs(node) = {},
Uargs(insertionsort) = {}, Uargs(insert) = {},
Uargs(insert#1) = {}, Uargs(insert#2) = {},
Uargs(insertionsort#1) = {}, Uargs(#neg) = {}, Uargs(#pos) = {},
Uargs(#s) = {}, Uargs(#less^#) = {}, Uargs(#cklt^#) = {},
Uargs(#compare^#) = {}, Uargs(append^#) = {},
Uargs(append#1^#) = {}, Uargs(flatten^#) = {},
Uargs(flatten#1^#) = {}, Uargs(flattensort^#) = {},
Uargs(insertionsort^#) = {}, Uargs(insertionsort#1^#) = {},
Uargs(insert^#) = {}, Uargs(insert#1^#) = {},
Uargs(insert#2^#) = {}, Uargs(c_1) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#less](x1, x2) = [0]
[#compare](x1, x2) = [0]
[#cklt](x1) = [0]
[append](x1, x2) = [1] x1 + [1] x2 + [0]
[append#1](x1, x2) = [1] x1 + [1] x2 + [0]
[::](x1, x2) = [1] x2 + [3]
[nil] = [0]
[flatten](x1) = [3] x1 + [0]
[flatten#1](x1) = [3] x1 + [0]
[leaf] = [0]
[node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [3]
[insertionsort](x1) = [0]
[insert](x1, x2) = [0]
[insert#1](x1, x2) = [0]
[insert#2](x1, x2, x3, x4) = [0]
[#false] = [0]
[#true] = [0]
[insertionsort#1](x1) = [0]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
[#0] = [0]
[#neg](x1) = [0]
[#pos](x1) = [0]
[#s](x1) = [0]
[#less^#](x1, x2) = [0]
[#cklt^#](x1) = [0]
[#compare^#](x1, x2) = [0]
[append^#](x1, x2) = [0]
[append#1^#](x1, x2) = [0]
[flatten^#](x1) = [0]
[flatten#1^#](x1) = [0]
[flattensort^#](x1) = [3] x1 + [3]
[insertionsort^#](x1) = [1] x1 + [3]
[insertionsort#1^#](x1) = [1] x1 + [3]
[insert^#](x1, x2) = [0]
[insert#1^#](x1, x2) = [0]
[insert#2^#](x1, x2, x3, x4) = [0]
[c_1](x1, x2) = [0]
[c] = [0]
This order satisfies following ordering constraints
[append(@l1, @l2)] = [1] @l1 + [1] @l2 + [0]
>= [1] @l1 + [1] @l2 + [0]
= [append#1(@l1, @l2)]
[append#1(::(@x, @xs), @l2)] = [1] @l2 + [1] @xs + [3]
>= [1] @l2 + [1] @xs + [3]
= [::(@x, append(@xs, @l2))]
[append#1(nil(), @l2)] = [1] @l2 + [0]
>= [1] @l2 + [0]
= [@l2]
[flatten(@t)] = [3] @t + [0]
>= [3] @t + [0]
= [flatten#1(@t)]
[flatten#1(leaf())] = [0]
>= [0]
= [nil()]
[flatten#1(node(@l, @t1, @t2))] = [3] @l + [3] @t1 + [3] @t2 + [9]
> [1] @l + [3] @t1 + [3] @t2 + [0]
= [append(@l, append(flatten(@t1), flatten(@t2)))]
[flattensort^#(@t)] = [3] @t + [3]
>= [3] @t + [3]
= [insertionsort^#(flatten(@t))]
[insertionsort^#(@l)] = [1] @l + [3]
>= [1] @l + [3]
= [insertionsort#1^#(@l)]
[insertionsort#1^#(::(@x, @xs))] = [1] @xs + [6]
> [1] @xs + [3]
= [insertionsort^#(@xs)]
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of rules {3}.
Here rules are labeled according to the (estimated) dependency
graph
1: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) :3
2: flattensort^#(@t) -> insertionsort^#(flatten(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :1
- The rules {3} have known complexity. These cover all predecessors
of {2}, their complexity is equally bounded.
- The rules {2,3} have known complexity. These cover all
predecessors of {1}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules {1,2,3}
is given by YES(?,O(n^1)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1} Weak SCC
|
`->2:{2,3} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: flattensort^#(@t) -> insertionsort^#(flatten(@t))
, 2: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 1: flattensort^#(@t) -> insertionsort^#(flatten(@t))
, 2: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) }
We apply the transformation 'usablerules' on the sub-problem:
Weak Trs:
{ append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2))) }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { insert^#(@x, @l) -> insert#1^#(@l, @x) }
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 2: flattensort^#(@t) -> insertionsort^#(flatten(@t))
, 4: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, 5: insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs)) }
Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, append#1(nil(), @l2) -> @l2
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertionsort#1(nil()) -> nil() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(#less) = {}, Uargs(#compare) = {}, Uargs(#cklt) = {},
Uargs(append) = {}, Uargs(append#1) = {}, Uargs(::) = {},
Uargs(flatten) = {}, Uargs(flatten#1) = {}, Uargs(node) = {},
Uargs(insertionsort) = {}, Uargs(insert) = {},
Uargs(insert#1) = {}, Uargs(insert#2) = {},
Uargs(insertionsort#1) = {}, Uargs(#neg) = {}, Uargs(#pos) = {},
Uargs(#s) = {}, Uargs(#less^#) = {}, Uargs(#cklt^#) = {},
Uargs(#compare^#) = {}, Uargs(append^#) = {},
Uargs(append#1^#) = {}, Uargs(flatten^#) = {},
Uargs(flatten#1^#) = {}, Uargs(flattensort^#) = {},
Uargs(insertionsort^#) = {}, Uargs(insertionsort#1^#) = {},
Uargs(insert^#) = {}, Uargs(insert#1^#) = {},
Uargs(insert#2^#) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#less](x1, x2) = [1]
[#compare](x1, x2) = [0]
[#cklt](x1) = [0]
[append](x1, x2) = [1] x1 + [1] x2 + [0]
[append#1](x1, x2) = [1] x1 + [1] x2 + [0]
[::](x1, x2) = [1] x2 + [1]
[nil] = [1]
[flatten](x1) = [1] x1 + [0]
[flatten#1](x1) = [1] x1 + [0]
[leaf] = [1]
[node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
[insertionsort](x1) = [2] x1 + [1]
[insert](x1, x2) = [1] x2 + [2]
[insert#1](x1, x2) = [1] x1 + [2]
[insert#2](x1, x2, x3, x4) = [1] x4 + [3]
[#false] = [0]
[#true] = [0]
[insertionsort#1](x1) = [2] x1 + [1]
[#EQ] = [0]
[#GT] = [0]
[#LT] = [0]
[#0] = [0]
[#neg](x1) = [1] x1 + [0]
[#pos](x1) = [1] x1 + [0]
[#s](x1) = [1] x1 + [0]
[#less^#](x1, x2) = [0]
[#cklt^#](x1) = [0]
[#compare^#](x1, x2) = [0]
[append^#](x1, x2) = [0]
[append#1^#](x1, x2) = [0]
[flatten^#](x1) = [0]
[flatten#1^#](x1) = [0]
[flattensort^#](x1) = [3] x1 + [3]
[insertionsort^#](x1) = [3] x1 + [2]
[insertionsort#1^#](x1) = [3] x1 + [2]
[insert^#](x1, x2) = [1] x2 + [3]
[insert#1^#](x1, x2) = [1] x1 + [2]
[insert#2^#](x1, x2, x3, x4) = [1] x4 + [3]
This order satisfies following ordering constraints
[#less(@x, @y)] = [1]
> [0]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [0]
>= [0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0]
>= [0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0]
>= [0]
= [#LT()]
[#compare(#0(), #s(@y))] = [0]
>= [0]
= [#LT()]
[#compare(#neg(@x), #0())] = [0]
>= [0]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0]
>= [0]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [0]
>= [0]
= [#LT()]
[#compare(#pos(@x), #0())] = [0]
>= [0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0]
>= [0]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [0]
>= [0]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [0]
>= [0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0]
>= [0]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [0]
>= [0]
= [#false()]
[#cklt(#GT())] = [0]
>= [0]
= [#false()]
[#cklt(#LT())] = [0]
>= [0]
= [#true()]
[append(@l1, @l2)] = [1] @l1 + [1] @l2 + [0]
>= [1] @l1 + [1] @l2 + [0]
= [append#1(@l1, @l2)]
[append#1(::(@x, @xs), @l2)] = [1] @l2 + [1] @xs + [1]
>= [1] @l2 + [1] @xs + [1]
= [::(@x, append(@xs, @l2))]
[append#1(nil(), @l2)] = [1] @l2 + [1]
> [1] @l2 + [0]
= [@l2]
[flatten(@t)] = [1] @t + [0]
>= [1] @t + [0]
= [flatten#1(@t)]
[flatten#1(leaf())] = [1]
>= [1]
= [nil()]
[flatten#1(node(@l, @t1, @t2))] = [1] @l + [1] @t1 + [1] @t2 + [1]
> [1] @l + [1] @t1 + [1] @t2 + [0]
= [append(@l, append(flatten(@t1), flatten(@t2)))]
[insertionsort(@l)] = [2] @l + [1]
>= [2] @l + [1]
= [insertionsort#1(@l)]
[insert(@x, @l)] = [1] @l + [2]
>= [1] @l + [2]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [1] @ys + [3]
>= [1] @ys + [3]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [3]
> [2]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [1] @ys + [3]
> [1] @ys + [2]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [1] @ys + [3]
>= [1] @ys + [3]
= [::(@y, insert(@x, @ys))]
[insertionsort#1(::(@x, @xs))] = [2] @xs + [3]
>= [2] @xs + [3]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [3]
> [1]
= [nil()]
[flattensort^#(@t)] = [3] @t + [3]
> [3] @t + [2]
= [insertionsort^#(flatten(@t))]
[insertionsort^#(@l)] = [3] @l + [2]
>= [3] @l + [2]
= [insertionsort#1^#(@l)]
[insertionsort#1^#(::(@x, @xs))] = [3] @xs + [5]
> [3] @xs + [2]
= [insertionsort^#(@xs)]
[insertionsort#1^#(::(@x, @xs))] = [3] @xs + [5]
> [2] @xs + [4]
= [insert^#(@x, insertionsort(@xs))]
[insert^#(@x, @l)] = [1] @l + [3]
> [1] @l + [2]
= [insert#1^#(@l, @x)]
[insert#1^#(::(@y, @ys), @x)] = [1] @ys + [3]
>= [1] @ys + [3]
= [insert#2^#(#less(@y, @x), @x, @y, @ys)]
[insert#2^#(#true(), @x, @y, @ys)] = [1] @ys + [3]
>= [1] @ys + [3]
= [insert^#(@x, @ys)]
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of rules
{1,2,4,5}. Here rules are labeled according to the (estimated)
dependency graph
1: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :6
2: flattensort^#(@t) -> insertionsort^#(flatten(@t))
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :3
3: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs)) :5
-->_1 insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs) :4
4: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
-->_1 insertionsort^#(@l) -> insertionsort#1^#(@l) :3
5: insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
6: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :7
7: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
- The rules {1,2,4,5} have known complexity. These cover all
predecessors of {3,6}, their complexity is equally bounded.
- The rules {1,2,3,4,5,6} have known complexity. These cover all
predecessors of {7}, their complexity is equally bounded.
Overall, we obtain that the number of applications of rules
{1,2,3,4,5,6,7} is given by YES(?,O(n^1)).
We apply the transformation 'removetails' on the sub-problem:
Weak DPs:
{ flattensort^#(@t) -> insertionsort^#(flatten(@t))
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{1} Weak SCC
|
`->2:{2,3} Weak SCC
|
`->3:{4} Weak SCC
|
`->4:{5,7,6} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: flattensort^#(@t) -> insertionsort^#(flatten(@t))
, 2: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, 4: insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
, 5: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 6: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, 7: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 1: flattensort^#(@t) -> insertionsort^#(flatten(@t))
, 2: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 3: insertionsort#1^#(::(@x, @xs)) -> insertionsort^#(@xs)
, 4: insertionsort#1^#(::(@x, @xs)) ->
insert^#(@x, insertionsort(@xs))
, 5: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 7: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 6: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) }
We apply the transformation 'usablerules' on the sub-problem:
Weak Trs:
{ #less(@x, @y) -> #cklt(#compare(@x, @y))
, #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
, #compare(#neg(@x), #pos(@y)) -> #LT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
, #compare(#s(@x), #0()) -> #GT()
, #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
, #cklt(#EQ()) -> #false()
, #cklt(#GT()) -> #false()
, #cklt(#LT()) -> #true()
, append(@l1, @l2) -> append#1(@l1, @l2)
, append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
, append#1(nil(), @l2) -> @l2
, flatten(@t) -> flatten#1(@t)
, flatten#1(leaf()) -> nil()
, flatten#1(node(@l, @t1, @t2)) ->
append(@l, append(flatten(@t1), flatten(@t2)))
, insertionsort(@l) -> insertionsort#1(@l)
, insert(@x, @l) -> insert#1(@l, @x)
, insert#1(::(@y, @ys), @x) -> insert#2(#less(@y, @x), @x, @y, @ys)
, insert#1(nil(), @x) -> ::(@x, nil())
, insert#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insert#2(#true(), @x, @y, @ys) -> ::(@y, insert(@x, @ys))
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
No rule is usable.
We apply the transformation 'trivial' on the sub-problem:
Rules: Empty
StartTerms: basic terms
Strategy: innermost
We consider the dependency graph
empty
All SCCs are trivial and dependency pairs can be removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^2))