tct
YES(?,O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#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:
{ #abs^#(#0()) -> c_1()
, #abs^#(#neg(@x)) -> c_2()
, #abs^#(#pos(@x)) -> c_3()
, #abs^#(#s(@x)) -> c_4()
, #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#1^#(nil(), @x) -> c_8()
, insert#2^#(#false(), @x, @y, @ys) -> c_9()
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insertD#1^#(nil(), @x) -> c_13()
, insertD#2^#(#false(), @x, @y, @ys) -> c_14()
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsort#1^#(nil()) -> c_18()
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
, insertionsortD#1^#(nil()) -> c_21() }
Weak DPs:
{ #cklt^#(#EQ()) -> c_34()
, #cklt^#(#GT()) -> c_35()
, #cklt^#(#LT()) -> c_36()
, #compare^#(#0(), #0()) -> c_22()
, #compare^#(#0(), #neg(@y)) -> c_23()
, #compare^#(#0(), #pos(@y)) -> c_24()
, #compare^#(#0(), #s(@y)) -> c_25()
, #compare^#(#neg(@x), #0()) -> c_26()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_28()
, #compare^#(#pos(@x), #0()) -> c_29()
, #compare^#(#pos(@x), #neg(@y)) -> c_30()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_32()
, #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:
{ #abs^#(#0()) -> c_1()
, #abs^#(#neg(@x)) -> c_2()
, #abs^#(#pos(@x)) -> c_3()
, #abs^#(#s(@x)) -> c_4()
, #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#1^#(nil(), @x) -> c_8()
, insert#2^#(#false(), @x, @y, @ys) -> c_9()
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insertD#1^#(nil(), @x) -> c_13()
, insertD#2^#(#false(), @x, @y, @ys) -> c_14()
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsort#1^#(nil()) -> c_18()
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
, insertionsortD#1^#(nil()) -> c_21() }
Weak DPs:
{ #cklt^#(#EQ()) -> c_34()
, #cklt^#(#GT()) -> c_35()
, #cklt^#(#LT()) -> c_36()
, #compare^#(#0(), #0()) -> c_22()
, #compare^#(#0(), #neg(@y)) -> c_23()
, #compare^#(#0(), #pos(@y)) -> c_24()
, #compare^#(#0(), #s(@y)) -> c_25()
, #compare^#(#neg(@x), #0()) -> c_26()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_28()
, #compare^#(#pos(@x), #0()) -> c_29()
, #compare^#(#pos(@x), #neg(@y)) -> c_30()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_32()
, #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the (estimated) dependency graph
1: #abs^#(#0()) -> c_1()
2: #abs^#(#neg(@x)) -> c_2()
3: #abs^#(#pos(@x)) -> c_3()
4: #abs^#(#s(@x)) -> c_4()
5: #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
-->_2 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :36
-->_2 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :34
-->_2 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :30
-->_2 #compare^#(#s(@x), #0()) -> c_32() :35
-->_2 #compare^#(#pos(@x), #neg(@y)) -> c_30() :33
-->_2 #compare^#(#pos(@x), #0()) -> c_29() :32
-->_2 #compare^#(#neg(@x), #pos(@y)) -> c_28() :31
-->_2 #compare^#(#neg(@x), #0()) -> c_26() :29
-->_2 #compare^#(#0(), #s(@y)) -> c_25() :28
-->_2 #compare^#(#0(), #pos(@y)) -> c_24() :27
-->_2 #compare^#(#0(), #neg(@y)) -> c_23() :26
-->_2 #compare^#(#0(), #0()) -> c_22() :25
-->_1 #cklt^#(#LT()) -> c_36() :24
-->_1 #cklt^#(#GT()) -> c_35() :23
-->_1 #cklt^#(#EQ()) -> c_34() :22
6: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :7
-->_1 insert#1^#(nil(), @x) -> c_8() :8
7: insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :10
-->_1 insert#2^#(#false(), @x, @y, @ys) -> c_9() :9
-->_2 #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) :5
8: insert#1^#(nil(), @x) -> c_8()
9: insert#2^#(#false(), @x, @y, @ys) -> c_9()
10: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :6
11: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :12
-->_1 insertD#1^#(nil(), @x) -> c_13() :13
12: insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :15
-->_1 insertD#2^#(#false(), @x, @y, @ys) -> c_14() :14
-->_2 #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) :5
13: insertD#1^#(nil(), @x) -> c_13()
14: insertD#2^#(#false(), @x, @y, @ys) -> c_14()
15: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :11
16: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :17
-->_1 insertionsort#1^#(nil()) -> c_18() :18
17: insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :16
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :6
18: insertionsort#1^#(nil()) -> c_18()
19: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :20
-->_1 insertionsortD#1^#(nil()) -> c_21() :21
20: insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :19
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :11
21: insertionsortD#1^#(nil()) -> c_21()
22: #cklt^#(#EQ()) -> c_34()
23: #cklt^#(#GT()) -> c_35()
24: #cklt^#(#LT()) -> c_36()
25: #compare^#(#0(), #0()) -> c_22()
26: #compare^#(#0(), #neg(@y)) -> c_23()
27: #compare^#(#0(), #pos(@y)) -> c_24()
28: #compare^#(#0(), #s(@y)) -> c_25()
29: #compare^#(#neg(@x), #0()) -> c_26()
30: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :36
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :34
-->_1 #compare^#(#s(@x), #0()) -> c_32() :35
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_30() :33
-->_1 #compare^#(#pos(@x), #0()) -> c_29() :32
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_28() :31
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :30
-->_1 #compare^#(#neg(@x), #0()) -> c_26() :29
-->_1 #compare^#(#0(), #s(@y)) -> c_25() :28
-->_1 #compare^#(#0(), #pos(@y)) -> c_24() :27
-->_1 #compare^#(#0(), #neg(@y)) -> c_23() :26
-->_1 #compare^#(#0(), #0()) -> c_22() :25
31: #compare^#(#neg(@x), #pos(@y)) -> c_28()
32: #compare^#(#pos(@x), #0()) -> c_29()
33: #compare^#(#pos(@x), #neg(@y)) -> c_30()
34: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :36
-->_1 #compare^#(#s(@x), #0()) -> c_32() :35
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :34
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_30() :33
-->_1 #compare^#(#pos(@x), #0()) -> c_29() :32
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_28() :31
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :30
-->_1 #compare^#(#neg(@x), #0()) -> c_26() :29
-->_1 #compare^#(#0(), #s(@y)) -> c_25() :28
-->_1 #compare^#(#0(), #pos(@y)) -> c_24() :27
-->_1 #compare^#(#0(), #neg(@y)) -> c_23() :26
-->_1 #compare^#(#0(), #0()) -> c_22() :25
35: #compare^#(#s(@x), #0()) -> c_32()
36: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :36
-->_1 #compare^#(#s(@x), #0()) -> c_32() :35
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :34
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_30() :33
-->_1 #compare^#(#pos(@x), #0()) -> c_29() :32
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_28() :31
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :30
-->_1 #compare^#(#neg(@x), #0()) -> c_26() :29
-->_1 #compare^#(#0(), #s(@y)) -> c_25() :28
-->_1 #compare^#(#0(), #pos(@y)) -> c_24() :27
-->_1 #compare^#(#0(), #neg(@y)) -> c_23() :26
-->_1 #compare^#(#0(), #0()) -> c_22() :25
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {21} and add Pre({21}) = {19} to the strict component.
- We remove {18} and add Pre({18}) = {16} to the strict component.
- We remove {13} and add Pre({13}) = {11} to the strict component.
- We remove {14} and add Pre({14}) = {12} to the strict component.
- We remove {8} and add Pre({8}) = {6} to the strict component.
- We remove {9} and add Pre({9}) = {7} to the strict component.
- We remove {5} and add Pre({5}) = {12,7} to the strict component.
- We remove {4} and add Pre({4}) = {} to the strict component.
- We remove {3} and add Pre({3}) = {} to the strict component.
- We remove {2} and add Pre({2}) = {} to the strict component.
- 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(n^2)).
Strict DPs:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak DPs:
{ #abs^#(#0()) -> c_1()
, #abs^#(#neg(@x)) -> c_2()
, #abs^#(#pos(@x)) -> c_3()
, #abs^#(#s(@x)) -> c_4()
, #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, #cklt^#(#EQ()) -> c_34()
, #cklt^#(#GT()) -> c_35()
, #cklt^#(#LT()) -> c_36()
, #compare^#(#0(), #0()) -> c_22()
, #compare^#(#0(), #neg(@y)) -> c_23()
, #compare^#(#0(), #pos(@y)) -> c_24()
, #compare^#(#0(), #s(@y)) -> c_25()
, #compare^#(#neg(@x), #0()) -> c_26()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_28()
, #compare^#(#pos(@x), #0()) -> c_29()
, #compare^#(#pos(@x), #neg(@y)) -> c_30()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_32()
, #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, insert#1^#(nil(), @x) -> c_8()
, insert#2^#(#false(), @x, @y, @ys) -> c_9()
, insertD#1^#(nil(), @x) -> c_13()
, insertD#2^#(#false(), @x, @y, @ys) -> c_14()
, insertionsort#1^#(nil()) -> c_18()
, insertionsortD#1^#(nil()) -> c_21() }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the the dependency graph
->7:{7,8}
|
|->12:{1,3,2}
| |
| |->15:{15} Weak SCC
| | |
| | |->16:{16} Weak SCC
| | |
| | |->17:{17} Weak SCC
| | |
| | |->18:{18} Weak SCC
| | |
| | |->20:{19} Weak SCC
| | |
| | |->21:{20} Weak SCC
| | |
| | |->22:{21} Weak SCC
| | |
| | |->23:{22} Weak SCC
| | |
| | |->24:{23} Weak SCC
| | |
| | |->25:{25} Weak SCC
| | |
| | |->26:{26} Weak SCC
| | |
| | |->27:{27} Weak SCC
| | |
| | |->28:{29} Weak SCC
| | |
| | `->19:{30,28,24} Weak SCC
| | |
| | |->20:{19} Weak SCC
| | |
| | |->21:{20} Weak SCC
| | |
| | |->22:{21} Weak SCC
| | |
| | |->23:{22} Weak SCC
| | |
| | |->24:{23} Weak SCC
| | |
| | |->25:{25} Weak SCC
| | |
| | |->26:{26} Weak SCC
| | |
| | |->27:{27} Weak SCC
| | |
| | `->28:{29} Weak SCC
| |
| |->13:{31} Weak SCC
| |
| `->14:{32} Weak SCC
|
`->8:{35} Weak SCC
->5:{9,10}
|
|->9:{4,6,5}
| |
| |->15:{15} Weak SCC
| | |
| | |->16:{16} Weak SCC
| | |
| | |->17:{17} Weak SCC
| | |
| | |->18:{18} Weak SCC
| | |
| | |->20:{19} Weak SCC
| | |
| | |->21:{20} Weak SCC
| | |
| | |->22:{21} Weak SCC
| | |
| | |->23:{22} Weak SCC
| | |
| | |->24:{23} Weak SCC
| | |
| | |->25:{25} Weak SCC
| | |
| | |->26:{26} Weak SCC
| | |
| | |->27:{27} Weak SCC
| | |
| | |->28:{29} Weak SCC
| | |
| | `->19:{30,28,24} Weak SCC
| | |
| | |->20:{19} Weak SCC
| | |
| | |->21:{20} Weak SCC
| | |
| | |->22:{21} Weak SCC
| | |
| | |->23:{22} Weak SCC
| | |
| | |->24:{23} Weak SCC
| | |
| | |->25:{25} Weak SCC
| | |
| | |->26:{26} Weak SCC
| | |
| | |->27:{27} Weak SCC
| | |
| | `->28:{29} Weak SCC
| |
| |->10:{33} Weak SCC
| |
| `->11:{34} Weak SCC
|
`->6:{36} Weak SCC
->4:{11} Weak SCC
->3:{12} Weak SCC
->2:{13} Weak SCC
->1:{14} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 2: insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, 3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 4: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, 5: insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, 6: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, 7: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 8: insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, 9: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, 10: insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak DPs:
{ 11: #abs^#(#0()) -> c_1()
, 12: #abs^#(#neg(@x)) -> c_2()
, 13: #abs^#(#pos(@x)) -> c_3()
, 14: #abs^#(#s(@x)) -> c_4()
, 15: #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, 16: #cklt^#(#EQ()) -> c_34()
, 17: #cklt^#(#GT()) -> c_35()
, 18: #cklt^#(#LT()) -> c_36()
, 19: #compare^#(#0(), #0()) -> c_22()
, 20: #compare^#(#0(), #neg(@y)) -> c_23()
, 21: #compare^#(#0(), #pos(@y)) -> c_24()
, 22: #compare^#(#0(), #s(@y)) -> c_25()
, 23: #compare^#(#neg(@x), #0()) -> c_26()
, 24: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, 25: #compare^#(#neg(@x), #pos(@y)) -> c_28()
, 26: #compare^#(#pos(@x), #0()) -> c_29()
, 27: #compare^#(#pos(@x), #neg(@y)) -> c_30()
, 28: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, 29: #compare^#(#s(@x), #0()) -> c_32()
, 30: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, 31: insert#1^#(nil(), @x) -> c_8()
, 32: insert#2^#(#false(), @x, @y, @ys) -> c_9()
, 33: insertD#1^#(nil(), @x) -> c_13()
, 34: insertD#2^#(#false(), @x, @y, @ys) -> c_14()
, 35: insertionsort#1^#(nil()) -> c_18()
, 36: insertionsortD#1^#(nil()) -> c_21() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 14: #abs^#(#s(@x)) -> c_4()
, 13: #abs^#(#pos(@x)) -> c_3()
, 12: #abs^#(#neg(@x)) -> c_2()
, 11: #abs^#(#0()) -> c_1()
, 36: insertionsortD#1^#(nil()) -> c_21()
, 35: insertionsort#1^#(nil()) -> c_18()
, 33: insertD#1^#(nil(), @x) -> c_13()
, 34: insertD#2^#(#false(), @x, @y, @ys) -> c_14()
, 31: insert#1^#(nil(), @x) -> c_8()
, 32: insert#2^#(#false(), @x, @y, @ys) -> c_9()
, 15: #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, 16: #cklt^#(#EQ()) -> c_34()
, 17: #cklt^#(#GT()) -> c_35()
, 18: #cklt^#(#LT()) -> c_36()
, 30: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, 28: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, 24: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, 19: #compare^#(#0(), #0()) -> c_22()
, 20: #compare^#(#0(), #neg(@y)) -> c_23()
, 21: #compare^#(#0(), #pos(@y)) -> c_24()
, 22: #compare^#(#0(), #s(@y)) -> c_25()
, 23: #compare^#(#neg(@x), #0()) -> c_26()
, 25: #compare^#(#neg(@x), #pos(@y)) -> c_28()
, 26: #compare^#(#pos(@x), #0()) -> c_29()
, 27: #compare^#(#pos(@x), #neg(@y)) -> c_30()
, 29: #compare^#(#s(@x), #0()) -> c_32() }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the following dependency-graph
1: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :2
2: insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :3
3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
4: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :5
5: insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :6
6: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :4
7: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :8
8: insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :7
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
9: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :10
10: insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :9
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :4
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#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:
{ 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)
, insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We employ 'linear path analysis' using the following approximated
dependency graph:
->2:{7,8} [ ? ]
|
`->4:{1,3,2} [ YES(O(1),O(n^2)) ]
->1:{9,10} [ ? ]
|
`->3:{4,6,5} [ YES(O(1),O(n^2)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 2: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, 3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 4: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, 5: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, 6: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, 7: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 8: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, 9: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, 10: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
* Path 2:{7,8}->4:{1,3,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:
{ 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)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider 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) :2
2: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :3
3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
4: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :5
5: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :4
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :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:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak DPs: { insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider 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) :2
2: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :5
3: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :4
4: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :3
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
5: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :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^2)).
Strict DPs:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
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:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider 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) :4
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :3
3: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
4: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :5
5: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :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:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insertionsort^#(@l) -> insertionsort#1^#(@l) }
Weak DPs:
{ insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#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()
, 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(@l) -> insertionsort#1(@l)
, 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:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insertionsort^#(@l) -> insertionsort#1^#(@l) }
Weak DPs:
{ insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 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()
, 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(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
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: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, 4: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 5: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Trs:
{ #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#s(@x), #0()) -> #GT()
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(#neg) = {}, Uargs(#pos) = {}, Uargs(#s) = {},
Uargs(#less) = {}, Uargs(#compare) = {}, Uargs(#cklt) = {},
Uargs(insert) = {}, Uargs(insert#1) = {}, Uargs(::) = {},
Uargs(insert#2) = {}, Uargs(insertionsort) = {},
Uargs(insertionsort#1) = {}, Uargs(#abs^#) = {},
Uargs(#less^#) = {}, Uargs(#cklt^#) = {}, Uargs(#compare^#) = {},
Uargs(insert^#) = {}, Uargs(insert#1^#) = {},
Uargs(insert#2^#) = {}, Uargs(insertD^#) = {},
Uargs(insertD#1^#) = {}, Uargs(insertD#2^#) = {},
Uargs(insertionsort^#) = {}, Uargs(insertionsort#1^#) = {},
Uargs(insertionsortD^#) = {}, Uargs(insertionsortD#1^#) = {},
Uargs(c_1) = {1, 2}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [2]
[0]
[#neg](x1) = [1 0] x1 + [1]
[1 1] [2]
[#pos](x1) = [1 0] x1 + [0]
[0 1] [2]
[#s](x1) = [1 0] x1 + [0]
[0 1] [2]
[#less](x1, x2) = [1]
[1]
[#compare](x1, x2) = [0 0] x1 + [0 0] x2 + [2]
[2 0] [2 0] [0]
[#cklt](x1) = [1]
[1]
[insert](x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[1 0] [1 1] [3]
[insert#1](x1, x2) = [1 0] x1 + [0 0] x2 + [2]
[1 1] [1 0] [3]
[::](x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[1 0] [1 1] [2]
[insert#2](x1, x2, x3, x4) = [2 2] x1 + [0 0] x2 + [0 0] x3 + [1
0] x4 + [0]
[1 3] [1 0] [1 0] [2
1] [3]
[nil] = [0]
[3]
[#false] = [1]
[1]
[#true] = [1]
[1]
[insertionsort](x1) = [2 0] x1 + [2]
[3 3] [3]
[insertionsort#1](x1) = [2 0] x1 + [2]
[3 3] [2]
[#EQ] = [0]
[0]
[#GT] = [0]
[0]
[#LT] = [2]
[2]
[#abs^#](x1) = [0]
[0]
[#less^#](x1, x2) = [0]
[0]
[#cklt^#](x1) = [0]
[0]
[#compare^#](x1, x2) = [0]
[0]
[insert^#](x1, x2) = [2 0] x1 + [1 0] x2 + [3]
[0 0] [0 0] [2]
[insert#1^#](x1, x2) = [1 0] x1 + [2 0] x2 + [3]
[0 0] [0 0] [2]
[insert#2^#](x1, x2, x3, x4) = [2 2] x1 + [2 0] x2 + [1
0] x4 + [0]
[0 1] [0 0] [0
0] [1]
[insertD^#](x1, x2) = [0]
[0]
[insertD#1^#](x1, x2) = [0]
[0]
[insertD#2^#](x1, x2, x3, x4) = [0]
[0]
[insertionsort^#](x1) = [3 3] x1 + [2]
[0 0] [1]
[insertionsort#1^#](x1) = [3 3] x1 + [2]
[0 0] [0]
[insertionsortD^#](x1) = [0]
[0]
[insertionsortD#1^#](x1) = [0]
[0]
[c_1](x1, x2) = [1 1] x1 + [1 3] x2 + [1]
[0 0] [0 0] [0]
This order satisfies following ordering constraints
[#less(@x, @y)] = [1]
[1]
>= [1]
[1]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [2]
[8]
> [0]
[0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0 0] @y + [2]
[2 0] [6]
> [0]
[0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0 0] @y + [2]
[2 0] [4]
>= [2]
[2]
= [#LT()]
[#compare(#0(), #s(@y))] = [0 0] @y + [2]
[2 0] [4]
>= [2]
[2]
= [#LT()]
[#compare(#neg(@x), #0())] = [0 0] @x + [2]
[2 0] [6]
>= [2]
[2]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [4]
>= [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [0]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [2]
>= [2]
[2]
= [#LT()]
[#compare(#pos(@x), #0())] = [0 0] @x + [2]
[2 0] [4]
> [0]
[0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [2]
> [0]
[0]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [0]
>= [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [0]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [0 0] @x + [2]
[2 0] [4]
> [0]
[0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [0]
>= [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [0]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [1]
[1]
>= [1]
[1]
= [#false()]
[#cklt(#GT())] = [1]
[1]
>= [1]
[1]
= [#false()]
[#cklt(#LT())] = [1]
[1]
>= [1]
[1]
= [#true()]
[insert(@x, @l)] = [1 0] @l + [0 0] @x + [2]
[1 1] [1 0] [3]
>= [1 0] @l + [0 0] @x + [2]
[1 1] [1 0] [3]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [7]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [7]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [0 0] @x + [2]
[1 0] [6]
>= [0 0] @x + [2]
[1 0] [5]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [7]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [7]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [7]
= [::(@y, insert(@x, @ys))]
[insertionsort(@l)] = [2 0] @l + [2]
[3 3] [3]
>= [2 0] @l + [2]
[3 3] [2]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [0 0] @x + [2 0] @xs + [6]
[3 0] [6 3] [14]
> [0 0] @x + [2 0] @xs + [4]
[1 0] [5 3] [8]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [2]
[11]
> [0]
[3]
= [nil()]
[insert^#(@x, @l)] = [1 0] @l + [2 0] @x + [3]
[0 0] [0 0] [2]
>= [1 0] @l + [2 0] @x + [3]
[0 0] [0 0] [2]
= [insert#1^#(@l, @x)]
[insert#1^#(::(@y, @ys), @x)] = [2 0] @x + [1 0] @ys + [5]
[0 0] [0 0] [2]
> [2 0] @x + [1 0] @ys + [4]
[0 0] [0 0] [2]
= [insert#2^#(#less(@y, @x), @x, @y, @ys)]
[insert#2^#(#true(), @x, @y, @ys)] = [2 0] @x + [1 0] @ys + [4]
[0 0] [0 0] [2]
> [2 0] @x + [1 0] @ys + [3]
[0 0] [0 0] [2]
= [insert^#(@x, @ys)]
[insertionsort^#(@l)] = [3 3] @l + [2]
[0 0] [1]
>= [3 3] @l + [2]
[0 0] [0]
= [insertionsort#1^#(@l)]
[insertionsort#1^#(::(@x, @xs))] = [3 0] @x + [6 3] @xs + [14]
[0 0] [0 0] [0]
> [2 0] @x + [5 3] @xs + [13]
[0 0] [0 0] [0]
= [c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))]
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: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :3
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :5
3: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :4
4: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
5: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
- 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:
{ 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)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, 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()
, 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(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{4,5} Weak SCC
|
`->2:{1,3,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 2: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, 3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 4: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 5: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 4: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 5: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, 1: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 2: 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()
, 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(@l) -> insertionsort#1(@l)
, 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
* Path 1:{9,10}->3:{4,6,5}: 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:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys) :2
2: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :3
3: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :1
4: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :5
5: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :4
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :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:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak DPs:
{ insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys) :2
2: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :5
3: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :4
4: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :3
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :1
5: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :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^2)).
Strict DPs:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak DPs:
{ insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys) :4
2: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :3
3: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :2
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :1
4: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :5
5: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :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:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l) }
Weak DPs:
{ insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#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()
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l) }
Weak DPs:
{ insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@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()
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
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:
{ 2: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, 4: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) }
Trs:
{ #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, insertionsortD#1(nil()) -> nil() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(#neg) = {}, Uargs(#pos) = {}, Uargs(#s) = {},
Uargs(#less) = {}, Uargs(#compare) = {}, Uargs(#cklt) = {},
Uargs(::) = {}, Uargs(insertD) = {}, Uargs(insertD#1) = {},
Uargs(insertD#2) = {}, Uargs(insertionsortD) = {},
Uargs(insertionsortD#1) = {}, Uargs(#abs^#) = {},
Uargs(#less^#) = {}, Uargs(#cklt^#) = {}, Uargs(#compare^#) = {},
Uargs(insert^#) = {}, Uargs(insert#1^#) = {},
Uargs(insert#2^#) = {}, Uargs(insertD^#) = {},
Uargs(insertD#1^#) = {}, Uargs(insertD#2^#) = {},
Uargs(insertionsort^#) = {}, Uargs(insertionsort#1^#) = {},
Uargs(insertionsortD^#) = {}, Uargs(insertionsortD#1^#) = {},
Uargs(c_2) = {1, 2}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [0]
[0]
[#neg](x1) = [0 0] x1 + [3]
[1 1] [0]
[#pos](x1) = [1 0] x1 + [0]
[0 1] [2]
[#s](x1) = [1 0] x1 + [0]
[0 1] [2]
[#less](x1, x2) = [0]
[1]
[#compare](x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[1 2] [1 2] [0]
[#cklt](x1) = [0]
[1]
[::](x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[1 0] [1 1] [2]
[nil] = [1]
[0]
[#false] = [0]
[1]
[#true] = [0]
[1]
[insertD](x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[1 0] [1 1] [2]
[insertD#1](x1, x2) = [1 0] x1 + [0 0] x2 + [2]
[1 1] [1 0] [2]
[insertD#2](x1, x2, x3, x4) = [0 2] x1 + [0 0] x2 + [0 0] x3 + [1
0] x4 + [2]
[2 3] [1 0] [1 0] [2
1] [3]
[insertionsortD](x1) = [1 0] x1 + [1]
[3 1] [3]
[insertionsortD#1](x1) = [1 0] x1 + [1]
[3 1] [2]
[#EQ] = [0]
[0]
[#GT] = [1]
[0]
[#LT] = [0]
[3]
[#abs^#](x1) = [0]
[0]
[#less^#](x1, x2) = [0]
[0]
[#cklt^#](x1) = [0]
[0]
[#compare^#](x1, x2) = [0]
[0]
[insert^#](x1, x2) = [0]
[0]
[insert#1^#](x1, x2) = [0]
[0]
[insert#2^#](x1, x2, x3, x4) = [0]
[0]
[insertD^#](x1, x2) = [2 0] x2 + [0]
[0 0] [3]
[insertD#1^#](x1, x2) = [2 0] x1 + [0]
[0 0] [3]
[insertD#2^#](x1, x2, x3, x4) = [3 2] x1 + [2 0] x4 + [2]
[0 2] [0 0] [1]
[insertionsort^#](x1) = [0]
[0]
[insertionsort#1^#](x1) = [0]
[0]
[insertionsortD^#](x1) = [3 3] x1 + [2]
[0 1] [1]
[insertionsortD#1^#](x1) = [2 3] x1 + [0]
[0 0] [0]
[c_2](x1, x2) = [1 2] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
This order satisfies following ordering constraints
[#less(@x, @y)] = [0]
[1]
>= [0]
[1]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [1]
[0]
> [0]
[0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0 0] @y + [1]
[2 2] [3]
>= [1]
[0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0 0] @y + [1]
[1 2] [4]
> [0]
[3]
= [#LT()]
[#compare(#0(), #s(@y))] = [0 0] @y + [1]
[1 2] [4]
> [0]
[3]
= [#LT()]
[#compare(#neg(@x), #0())] = [0 0] @x + [1]
[2 2] [3]
> [0]
[3]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0 0] @x + [0 0] @y + [1]
[2 2] [2 2] [6]
>= [0 0] @x + [0 0] @y + [1]
[1 2] [1 2] [0]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [0 0] @x + [0 0] @y + [1]
[2 2] [1 2] [7]
> [0]
[3]
= [#LT()]
[#compare(#pos(@x), #0())] = [0 0] @x + [1]
[1 2] [4]
>= [1]
[0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0 0] @x + [0 0] @y + [1]
[1 2] [2 2] [7]
>= [1]
[0]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [0 0] @x + [0 0] @y + [1]
[1 2] [1 2] [8]
>= [0 0] @x + [0 0] @y + [1]
[1 2] [1 2] [0]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [0 0] @x + [1]
[1 2] [4]
>= [1]
[0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0 0] @x + [0 0] @y + [1]
[1 2] [1 2] [8]
>= [0 0] @x + [0 0] @y + [1]
[1 2] [1 2] [0]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [0]
[1]
>= [0]
[1]
= [#false()]
[#cklt(#GT())] = [0]
[1]
>= [0]
[1]
= [#false()]
[#cklt(#LT())] = [0]
[1]
>= [0]
[1]
= [#true()]
[insertD(@x, @l)] = [1 0] @l + [0 0] @x + [2]
[1 1] [1 0] [2]
>= [1 0] @l + [0 0] @x + [2]
[1 1] [1 0] [2]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [0 0] @x + [3]
[1 0] [3]
>= [0 0] @x + [3]
[1 0] [3]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
= [::(@y, insertD(@x, @ys))]
[insertionsortD(@l)] = [1 0] @l + [1]
[3 1] [3]
>= [1 0] @l + [1]
[3 1] [2]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [0 0] @x + [1 0] @xs + [3]
[1 0] [4 1] [10]
>= [0 0] @x + [1 0] @xs + [3]
[1 0] [4 1] [6]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [2]
[5]
> [1]
[0]
= [nil()]
[insertD^#(@x, @l)] = [2 0] @l + [0]
[0 0] [3]
>= [2 0] @l + [0]
[0 0] [3]
= [insertD#1^#(@l, @x)]
[insertD#1^#(::(@y, @ys), @x)] = [2 0] @ys + [4]
[0 0] [3]
>= [2 0] @ys + [4]
[0 0] [3]
= [insertD#2^#(#less(@y, @x), @x, @y, @ys)]
[insertD#2^#(#true(), @x, @y, @ys)] = [2 0] @ys + [4]
[0 0] [3]
> [2 0] @ys + [0]
[0 0] [3]
= [insertD^#(@x, @ys)]
[insertionsortD^#(@l)] = [3 3] @l + [2]
[0 1] [1]
> [2 3] @l + [0]
[0 0] [0]
= [insertionsortD#1^#(@l)]
[insertionsortD#1^#(::(@x, @xs))] = [3 0] @x + [5 3] @xs + [10]
[0 0] [0 0] [0]
>= [5 3] @xs + [10]
[0 0] [0]
= [c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))]
Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^2)) on application of rules {2,4}.
Here rules are labeled according to the (estimated) dependency
graph
1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys) :3
2: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :5
3: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :4
4: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :1
5: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :2
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :1
- The rules {2,4} have known complexity. These cover all
predecessors of {5}, their complexity is equally bounded.
- The rules {2,4,5} have known complexity. These cover all
predecessors of {1}, their complexity is equally bounded.
- The rules {1,2,4,5} have known complexity. These cover all
predecessors of {3}, 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:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@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()
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{4,5} Weak SCC
|
`->2:{1,3,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, 2: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, 3: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, 4: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, 5: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 4: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, 5: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
, 1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, 3: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, 2: insertD#1^#(::(@y, @ys), @x) ->
insertD#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()
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#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
YES(?,O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #less(@x, @y) -> #cklt(#compare(@x, @y))
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#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:
{ #abs^#(#0()) -> c_1()
, #abs^#(#neg(@x)) -> c_2()
, #abs^#(#pos(@x)) -> c_3()
, #abs^#(#s(@x)) -> c_4()
, #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#1^#(nil(), @x) -> c_8()
, insert#2^#(#false(), @x, @y, @ys) -> c_9()
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insertD#1^#(nil(), @x) -> c_13()
, insertD#2^#(#false(), @x, @y, @ys) -> c_14()
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsort#1^#(nil()) -> c_18()
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
, insertionsortD#1^#(nil()) -> c_21() }
Weak DPs:
{ #cklt^#(#EQ()) -> c_34()
, #cklt^#(#GT()) -> c_35()
, #cklt^#(#LT()) -> c_36()
, #compare^#(#0(), #0()) -> c_22()
, #compare^#(#0(), #neg(@y)) -> c_23()
, #compare^#(#0(), #pos(@y)) -> c_24()
, #compare^#(#0(), #s(@y)) -> c_25()
, #compare^#(#neg(@x), #0()) -> c_26()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_28()
, #compare^#(#pos(@x), #0()) -> c_29()
, #compare^#(#pos(@x), #neg(@y)) -> c_30()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_32()
, #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:
{ #abs^#(#0()) -> c_1()
, #abs^#(#neg(@x)) -> c_2()
, #abs^#(#pos(@x)) -> c_3()
, #abs^#(#s(@x)) -> c_4()
, #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#1^#(nil(), @x) -> c_8()
, insert#2^#(#false(), @x, @y, @ys) -> c_9()
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insertD#1^#(nil(), @x) -> c_13()
, insertD#2^#(#false(), @x, @y, @ys) -> c_14()
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsort#1^#(nil()) -> c_18()
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
, insertionsortD#1^#(nil()) -> c_21() }
Weak DPs:
{ #cklt^#(#EQ()) -> c_34()
, #cklt^#(#GT()) -> c_35()
, #cklt^#(#LT()) -> c_36()
, #compare^#(#0(), #0()) -> c_22()
, #compare^#(#0(), #neg(@y)) -> c_23()
, #compare^#(#0(), #pos(@y)) -> c_24()
, #compare^#(#0(), #s(@y)) -> c_25()
, #compare^#(#neg(@x), #0()) -> c_26()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_28()
, #compare^#(#pos(@x), #0()) -> c_29()
, #compare^#(#pos(@x), #neg(@y)) -> c_30()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_32()
, #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the (estimated) dependency graph
1: #abs^#(#0()) -> c_1()
2: #abs^#(#neg(@x)) -> c_2()
3: #abs^#(#pos(@x)) -> c_3()
4: #abs^#(#s(@x)) -> c_4()
5: #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
-->_2 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :36
-->_2 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :34
-->_2 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :30
-->_2 #compare^#(#s(@x), #0()) -> c_32() :35
-->_2 #compare^#(#pos(@x), #neg(@y)) -> c_30() :33
-->_2 #compare^#(#pos(@x), #0()) -> c_29() :32
-->_2 #compare^#(#neg(@x), #pos(@y)) -> c_28() :31
-->_2 #compare^#(#neg(@x), #0()) -> c_26() :29
-->_2 #compare^#(#0(), #s(@y)) -> c_25() :28
-->_2 #compare^#(#0(), #pos(@y)) -> c_24() :27
-->_2 #compare^#(#0(), #neg(@y)) -> c_23() :26
-->_2 #compare^#(#0(), #0()) -> c_22() :25
-->_1 #cklt^#(#LT()) -> c_36() :24
-->_1 #cklt^#(#GT()) -> c_35() :23
-->_1 #cklt^#(#EQ()) -> c_34() :22
6: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :7
-->_1 insert#1^#(nil(), @x) -> c_8() :8
7: insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :10
-->_1 insert#2^#(#false(), @x, @y, @ys) -> c_9() :9
-->_2 #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) :5
8: insert#1^#(nil(), @x) -> c_8()
9: insert#2^#(#false(), @x, @y, @ys) -> c_9()
10: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :6
11: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :12
-->_1 insertD#1^#(nil(), @x) -> c_13() :13
12: insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :15
-->_1 insertD#2^#(#false(), @x, @y, @ys) -> c_14() :14
-->_2 #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) :5
13: insertD#1^#(nil(), @x) -> c_13()
14: insertD#2^#(#false(), @x, @y, @ys) -> c_14()
15: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :11
16: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :17
-->_1 insertionsort#1^#(nil()) -> c_18() :18
17: insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :16
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :6
18: insertionsort#1^#(nil()) -> c_18()
19: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :20
-->_1 insertionsortD#1^#(nil()) -> c_21() :21
20: insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :19
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :11
21: insertionsortD#1^#(nil()) -> c_21()
22: #cklt^#(#EQ()) -> c_34()
23: #cklt^#(#GT()) -> c_35()
24: #cklt^#(#LT()) -> c_36()
25: #compare^#(#0(), #0()) -> c_22()
26: #compare^#(#0(), #neg(@y)) -> c_23()
27: #compare^#(#0(), #pos(@y)) -> c_24()
28: #compare^#(#0(), #s(@y)) -> c_25()
29: #compare^#(#neg(@x), #0()) -> c_26()
30: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :36
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :34
-->_1 #compare^#(#s(@x), #0()) -> c_32() :35
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_30() :33
-->_1 #compare^#(#pos(@x), #0()) -> c_29() :32
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_28() :31
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :30
-->_1 #compare^#(#neg(@x), #0()) -> c_26() :29
-->_1 #compare^#(#0(), #s(@y)) -> c_25() :28
-->_1 #compare^#(#0(), #pos(@y)) -> c_24() :27
-->_1 #compare^#(#0(), #neg(@y)) -> c_23() :26
-->_1 #compare^#(#0(), #0()) -> c_22() :25
31: #compare^#(#neg(@x), #pos(@y)) -> c_28()
32: #compare^#(#pos(@x), #0()) -> c_29()
33: #compare^#(#pos(@x), #neg(@y)) -> c_30()
34: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :36
-->_1 #compare^#(#s(@x), #0()) -> c_32() :35
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :34
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_30() :33
-->_1 #compare^#(#pos(@x), #0()) -> c_29() :32
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_28() :31
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :30
-->_1 #compare^#(#neg(@x), #0()) -> c_26() :29
-->_1 #compare^#(#0(), #s(@y)) -> c_25() :28
-->_1 #compare^#(#0(), #pos(@y)) -> c_24() :27
-->_1 #compare^#(#0(), #neg(@y)) -> c_23() :26
-->_1 #compare^#(#0(), #0()) -> c_22() :25
35: #compare^#(#s(@x), #0()) -> c_32()
36: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
-->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :36
-->_1 #compare^#(#s(@x), #0()) -> c_32() :35
-->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :34
-->_1 #compare^#(#pos(@x), #neg(@y)) -> c_30() :33
-->_1 #compare^#(#pos(@x), #0()) -> c_29() :32
-->_1 #compare^#(#neg(@x), #pos(@y)) -> c_28() :31
-->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :30
-->_1 #compare^#(#neg(@x), #0()) -> c_26() :29
-->_1 #compare^#(#0(), #s(@y)) -> c_25() :28
-->_1 #compare^#(#0(), #pos(@y)) -> c_24() :27
-->_1 #compare^#(#0(), #neg(@y)) -> c_23() :26
-->_1 #compare^#(#0(), #0()) -> c_22() :25
We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {21} and add Pre({21}) = {19} to the strict component.
- We remove {18} and add Pre({18}) = {16} to the strict component.
- We remove {13} and add Pre({13}) = {11} to the strict component.
- We remove {14} and add Pre({14}) = {12} to the strict component.
- We remove {8} and add Pre({8}) = {6} to the strict component.
- We remove {9} and add Pre({9}) = {7} to the strict component.
- We remove {5} and add Pre({5}) = {12,7} to the strict component.
- We remove {4} and add Pre({4}) = {} to the strict component.
- We remove {3} and add Pre({3}) = {} to the strict component.
- We remove {2} and add Pre({2}) = {} to the strict component.
- 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(n^2)).
Strict DPs:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak DPs:
{ #abs^#(#0()) -> c_1()
, #abs^#(#neg(@x)) -> c_2()
, #abs^#(#pos(@x)) -> c_3()
, #abs^#(#s(@x)) -> c_4()
, #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, #cklt^#(#EQ()) -> c_34()
, #cklt^#(#GT()) -> c_35()
, #cklt^#(#LT()) -> c_36()
, #compare^#(#0(), #0()) -> c_22()
, #compare^#(#0(), #neg(@y)) -> c_23()
, #compare^#(#0(), #pos(@y)) -> c_24()
, #compare^#(#0(), #s(@y)) -> c_25()
, #compare^#(#neg(@x), #0()) -> c_26()
, #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, #compare^#(#neg(@x), #pos(@y)) -> c_28()
, #compare^#(#pos(@x), #0()) -> c_29()
, #compare^#(#pos(@x), #neg(@y)) -> c_30()
, #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, #compare^#(#s(@x), #0()) -> c_32()
, #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, insert#1^#(nil(), @x) -> c_8()
, insert#2^#(#false(), @x, @y, @ys) -> c_9()
, insertD#1^#(nil(), @x) -> c_13()
, insertD#2^#(#false(), @x, @y, @ys) -> c_14()
, insertionsort#1^#(nil()) -> c_18()
, insertionsortD#1^#(nil()) -> c_21() }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the the dependency graph
->7:{7,8}
|
|->12:{1,3,2}
| |
| |->15:{15} Weak SCC
| | |
| | |->16:{16} Weak SCC
| | |
| | |->17:{17} Weak SCC
| | |
| | |->18:{18} Weak SCC
| | |
| | |->20:{19} Weak SCC
| | |
| | |->21:{20} Weak SCC
| | |
| | |->22:{21} Weak SCC
| | |
| | |->23:{22} Weak SCC
| | |
| | |->24:{23} Weak SCC
| | |
| | |->25:{25} Weak SCC
| | |
| | |->26:{26} Weak SCC
| | |
| | |->27:{27} Weak SCC
| | |
| | |->28:{29} Weak SCC
| | |
| | `->19:{30,28,24} Weak SCC
| | |
| | |->20:{19} Weak SCC
| | |
| | |->21:{20} Weak SCC
| | |
| | |->22:{21} Weak SCC
| | |
| | |->23:{22} Weak SCC
| | |
| | |->24:{23} Weak SCC
| | |
| | |->25:{25} Weak SCC
| | |
| | |->26:{26} Weak SCC
| | |
| | |->27:{27} Weak SCC
| | |
| | `->28:{29} Weak SCC
| |
| |->13:{31} Weak SCC
| |
| `->14:{32} Weak SCC
|
`->8:{35} Weak SCC
->5:{9,10}
|
|->9:{4,6,5}
| |
| |->15:{15} Weak SCC
| | |
| | |->16:{16} Weak SCC
| | |
| | |->17:{17} Weak SCC
| | |
| | |->18:{18} Weak SCC
| | |
| | |->20:{19} Weak SCC
| | |
| | |->21:{20} Weak SCC
| | |
| | |->22:{21} Weak SCC
| | |
| | |->23:{22} Weak SCC
| | |
| | |->24:{23} Weak SCC
| | |
| | |->25:{25} Weak SCC
| | |
| | |->26:{26} Weak SCC
| | |
| | |->27:{27} Weak SCC
| | |
| | |->28:{29} Weak SCC
| | |
| | `->19:{30,28,24} Weak SCC
| | |
| | |->20:{19} Weak SCC
| | |
| | |->21:{20} Weak SCC
| | |
| | |->22:{21} Weak SCC
| | |
| | |->23:{22} Weak SCC
| | |
| | |->24:{23} Weak SCC
| | |
| | |->25:{25} Weak SCC
| | |
| | |->26:{26} Weak SCC
| | |
| | |->27:{27} Weak SCC
| | |
| | `->28:{29} Weak SCC
| |
| |->10:{33} Weak SCC
| |
| `->11:{34} Weak SCC
|
`->6:{36} Weak SCC
->4:{11} Weak SCC
->3:{12} Weak SCC
->2:{13} Weak SCC
->1:{14} Weak SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 2: insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, 3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 4: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, 5: insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, 6: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, 7: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 8: insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, 9: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, 10: insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak DPs:
{ 11: #abs^#(#0()) -> c_1()
, 12: #abs^#(#neg(@x)) -> c_2()
, 13: #abs^#(#pos(@x)) -> c_3()
, 14: #abs^#(#s(@x)) -> c_4()
, 15: #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, 16: #cklt^#(#EQ()) -> c_34()
, 17: #cklt^#(#GT()) -> c_35()
, 18: #cklt^#(#LT()) -> c_36()
, 19: #compare^#(#0(), #0()) -> c_22()
, 20: #compare^#(#0(), #neg(@y)) -> c_23()
, 21: #compare^#(#0(), #pos(@y)) -> c_24()
, 22: #compare^#(#0(), #s(@y)) -> c_25()
, 23: #compare^#(#neg(@x), #0()) -> c_26()
, 24: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, 25: #compare^#(#neg(@x), #pos(@y)) -> c_28()
, 26: #compare^#(#pos(@x), #0()) -> c_29()
, 27: #compare^#(#pos(@x), #neg(@y)) -> c_30()
, 28: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, 29: #compare^#(#s(@x), #0()) -> c_32()
, 30: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, 31: insert#1^#(nil(), @x) -> c_8()
, 32: insert#2^#(#false(), @x, @y, @ys) -> c_9()
, 33: insertD#1^#(nil(), @x) -> c_13()
, 34: insertD#2^#(#false(), @x, @y, @ys) -> c_14()
, 35: insertionsort#1^#(nil()) -> c_18()
, 36: insertionsortD#1^#(nil()) -> c_21() }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 14: #abs^#(#s(@x)) -> c_4()
, 13: #abs^#(#pos(@x)) -> c_3()
, 12: #abs^#(#neg(@x)) -> c_2()
, 11: #abs^#(#0()) -> c_1()
, 36: insertionsortD#1^#(nil()) -> c_21()
, 35: insertionsort#1^#(nil()) -> c_18()
, 33: insertD#1^#(nil(), @x) -> c_13()
, 34: insertD#2^#(#false(), @x, @y, @ys) -> c_14()
, 31: insert#1^#(nil(), @x) -> c_8()
, 32: insert#2^#(#false(), @x, @y, @ys) -> c_9()
, 15: #less^#(@x, @y) ->
c_5(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, 16: #cklt^#(#EQ()) -> c_34()
, 17: #cklt^#(#GT()) -> c_35()
, 18: #cklt^#(#LT()) -> c_36()
, 30: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
, 28: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
, 24: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
, 19: #compare^#(#0(), #0()) -> c_22()
, 20: #compare^#(#0(), #neg(@y)) -> c_23()
, 21: #compare^#(#0(), #pos(@y)) -> c_24()
, 22: #compare^#(#0(), #s(@y)) -> c_25()
, 23: #compare^#(#neg(@x), #0()) -> c_26()
, 25: #compare^#(#neg(@x), #pos(@y)) -> c_28()
, 26: #compare^#(#pos(@x), #0()) -> c_29()
, 27: #compare^#(#pos(@x), #neg(@y)) -> c_30()
, 29: #compare^#(#s(@x), #0()) -> c_32() }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We consider the following dependency-graph
1: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :2
2: insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :3
3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
4: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x)) :5
5: insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :6
6: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :4
7: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :8
8: insertionsort#1^#(::(@x, @xs)) ->
c_17(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :7
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
9: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :10
10: insertionsortD#1^#(::(@x, @xs)) ->
c_20(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :9
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :4
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ insert#1^#(::(@y, @ys), @x) ->
c_7(insert#2^#(#less(@y, @x), @x, @y, @ys), #less^#(@y, @x))
, insertD#1^#(::(@y, @ys), @x) ->
c_12(insertD#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:
{ 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)
, insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We employ 'linear path analysis' using the following approximated
dependency graph:
->2:{7,8} [ ? ]
|
`->4:{1,3,2} [ YES(O(1),O(n^2)) ]
->1:{9,10} [ ? ]
|
`->3:{4,6,5} [ YES(O(1),O(n^2)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 2: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, 3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 4: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, 5: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, 6: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, 7: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 8: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, 9: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, 10: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
* Path 2:{7,8}->4:{1,3,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:
{ 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)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider 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) :2
2: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :3
3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
4: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :5
5: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :4
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :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:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak DPs: { insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider 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) :2
2: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :5
3: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :4
4: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :3
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
5: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :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^2)).
Strict DPs:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
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:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider 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) :4
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :3
3: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
4: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :5
5: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :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:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insertionsort^#(@l) -> insertionsort#1^#(@l) }
Weak DPs:
{ insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#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()
, 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(@l) -> insertionsort#1(@l)
, 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:
{ insert^#(@x, @l) -> insert#1^#(@l, @x)
, insertionsort^#(@l) -> insertionsort#1^#(@l) }
Weak DPs:
{ insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 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()
, 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(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
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: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, 4: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 5: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
Trs:
{ #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #neg(@y)) -> #GT()
, #compare(#pos(@x), #0()) -> #GT()
, #compare(#pos(@x), #neg(@y)) -> #GT()
, #compare(#s(@x), #0()) -> #GT()
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(#neg) = {}, Uargs(#pos) = {}, Uargs(#s) = {},
Uargs(#less) = {}, Uargs(#compare) = {}, Uargs(#cklt) = {},
Uargs(insert) = {}, Uargs(insert#1) = {}, Uargs(::) = {},
Uargs(insert#2) = {}, Uargs(insertionsort) = {},
Uargs(insertionsort#1) = {}, Uargs(#abs^#) = {},
Uargs(#less^#) = {}, Uargs(#cklt^#) = {}, Uargs(#compare^#) = {},
Uargs(insert^#) = {}, Uargs(insert#1^#) = {},
Uargs(insert#2^#) = {}, Uargs(insertD^#) = {},
Uargs(insertD#1^#) = {}, Uargs(insertD#2^#) = {},
Uargs(insertionsort^#) = {}, Uargs(insertionsort#1^#) = {},
Uargs(insertionsortD^#) = {}, Uargs(insertionsortD#1^#) = {},
Uargs(c_1) = {1, 2}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [2]
[0]
[#neg](x1) = [1 0] x1 + [1]
[1 1] [2]
[#pos](x1) = [1 0] x1 + [0]
[0 1] [2]
[#s](x1) = [1 0] x1 + [0]
[0 1] [2]
[#less](x1, x2) = [1]
[1]
[#compare](x1, x2) = [0 0] x1 + [0 0] x2 + [2]
[2 0] [2 0] [0]
[#cklt](x1) = [1]
[1]
[insert](x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[1 0] [1 1] [3]
[insert#1](x1, x2) = [1 0] x1 + [0 0] x2 + [2]
[1 1] [1 0] [3]
[::](x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[1 0] [1 1] [2]
[insert#2](x1, x2, x3, x4) = [2 2] x1 + [0 0] x2 + [0 0] x3 + [1
0] x4 + [0]
[1 3] [1 0] [1 0] [2
1] [3]
[nil] = [0]
[3]
[#false] = [1]
[1]
[#true] = [1]
[1]
[insertionsort](x1) = [2 0] x1 + [2]
[3 3] [3]
[insertionsort#1](x1) = [2 0] x1 + [2]
[3 3] [2]
[#EQ] = [0]
[0]
[#GT] = [0]
[0]
[#LT] = [2]
[2]
[#abs^#](x1) = [0]
[0]
[#less^#](x1, x2) = [0]
[0]
[#cklt^#](x1) = [0]
[0]
[#compare^#](x1, x2) = [0]
[0]
[insert^#](x1, x2) = [2 0] x1 + [1 0] x2 + [3]
[0 0] [0 0] [2]
[insert#1^#](x1, x2) = [1 0] x1 + [2 0] x2 + [3]
[0 0] [0 0] [2]
[insert#2^#](x1, x2, x3, x4) = [2 2] x1 + [2 0] x2 + [1
0] x4 + [0]
[0 1] [0 0] [0
0] [1]
[insertD^#](x1, x2) = [0]
[0]
[insertD#1^#](x1, x2) = [0]
[0]
[insertD#2^#](x1, x2, x3, x4) = [0]
[0]
[insertionsort^#](x1) = [3 3] x1 + [2]
[0 0] [1]
[insertionsort#1^#](x1) = [3 3] x1 + [2]
[0 0] [0]
[insertionsortD^#](x1) = [0]
[0]
[insertionsortD#1^#](x1) = [0]
[0]
[c_1](x1, x2) = [1 1] x1 + [1 3] x2 + [1]
[0 0] [0 0] [0]
This order satisfies following ordering constraints
[#less(@x, @y)] = [1]
[1]
>= [1]
[1]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [2]
[8]
> [0]
[0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0 0] @y + [2]
[2 0] [6]
> [0]
[0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0 0] @y + [2]
[2 0] [4]
>= [2]
[2]
= [#LT()]
[#compare(#0(), #s(@y))] = [0 0] @y + [2]
[2 0] [4]
>= [2]
[2]
= [#LT()]
[#compare(#neg(@x), #0())] = [0 0] @x + [2]
[2 0] [6]
>= [2]
[2]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [4]
>= [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [0]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [2]
>= [2]
[2]
= [#LT()]
[#compare(#pos(@x), #0())] = [0 0] @x + [2]
[2 0] [4]
> [0]
[0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [2]
> [0]
[0]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [0]
>= [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [0]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [0 0] @x + [2]
[2 0] [4]
> [0]
[0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [0]
>= [0 0] @x + [0 0] @y + [2]
[2 0] [2 0] [0]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [1]
[1]
>= [1]
[1]
= [#false()]
[#cklt(#GT())] = [1]
[1]
>= [1]
[1]
= [#false()]
[#cklt(#LT())] = [1]
[1]
>= [1]
[1]
= [#true()]
[insert(@x, @l)] = [1 0] @l + [0 0] @x + [2]
[1 1] [1 0] [3]
>= [1 0] @l + [0 0] @x + [2]
[1 1] [1 0] [3]
= [insert#1(@l, @x)]
[insert#1(::(@y, @ys), @x)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [7]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [7]
= [insert#2(#less(@y, @x), @x, @y, @ys)]
[insert#1(nil(), @x)] = [0 0] @x + [2]
[1 0] [6]
>= [0 0] @x + [2]
[1 0] [5]
= [::(@x, nil())]
[insert#2(#false(), @x, @y, @ys)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [7]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
= [::(@x, ::(@y, @ys))]
[insert#2(#true(), @x, @y, @ys)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [7]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [7]
= [::(@y, insert(@x, @ys))]
[insertionsort(@l)] = [2 0] @l + [2]
[3 3] [3]
>= [2 0] @l + [2]
[3 3] [2]
= [insertionsort#1(@l)]
[insertionsort#1(::(@x, @xs))] = [0 0] @x + [2 0] @xs + [6]
[3 0] [6 3] [14]
> [0 0] @x + [2 0] @xs + [4]
[1 0] [5 3] [8]
= [insert(@x, insertionsort(@xs))]
[insertionsort#1(nil())] = [2]
[11]
> [0]
[3]
= [nil()]
[insert^#(@x, @l)] = [1 0] @l + [2 0] @x + [3]
[0 0] [0 0] [2]
>= [1 0] @l + [2 0] @x + [3]
[0 0] [0 0] [2]
= [insert#1^#(@l, @x)]
[insert#1^#(::(@y, @ys), @x)] = [2 0] @x + [1 0] @ys + [5]
[0 0] [0 0] [2]
> [2 0] @x + [1 0] @ys + [4]
[0 0] [0 0] [2]
= [insert#2^#(#less(@y, @x), @x, @y, @ys)]
[insert#2^#(#true(), @x, @y, @ys)] = [2 0] @x + [1 0] @ys + [4]
[0 0] [0 0] [2]
> [2 0] @x + [1 0] @ys + [3]
[0 0] [0 0] [2]
= [insert^#(@x, @ys)]
[insertionsort^#(@l)] = [3 3] @l + [2]
[0 0] [1]
>= [3 3] @l + [2]
[0 0] [0]
= [insertionsort#1^#(@l)]
[insertionsort#1^#(::(@x, @xs))] = [3 0] @x + [6 3] @xs + [14]
[0 0] [0 0] [0]
> [2 0] @x + [5 3] @xs + [13]
[0 0] [0 0] [0]
= [c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))]
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: insert^#(@x, @l) -> insert#1^#(@l, @x)
-->_1 insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys) :3
2: insertionsort^#(@l) -> insertionsort#1^#(@l)
-->_1 insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) :5
3: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys) :4
4: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
5: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
-->_2 insertionsort^#(@l) -> insertionsort#1^#(@l) :2
-->_1 insert^#(@x, @l) -> insert#1^#(@l, @x) :1
- 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:
{ 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)
, insertionsort^#(@l) -> insertionsort#1^#(@l)
, 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()
, 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(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{4,5} Weak SCC
|
`->2:{1,3,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 2: insert#1^#(::(@y, @ys), @x) ->
insert#2^#(#less(@y, @x), @x, @y, @ys)
, 3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 4: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 5: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs)) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 4: insertionsort^#(@l) -> insertionsort#1^#(@l)
, 5: insertionsort#1^#(::(@x, @xs)) ->
c_1(insert^#(@x, insertionsort(@xs)), insertionsort^#(@xs))
, 1: insert^#(@x, @l) -> insert#1^#(@l, @x)
, 3: insert#2^#(#true(), @x, @y, @ys) -> insert^#(@x, @ys)
, 2: 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()
, 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(@l) -> insertionsort#1(@l)
, 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
* Path 1:{9,10}->3:{4,6,5}: 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:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys) :2
2: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :3
3: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :1
4: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :5
5: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :4
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :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:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak DPs:
{ insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys) :2
2: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :5
3: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :4
4: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :3
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :1
5: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :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^2)).
Strict DPs:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak DPs:
{ insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We consider the (estimated) dependency graph
1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys) :4
2: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :3
3: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :2
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :1
4: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :5
5: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :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:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l) }
Weak DPs:
{ insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
Weak Trs:
{ #abs(#0()) -> #0()
, #abs(#neg(@x)) -> #pos(@x)
, #abs(#pos(@x)) -> #pos(@x)
, #abs(#s(@x)) -> #pos(#s(@x))
, #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()
, 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))
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsort(@l) -> insertionsort#1(@l)
, insertionsort#1(::(@x, @xs)) -> insert(@x, insertionsort(@xs))
, insertionsort#1(nil()) -> nil()
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#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()
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l) }
Weak DPs:
{ insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@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()
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
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:
{ 2: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, 4: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) }
Trs:
{ #compare(#0(), #0()) -> #EQ()
, #compare(#0(), #pos(@y)) -> #LT()
, #compare(#0(), #s(@y)) -> #LT()
, #compare(#neg(@x), #0()) -> #LT()
, #compare(#neg(@x), #pos(@y)) -> #LT()
, insertionsortD#1(nil()) -> nil() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(#neg) = {}, Uargs(#pos) = {}, Uargs(#s) = {},
Uargs(#less) = {}, Uargs(#compare) = {}, Uargs(#cklt) = {},
Uargs(::) = {}, Uargs(insertD) = {}, Uargs(insertD#1) = {},
Uargs(insertD#2) = {}, Uargs(insertionsortD) = {},
Uargs(insertionsortD#1) = {}, Uargs(#abs^#) = {},
Uargs(#less^#) = {}, Uargs(#cklt^#) = {}, Uargs(#compare^#) = {},
Uargs(insert^#) = {}, Uargs(insert#1^#) = {},
Uargs(insert#2^#) = {}, Uargs(insertD^#) = {},
Uargs(insertD#1^#) = {}, Uargs(insertD#2^#) = {},
Uargs(insertionsort^#) = {}, Uargs(insertionsort#1^#) = {},
Uargs(insertionsortD^#) = {}, Uargs(insertionsortD#1^#) = {},
Uargs(c_2) = {1, 2}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[#0] = [0]
[0]
[#neg](x1) = [0 0] x1 + [3]
[1 1] [0]
[#pos](x1) = [1 0] x1 + [0]
[0 1] [2]
[#s](x1) = [1 0] x1 + [0]
[0 1] [2]
[#less](x1, x2) = [0]
[1]
[#compare](x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[1 2] [1 2] [0]
[#cklt](x1) = [0]
[1]
[::](x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[1 0] [1 1] [2]
[nil] = [1]
[0]
[#false] = [0]
[1]
[#true] = [0]
[1]
[insertD](x1, x2) = [0 0] x1 + [1 0] x2 + [2]
[1 0] [1 1] [2]
[insertD#1](x1, x2) = [1 0] x1 + [0 0] x2 + [2]
[1 1] [1 0] [2]
[insertD#2](x1, x2, x3, x4) = [0 2] x1 + [0 0] x2 + [0 0] x3 + [1
0] x4 + [2]
[2 3] [1 0] [1 0] [2
1] [3]
[insertionsortD](x1) = [1 0] x1 + [1]
[3 1] [3]
[insertionsortD#1](x1) = [1 0] x1 + [1]
[3 1] [2]
[#EQ] = [0]
[0]
[#GT] = [1]
[0]
[#LT] = [0]
[3]
[#abs^#](x1) = [0]
[0]
[#less^#](x1, x2) = [0]
[0]
[#cklt^#](x1) = [0]
[0]
[#compare^#](x1, x2) = [0]
[0]
[insert^#](x1, x2) = [0]
[0]
[insert#1^#](x1, x2) = [0]
[0]
[insert#2^#](x1, x2, x3, x4) = [0]
[0]
[insertD^#](x1, x2) = [2 0] x2 + [0]
[0 0] [3]
[insertD#1^#](x1, x2) = [2 0] x1 + [0]
[0 0] [3]
[insertD#2^#](x1, x2, x3, x4) = [3 2] x1 + [2 0] x4 + [2]
[0 2] [0 0] [1]
[insertionsort^#](x1) = [0]
[0]
[insertionsort#1^#](x1) = [0]
[0]
[insertionsortD^#](x1) = [3 3] x1 + [2]
[0 1] [1]
[insertionsortD#1^#](x1) = [2 3] x1 + [0]
[0 0] [0]
[c_2](x1, x2) = [1 2] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
This order satisfies following ordering constraints
[#less(@x, @y)] = [0]
[1]
>= [0]
[1]
= [#cklt(#compare(@x, @y))]
[#compare(#0(), #0())] = [1]
[0]
> [0]
[0]
= [#EQ()]
[#compare(#0(), #neg(@y))] = [0 0] @y + [1]
[2 2] [3]
>= [1]
[0]
= [#GT()]
[#compare(#0(), #pos(@y))] = [0 0] @y + [1]
[1 2] [4]
> [0]
[3]
= [#LT()]
[#compare(#0(), #s(@y))] = [0 0] @y + [1]
[1 2] [4]
> [0]
[3]
= [#LT()]
[#compare(#neg(@x), #0())] = [0 0] @x + [1]
[2 2] [3]
> [0]
[3]
= [#LT()]
[#compare(#neg(@x), #neg(@y))] = [0 0] @x + [0 0] @y + [1]
[2 2] [2 2] [6]
>= [0 0] @x + [0 0] @y + [1]
[1 2] [1 2] [0]
= [#compare(@y, @x)]
[#compare(#neg(@x), #pos(@y))] = [0 0] @x + [0 0] @y + [1]
[2 2] [1 2] [7]
> [0]
[3]
= [#LT()]
[#compare(#pos(@x), #0())] = [0 0] @x + [1]
[1 2] [4]
>= [1]
[0]
= [#GT()]
[#compare(#pos(@x), #neg(@y))] = [0 0] @x + [0 0] @y + [1]
[1 2] [2 2] [7]
>= [1]
[0]
= [#GT()]
[#compare(#pos(@x), #pos(@y))] = [0 0] @x + [0 0] @y + [1]
[1 2] [1 2] [8]
>= [0 0] @x + [0 0] @y + [1]
[1 2] [1 2] [0]
= [#compare(@x, @y)]
[#compare(#s(@x), #0())] = [0 0] @x + [1]
[1 2] [4]
>= [1]
[0]
= [#GT()]
[#compare(#s(@x), #s(@y))] = [0 0] @x + [0 0] @y + [1]
[1 2] [1 2] [8]
>= [0 0] @x + [0 0] @y + [1]
[1 2] [1 2] [0]
= [#compare(@x, @y)]
[#cklt(#EQ())] = [0]
[1]
>= [0]
[1]
= [#false()]
[#cklt(#GT())] = [0]
[1]
>= [0]
[1]
= [#false()]
[#cklt(#LT())] = [0]
[1]
>= [0]
[1]
= [#true()]
[insertD(@x, @l)] = [1 0] @l + [0 0] @x + [2]
[1 1] [1 0] [2]
>= [1 0] @l + [0 0] @x + [2]
[1 1] [1 0] [2]
= [insertD#1(@l, @x)]
[insertD#1(::(@y, @ys), @x)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
= [insertD#2(#less(@y, @x), @x, @y, @ys)]
[insertD#1(nil(), @x)] = [0 0] @x + [3]
[1 0] [3]
>= [0 0] @x + [3]
[1 0] [3]
= [::(@x, nil())]
[insertD#2(#false(), @x, @y, @ys)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
= [::(@x, ::(@y, @ys))]
[insertD#2(#true(), @x, @y, @ys)] = [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
>= [0 0] @x + [0 0] @y + [1 0] @ys + [4]
[1 0] [1 0] [2 1] [6]
= [::(@y, insertD(@x, @ys))]
[insertionsortD(@l)] = [1 0] @l + [1]
[3 1] [3]
>= [1 0] @l + [1]
[3 1] [2]
= [insertionsortD#1(@l)]
[insertionsortD#1(::(@x, @xs))] = [0 0] @x + [1 0] @xs + [3]
[1 0] [4 1] [10]
>= [0 0] @x + [1 0] @xs + [3]
[1 0] [4 1] [6]
= [insertD(@x, insertionsortD(@xs))]
[insertionsortD#1(nil())] = [2]
[5]
> [1]
[0]
= [nil()]
[insertD^#(@x, @l)] = [2 0] @l + [0]
[0 0] [3]
>= [2 0] @l + [0]
[0 0] [3]
= [insertD#1^#(@l, @x)]
[insertD#1^#(::(@y, @ys), @x)] = [2 0] @ys + [4]
[0 0] [3]
>= [2 0] @ys + [4]
[0 0] [3]
= [insertD#2^#(#less(@y, @x), @x, @y, @ys)]
[insertD#2^#(#true(), @x, @y, @ys)] = [2 0] @ys + [4]
[0 0] [3]
> [2 0] @ys + [0]
[0 0] [3]
= [insertD^#(@x, @ys)]
[insertionsortD^#(@l)] = [3 3] @l + [2]
[0 1] [1]
> [2 3] @l + [0]
[0 0] [0]
= [insertionsortD#1^#(@l)]
[insertionsortD#1^#(::(@x, @xs))] = [3 0] @x + [5 3] @xs + [10]
[0 0] [0 0] [0]
>= [5 3] @xs + [10]
[0 0] [0]
= [c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))]
Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^2)) on application of rules {2,4}.
Here rules are labeled according to the (estimated) dependency
graph
1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
-->_1 insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys) :3
2: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
-->_1 insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) :5
3: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
-->_1 insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys) :4
4: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :1
5: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
-->_2 insertionsortD^#(@l) -> insertionsortD#1^#(@l) :2
-->_1 insertD^#(@x, @l) -> insertD#1^#(@l, @x) :1
- The rules {2,4} have known complexity. These cover all
predecessors of {5}, their complexity is equally bounded.
- The rules {2,4,5} have known complexity. These cover all
predecessors of {1}, their complexity is equally bounded.
- The rules {1,2,4,5} have known complexity. These cover all
predecessors of {3}, 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:
{ insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@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()
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#1(nil()) -> nil() }
StartTerms: basic terms
Strategy: innermost
We consider the the dependency graph
->1:{4,5} Weak SCC
|
`->2:{1,3,2} Weak SCC
Here dependency-pairs are as follows:
Weak DPs:
{ 1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, 2: insertD#1^#(::(@y, @ys), @x) ->
insertD#2^#(#less(@y, @x), @x, @y, @ys)
, 3: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, 4: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, 5: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs)) }
The following rules are part of trailing weak paths, and thus they
can be removed:
{ 4: insertionsortD^#(@l) -> insertionsortD#1^#(@l)
, 5: insertionsortD#1^#(::(@x, @xs)) ->
c_2(insertD^#(@x, insertionsortD(@xs)), insertionsortD^#(@xs))
, 1: insertD^#(@x, @l) -> insertD#1^#(@l, @x)
, 3: insertD#2^#(#true(), @x, @y, @ys) -> insertD^#(@x, @ys)
, 2: insertD#1^#(::(@y, @ys), @x) ->
insertD#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()
, insertD(@x, @l) -> insertD#1(@l, @x)
, insertD#1(::(@y, @ys), @x) ->
insertD#2(#less(@y, @x), @x, @y, @ys)
, insertD#1(nil(), @x) -> ::(@x, nil())
, insertD#2(#false(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
, insertD#2(#true(), @x, @y, @ys) -> ::(@y, insertD(@x, @ys))
, insertionsortD(@l) -> insertionsortD#1(@l)
, insertionsortD#1(::(@x, @xs)) -> insertD(@x, insertionsortD(@xs))
, insertionsortD#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))