Problem minsort.raml

tct

Execution Time (secs)	3.966
Answer	YES(O(1),O(n^2))
Input	minsort.raml

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 Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#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(1),O(n^2))

We add following dependency tuples

Strict DPs:
  { #less^#(@x, @y) ->
    c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , findMin^#(@l) -> findMin#1^#(@l)
  , findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
  , findMin#1^#(nil()) -> c_4()
  , findMin#2^#(::(@y, @ys), @x) ->
    c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
  , findMin#2^#(nil(), @x) -> c_6()
  , findMin#3^#(#false(), @x, @y, @ys) -> c_7()
  , findMin#3^#(#true(), @x, @y, @ys) -> c_8()
  , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> minSort^#(@xs)
  , minSort#1^#(nil()) -> c_11() }
Weak DPs:
  { #cklt^#(#EQ()) -> c_24()
  , #cklt^#(#GT()) -> c_25()
  , #cklt^#(#LT()) -> c_26()
  , #compare^#(#0(), #0()) -> c_12()
  , #compare^#(#0(), #neg(@y)) -> c_13()
  , #compare^#(#0(), #pos(@y)) -> c_14()
  , #compare^#(#0(), #s(@y)) -> c_15()
  , #compare^#(#neg(@x), #0()) -> c_16()
  , #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
  , #compare^#(#neg(@x), #pos(@y)) -> c_18()
  , #compare^#(#pos(@x), #0()) -> c_19()
  , #compare^#(#pos(@x), #neg(@y)) -> c_20()
  , #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
  , #compare^#(#s(@x), #0()) -> c_22()
  , #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(1),O(n^2)).

Strict DPs:
  { #less^#(@x, @y) ->
    c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , findMin^#(@l) -> findMin#1^#(@l)
  , findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
  , findMin#1^#(nil()) -> c_4()
  , findMin#2^#(::(@y, @ys), @x) ->
    c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
  , findMin#2^#(nil(), @x) -> c_6()
  , findMin#3^#(#false(), @x, @y, @ys) -> c_7()
  , findMin#3^#(#true(), @x, @y, @ys) -> c_8()
  , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> minSort^#(@xs)
  , minSort#1^#(nil()) -> c_11() }
Weak DPs:
  { #cklt^#(#EQ()) -> c_24()
  , #cklt^#(#GT()) -> c_25()
  , #cklt^#(#LT()) -> c_26()
  , #compare^#(#0(), #0()) -> c_12()
  , #compare^#(#0(), #neg(@y)) -> c_13()
  , #compare^#(#0(), #pos(@y)) -> c_14()
  , #compare^#(#0(), #s(@y)) -> c_15()
  , #compare^#(#neg(@x), #0()) -> c_16()
  , #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
  , #compare^#(#neg(@x), #pos(@y)) -> c_18()
  , #compare^#(#pos(@x), #0()) -> c_19()
  , #compare^#(#pos(@x), #neg(@y)) -> c_20()
  , #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
  , #compare^#(#s(@x), #0()) -> c_22()
  , #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We consider the (estimated) dependency graph

  1: #less^#(@x, @y) ->
     c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
     -->_2 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :26
     -->_2 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :24
     -->_2 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :20
     -->_2 #compare^#(#s(@x), #0()) -> c_22() :25
     -->_2 #compare^#(#pos(@x), #neg(@y)) -> c_20() :23
     -->_2 #compare^#(#pos(@x), #0()) -> c_19() :22
     -->_2 #compare^#(#neg(@x), #pos(@y)) -> c_18() :21
     -->_2 #compare^#(#neg(@x), #0()) -> c_16() :19
     -->_2 #compare^#(#0(), #s(@y)) -> c_15() :18
     -->_2 #compare^#(#0(), #pos(@y)) -> c_14() :17
     -->_2 #compare^#(#0(), #neg(@y)) -> c_13() :16
     -->_2 #compare^#(#0(), #0()) -> c_12() :15
     -->_1 #cklt^#(#LT()) -> c_26() :14
     -->_1 #cklt^#(#GT()) -> c_25() :13
     -->_1 #cklt^#(#EQ()) -> c_24() :12

  2: findMin^#(@l) -> findMin#1^#(@l)
     -->_1 findMin#1^#(::(@x, @xs)) ->
           c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) :3
     -->_1 findMin#1^#(nil()) -> c_4() :4

  3: findMin#1^#(::(@x, @xs)) ->
     c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
     -->_1 findMin#2^#(::(@y, @ys), @x) ->
           c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) :5
     -->_1 findMin#2^#(nil(), @x) -> c_6() :6
     -->_2 findMin^#(@l) -> findMin#1^#(@l) :2

  4: findMin#1^#(nil()) -> c_4()

  5: findMin#2^#(::(@y, @ys), @x) ->
     c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
     -->_1 findMin#3^#(#true(), @x, @y, @ys) -> c_8() :8
     -->_1 findMin#3^#(#false(), @x, @y, @ys) -> c_7() :7
     -->_2 #less^#(@x, @y) ->
           c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) :1

  6: findMin#2^#(nil(), @x) -> c_6()

  7: findMin#3^#(#false(), @x, @y, @ys) -> c_7()

  8: findMin#3^#(#true(), @x, @y, @ys) -> c_8()

  9: minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
     -->_1 minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) :10
     -->_1 minSort#1^#(nil()) -> c_11() :11
     -->_2 findMin^#(@l) -> findMin#1^#(@l) :2

  10: minSort#1^#(::(@x, @xs)) -> minSort^#(@xs)
     -->_1 minSort^#(@l) ->
           c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) :9

  11: minSort#1^#(nil()) -> c_11()

  12: #cklt^#(#EQ()) -> c_24()

  13: #cklt^#(#GT()) -> c_25()

  14: #cklt^#(#LT()) -> c_26()

  15: #compare^#(#0(), #0()) -> c_12()

  16: #compare^#(#0(), #neg(@y)) -> c_13()

  17: #compare^#(#0(), #pos(@y)) -> c_14()

  18: #compare^#(#0(), #s(@y)) -> c_15()

  19: #compare^#(#neg(@x), #0()) -> c_16()

  20: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
     -->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :26
     -->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :24
     -->_1 #compare^#(#s(@x), #0()) -> c_22() :25
     -->_1 #compare^#(#pos(@x), #neg(@y)) -> c_20() :23
     -->_1 #compare^#(#pos(@x), #0()) -> c_19() :22
     -->_1 #compare^#(#neg(@x), #pos(@y)) -> c_18() :21
     -->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :20
     -->_1 #compare^#(#neg(@x), #0()) -> c_16() :19
     -->_1 #compare^#(#0(), #s(@y)) -> c_15() :18
     -->_1 #compare^#(#0(), #pos(@y)) -> c_14() :17
     -->_1 #compare^#(#0(), #neg(@y)) -> c_13() :16
     -->_1 #compare^#(#0(), #0()) -> c_12() :15

  21: #compare^#(#neg(@x), #pos(@y)) -> c_18()

  22: #compare^#(#pos(@x), #0()) -> c_19()

  23: #compare^#(#pos(@x), #neg(@y)) -> c_20()

  24: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
     -->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :26
     -->_1 #compare^#(#s(@x), #0()) -> c_22() :25
     -->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :24
     -->_1 #compare^#(#pos(@x), #neg(@y)) -> c_20() :23
     -->_1 #compare^#(#pos(@x), #0()) -> c_19() :22
     -->_1 #compare^#(#neg(@x), #pos(@y)) -> c_18() :21
     -->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :20
     -->_1 #compare^#(#neg(@x), #0()) -> c_16() :19
     -->_1 #compare^#(#0(), #s(@y)) -> c_15() :18
     -->_1 #compare^#(#0(), #pos(@y)) -> c_14() :17
     -->_1 #compare^#(#0(), #neg(@y)) -> c_13() :16
     -->_1 #compare^#(#0(), #0()) -> c_12() :15

  25: #compare^#(#s(@x), #0()) -> c_22()

  26: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
     -->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :26
     -->_1 #compare^#(#s(@x), #0()) -> c_22() :25
     -->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :24
     -->_1 #compare^#(#pos(@x), #neg(@y)) -> c_20() :23
     -->_1 #compare^#(#pos(@x), #0()) -> c_19() :22
     -->_1 #compare^#(#neg(@x), #pos(@y)) -> c_18() :21
     -->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :20
     -->_1 #compare^#(#neg(@x), #0()) -> c_16() :19
     -->_1 #compare^#(#0(), #s(@y)) -> c_15() :18
     -->_1 #compare^#(#0(), #pos(@y)) -> c_14() :17
     -->_1 #compare^#(#0(), #neg(@y)) -> c_13() :16
     -->_1 #compare^#(#0(), #0()) -> c_12() :15

We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {11} and add Pre({11}) = {9} to the strict component.
- We remove {4} and add Pre({4}) = {2} to the strict component.
- We remove {6} and add Pre({6}) = {3} to the strict component.
- We remove {7} and add Pre({7}) = {5} to the strict component.
- We remove {8} and add Pre({8}) = {5} to the strict component.
- We remove {1} and add Pre({1}) = {5} to the strict component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { findMin^#(@l) -> findMin#1^#(@l)
  , findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
  , findMin#2^#(::(@y, @ys), @x) ->
    c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
  , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) }
Weak DPs:
  { #less^#(@x, @y) ->
    c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , #cklt^#(#EQ()) -> c_24()
  , #cklt^#(#GT()) -> c_25()
  , #cklt^#(#LT()) -> c_26()
  , #compare^#(#0(), #0()) -> c_12()
  , #compare^#(#0(), #neg(@y)) -> c_13()
  , #compare^#(#0(), #pos(@y)) -> c_14()
  , #compare^#(#0(), #s(@y)) -> c_15()
  , #compare^#(#neg(@x), #0()) -> c_16()
  , #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
  , #compare^#(#neg(@x), #pos(@y)) -> c_18()
  , #compare^#(#pos(@x), #0()) -> c_19()
  , #compare^#(#pos(@x), #neg(@y)) -> c_20()
  , #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
  , #compare^#(#s(@x), #0()) -> c_22()
  , #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
  , findMin#1^#(nil()) -> c_4()
  , findMin#2^#(nil(), @x) -> c_6()
  , findMin#3^#(#false(), @x, @y, @ys) -> c_7()
  , findMin#3^#(#true(), @x, @y, @ys) -> c_8()
  , minSort#1^#(nil()) -> c_11() }
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()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We consider the (estimated) dependency graph

  1: findMin^#(@l) -> findMin#1^#(@l)
     -->_1 findMin#1^#(::(@x, @xs)) ->
           c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) :2
     -->_1 findMin#1^#(nil()) -> c_4() :22

  2: findMin#1^#(::(@x, @xs)) ->
     c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
     -->_1 findMin#2^#(::(@y, @ys), @x) ->
           c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y)) :3
     -->_1 findMin#2^#(nil(), @x) -> c_6() :23
     -->_2 findMin^#(@l) -> findMin#1^#(@l) :1

  3: findMin#2^#(::(@y, @ys), @x) ->
     c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
     -->_2 #less^#(@x, @y) ->
           c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y)) :6
     -->_1 findMin#3^#(#true(), @x, @y, @ys) -> c_8() :25
     -->_1 findMin#3^#(#false(), @x, @y, @ys) -> c_7() :24

  4: minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
     -->_1 minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) :5
     -->_1 minSort#1^#(nil()) -> c_11() :26
     -->_2 findMin^#(@l) -> findMin#1^#(@l) :1

  5: minSort#1^#(::(@x, @xs)) -> minSort^#(@xs)
     -->_1 minSort^#(@l) ->
           c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) :4

  6: #less^#(@x, @y) ->
     c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
     -->_2 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :21
     -->_2 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :19
     -->_2 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :15
     -->_2 #compare^#(#s(@x), #0()) -> c_22() :20
     -->_2 #compare^#(#pos(@x), #neg(@y)) -> c_20() :18
     -->_2 #compare^#(#pos(@x), #0()) -> c_19() :17
     -->_2 #compare^#(#neg(@x), #pos(@y)) -> c_18() :16
     -->_2 #compare^#(#neg(@x), #0()) -> c_16() :14
     -->_2 #compare^#(#0(), #s(@y)) -> c_15() :13
     -->_2 #compare^#(#0(), #pos(@y)) -> c_14() :12
     -->_2 #compare^#(#0(), #neg(@y)) -> c_13() :11
     -->_2 #compare^#(#0(), #0()) -> c_12() :10
     -->_1 #cklt^#(#LT()) -> c_26() :9
     -->_1 #cklt^#(#GT()) -> c_25() :8
     -->_1 #cklt^#(#EQ()) -> c_24() :7

  7: #cklt^#(#EQ()) -> c_24()

  8: #cklt^#(#GT()) -> c_25()

  9: #cklt^#(#LT()) -> c_26()

  10: #compare^#(#0(), #0()) -> c_12()

  11: #compare^#(#0(), #neg(@y)) -> c_13()

  12: #compare^#(#0(), #pos(@y)) -> c_14()

  13: #compare^#(#0(), #s(@y)) -> c_15()

  14: #compare^#(#neg(@x), #0()) -> c_16()

  15: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
     -->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :21
     -->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :19
     -->_1 #compare^#(#s(@x), #0()) -> c_22() :20
     -->_1 #compare^#(#pos(@x), #neg(@y)) -> c_20() :18
     -->_1 #compare^#(#pos(@x), #0()) -> c_19() :17
     -->_1 #compare^#(#neg(@x), #pos(@y)) -> c_18() :16
     -->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :15
     -->_1 #compare^#(#neg(@x), #0()) -> c_16() :14
     -->_1 #compare^#(#0(), #s(@y)) -> c_15() :13
     -->_1 #compare^#(#0(), #pos(@y)) -> c_14() :12
     -->_1 #compare^#(#0(), #neg(@y)) -> c_13() :11
     -->_1 #compare^#(#0(), #0()) -> c_12() :10

  16: #compare^#(#neg(@x), #pos(@y)) -> c_18()

  17: #compare^#(#pos(@x), #0()) -> c_19()

  18: #compare^#(#pos(@x), #neg(@y)) -> c_20()

  19: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
     -->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :21
     -->_1 #compare^#(#s(@x), #0()) -> c_22() :20
     -->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :19
     -->_1 #compare^#(#pos(@x), #neg(@y)) -> c_20() :18
     -->_1 #compare^#(#pos(@x), #0()) -> c_19() :17
     -->_1 #compare^#(#neg(@x), #pos(@y)) -> c_18() :16
     -->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :15
     -->_1 #compare^#(#neg(@x), #0()) -> c_16() :14
     -->_1 #compare^#(#0(), #s(@y)) -> c_15() :13
     -->_1 #compare^#(#0(), #pos(@y)) -> c_14() :12
     -->_1 #compare^#(#0(), #neg(@y)) -> c_13() :11
     -->_1 #compare^#(#0(), #0()) -> c_12() :10

  20: #compare^#(#s(@x), #0()) -> c_22()

  21: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
     -->_1 #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y) :21
     -->_1 #compare^#(#s(@x), #0()) -> c_22() :20
     -->_1 #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y) :19
     -->_1 #compare^#(#pos(@x), #neg(@y)) -> c_20() :18
     -->_1 #compare^#(#pos(@x), #0()) -> c_19() :17
     -->_1 #compare^#(#neg(@x), #pos(@y)) -> c_18() :16
     -->_1 #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x) :15
     -->_1 #compare^#(#neg(@x), #0()) -> c_16() :14
     -->_1 #compare^#(#0(), #s(@y)) -> c_15() :13
     -->_1 #compare^#(#0(), #pos(@y)) -> c_14() :12
     -->_1 #compare^#(#0(), #neg(@y)) -> c_13() :11
     -->_1 #compare^#(#0(), #0()) -> c_12() :10

  22: findMin#1^#(nil()) -> c_4()

  23: findMin#2^#(nil(), @x) -> c_6()

  24: findMin#3^#(#false(), @x, @y, @ys) -> c_7()

  25: findMin#3^#(#true(), @x, @y, @ys) -> c_8()

  26: minSort#1^#(nil()) -> c_11()

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:
  { findMin^#(@l) -> findMin#1^#(@l)
  , findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
  , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) }
Weak DPs:
  { #less^#(@x, @y) ->
    c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , #cklt^#(#EQ()) -> c_24()
  , #cklt^#(#GT()) -> c_25()
  , #cklt^#(#LT()) -> c_26()
  , #compare^#(#0(), #0()) -> c_12()
  , #compare^#(#0(), #neg(@y)) -> c_13()
  , #compare^#(#0(), #pos(@y)) -> c_14()
  , #compare^#(#0(), #s(@y)) -> c_15()
  , #compare^#(#neg(@x), #0()) -> c_16()
  , #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
  , #compare^#(#neg(@x), #pos(@y)) -> c_18()
  , #compare^#(#pos(@x), #0()) -> c_19()
  , #compare^#(#pos(@x), #neg(@y)) -> c_20()
  , #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
  , #compare^#(#s(@x), #0()) -> c_22()
  , #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
  , findMin#1^#(nil()) -> c_4()
  , findMin#2^#(::(@y, @ys), @x) ->
    c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
  , findMin#2^#(nil(), @x) -> c_6()
  , findMin#3^#(#false(), @x, @y, @ys) -> c_7()
  , findMin#3^#(#true(), @x, @y, @ys) -> c_8()
  , minSort#1^#(nil()) -> c_11() }
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()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We consider the the dependency graph

  ->1:{3,4}
     |
     |->3:{1,2}
     |   |
     |   |->4:{21}                             Weak SCC
     |   |
     |   |->6:{22}                             Weak SCC
     |   |   |
     |   |   |->7:{5}                          Weak SCC
     |   |   |   |
     |   |   |   |->8:{6}                      Weak SCC
     |   |   |   |
     |   |   |   |->9:{7}                      Weak SCC
     |   |   |   |
     |   |   |   |->10:{8}                     Weak SCC
     |   |   |   |
     |   |   |   |->12:{9}                     Weak SCC
     |   |   |   |
     |   |   |   |->13:{10}                    Weak SCC
     |   |   |   |
     |   |   |   |->14:{11}                    Weak SCC
     |   |   |   |
     |   |   |   |->15:{12}                    Weak SCC
     |   |   |   |
     |   |   |   |->16:{13}                    Weak SCC
     |   |   |   |
     |   |   |   |->17:{15}                    Weak SCC
     |   |   |   |
     |   |   |   |->18:{16}                    Weak SCC
     |   |   |   |
     |   |   |   |->19:{17}                    Weak SCC
     |   |   |   |
     |   |   |   |->20:{19}                    Weak SCC
     |   |   |   |
     |   |   |   `->11:{20,18,14}              Weak SCC
     |   |   |       |
     |   |   |       |->12:{9}                 Weak SCC
     |   |   |       |
     |   |   |       |->13:{10}                Weak SCC
     |   |   |       |
     |   |   |       |->14:{11}                Weak SCC
     |   |   |       |
     |   |   |       |->15:{12}                Weak SCC
     |   |   |       |
     |   |   |       |->16:{13}                Weak SCC
     |   |   |       |
     |   |   |       |->17:{15}                Weak SCC
     |   |   |       |
     |   |   |       |->18:{16}                Weak SCC
     |   |   |       |
     |   |   |       |->19:{17}                Weak SCC
     |   |   |       |
     |   |   |       `->20:{19}                Weak SCC
     |   |   |
     |   |   |->21:{24}                        Weak SCC
     |   |   |
     |   |   `->22:{25}                        Weak SCC
     |   |
     |   `->5:{23}                             Weak SCC
     |
     `->2:{26}                                 Weak SCC


  Here dependency-pairs are as follows:

  Strict DPs:
    { 1: findMin^#(@l) -> findMin#1^#(@l)
    , 2: findMin#1^#(::(@x, @xs)) ->
         c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
    , 3: minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
    , 4: minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) }
  Weak DPs:
    { 5: #less^#(@x, @y) ->
         c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
    , 6: #cklt^#(#EQ()) -> c_24()
    , 7: #cklt^#(#GT()) -> c_25()
    , 8: #cklt^#(#LT()) -> c_26()
    , 9: #compare^#(#0(), #0()) -> c_12()
    , 10: #compare^#(#0(), #neg(@y)) -> c_13()
    , 11: #compare^#(#0(), #pos(@y)) -> c_14()
    , 12: #compare^#(#0(), #s(@y)) -> c_15()
    , 13: #compare^#(#neg(@x), #0()) -> c_16()
    , 14: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
    , 15: #compare^#(#neg(@x), #pos(@y)) -> c_18()
    , 16: #compare^#(#pos(@x), #0()) -> c_19()
    , 17: #compare^#(#pos(@x), #neg(@y)) -> c_20()
    , 18: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
    , 19: #compare^#(#s(@x), #0()) -> c_22()
    , 20: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
    , 21: findMin#1^#(nil()) -> c_4()
    , 22: findMin#2^#(::(@y, @ys), @x) ->
          c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
    , 23: findMin#2^#(nil(), @x) -> c_6()
    , 24: findMin#3^#(#false(), @x, @y, @ys) -> c_7()
    , 25: findMin#3^#(#true(), @x, @y, @ys) -> c_8()
    , 26: minSort#1^#(nil()) -> c_11() }

The following rules are part of trailing weak paths, and thus they
can be removed:

  { 26: minSort#1^#(nil()) -> c_11()
  , 21: findMin#1^#(nil()) -> c_4()
  , 23: findMin#2^#(nil(), @x) -> c_6()
  , 22: findMin#2^#(::(@y, @ys), @x) ->
        c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
  , 5: #less^#(@x, @y) ->
       c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , 6: #cklt^#(#EQ()) -> c_24()
  , 7: #cklt^#(#GT()) -> c_25()
  , 8: #cklt^#(#LT()) -> c_26()
  , 20: #compare^#(#s(@x), #s(@y)) -> #compare^#(@x, @y)
  , 18: #compare^#(#pos(@x), #pos(@y)) -> #compare^#(@x, @y)
  , 14: #compare^#(#neg(@x), #neg(@y)) -> #compare^#(@y, @x)
  , 9: #compare^#(#0(), #0()) -> c_12()
  , 10: #compare^#(#0(), #neg(@y)) -> c_13()
  , 11: #compare^#(#0(), #pos(@y)) -> c_14()
  , 12: #compare^#(#0(), #s(@y)) -> c_15()
  , 13: #compare^#(#neg(@x), #0()) -> c_16()
  , 15: #compare^#(#neg(@x), #pos(@y)) -> c_18()
  , 16: #compare^#(#pos(@x), #0()) -> c_19()
  , 17: #compare^#(#pos(@x), #neg(@y)) -> c_20()
  , 19: #compare^#(#s(@x), #0()) -> c_22()
  , 24: findMin#3^#(#false(), @x, @y, @ys) -> c_7()
  , 25: findMin#3^#(#true(), @x, @y, @ys) -> c_8() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { findMin^#(@l) -> findMin#1^#(@l)
  , findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
  , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> minSort^#(@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()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We consider the following dependency-graph

  1: findMin^#(@l) -> findMin#1^#(@l)
     -->_1 findMin#1^#(::(@x, @xs)) ->
           c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) :2

  2: findMin#1^#(::(@x, @xs)) ->
     c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
     -->_2 findMin^#(@l) -> findMin#1^#(@l) :1

  3: minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
     -->_1 minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) :4
     -->_2 findMin^#(@l) -> findMin#1^#(@l) :1

  4: minSort#1^#(::(@x, @xs)) -> minSort^#(@xs)
     -->_1 minSort^#(@l) ->
           c_9(minSort#1^#(findMin(@l)), findMin^#(@l)) :3

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { findMin^#(@l) -> findMin#1^#(@l)
  , findMin#1^#(::(@x, @xs)) -> findMin^#(@xs)
  , minSort^#(@l) -> c_1(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> minSort^#(@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()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We consider the (estimated) dependency graph

  1: findMin^#(@l) -> findMin#1^#(@l)
     -->_1 findMin#1^#(::(@x, @xs)) -> findMin^#(@xs) :2

  2: findMin#1^#(::(@x, @xs)) -> findMin^#(@xs)
     -->_1 findMin^#(@l) -> findMin#1^#(@l) :1

  3: minSort^#(@l) -> c_1(minSort#1^#(findMin(@l)), findMin^#(@l))
     -->_1 minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) :4
     -->_2 findMin^#(@l) -> findMin#1^#(@l) :1

  4: minSort#1^#(::(@x, @xs)) -> minSort^#(@xs)
     -->_1 minSort^#(@l) ->
           c_1(minSort#1^#(findMin(@l)), findMin^#(@l)) :3

We estimate the application of rules based on the application of
their predecessors as follows:
- We remove {2} and add Pre({2}) = {1} to the strict component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { findMin^#(@l) -> findMin#1^#(@l)
  , minSort^#(@l) -> c_1(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) }
Weak DPs: { findMin#1^#(::(@x, @xs)) -> findMin^#(@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()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We consider the (estimated) dependency graph

  1: findMin^#(@l) -> findMin#1^#(@l)
     -->_1 findMin#1^#(::(@x, @xs)) -> findMin^#(@xs) :4

  2: minSort^#(@l) -> c_1(minSort#1^#(findMin(@l)), findMin^#(@l))
     -->_1 minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) :3
     -->_2 findMin^#(@l) -> findMin#1^#(@l) :1

  3: minSort#1^#(::(@x, @xs)) -> minSort^#(@xs)
     -->_1 minSort^#(@l) ->
           c_1(minSort#1^#(findMin(@l)), findMin^#(@l)) :2

  4: findMin#1^#(::(@x, @xs)) -> findMin^#(@xs)
     -->_1 findMin^#(@l) -> findMin#1^#(@l) :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:
  { findMin^#(@l) -> findMin#1^#(@l)
  , minSort^#(@l) -> c_1(minSort#1^#(findMin(@l)), findMin^#(@l)) }
Weak DPs:
  { findMin#1^#(::(@x, @xs)) -> findMin^#(@xs)
  , minSort#1^#(::(@x, @xs)) -> minSort^#(@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()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#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()
    , findMin(@l) -> findMin#1(@l)
    , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
    , findMin#1(nil()) -> nil()
    , findMin#2(::(@y, @ys), @x) ->
      findMin#3(#less(@x, @y), @x, @y, @ys)
    , findMin#2(nil(), @x) -> ::(@x, nil())
    , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
    , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { findMin^#(@l) -> findMin#1^#(@l)
  , minSort^#(@l) -> c_1(minSort#1^#(findMin(@l)), findMin^#(@l)) }
Weak DPs:
  { findMin#1^#(::(@x, @xs)) -> findMin^#(@xs)
  , minSort#1^#(::(@x, @xs)) -> minSort^#(@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()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) }
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: minSort^#(@l) -> c_1(minSort#1^#(findMin(@l)), findMin^#(@l))
  , 3: findMin#1^#(::(@x, @xs)) -> findMin^#(@xs) }
Trs:
  { #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #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() }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(#less) = {}, Uargs(#compare) = {}, Uargs(#cklt) = {},
    Uargs(findMin) = {}, Uargs(findMin#1) = {}, Uargs(::) = {},
    Uargs(findMin#2) = {}, Uargs(findMin#3) = {}, Uargs(#neg) = {},
    Uargs(#pos) = {}, Uargs(#s) = {}, Uargs(#less^#) = {},
    Uargs(#cklt^#) = {}, Uargs(#compare^#) = {}, Uargs(findMin^#) = {},
    Uargs(findMin#1^#) = {}, Uargs(findMin#2^#) = {},
    Uargs(findMin#3^#) = {}, Uargs(minSort^#) = {},
    Uargs(minSort#1^#) = {}, Uargs(c_1) = {1, 2}

  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).

                  [#less](x1, x2) = [2 0] x1 + [1]
                                    [0 0]      [1]

               [#compare](x1, x2) = [1 0] x1 + [1 0] x2 + [2]
                                    [2 1]      [2 1]      [3]

                      [#cklt](x1) = [1]
                                    [1]

                    [findMin](x1) = [1 0] x1 + [0]
                                    [0 1]      [2]

                  [findMin#1](x1) = [1 0] x1 + [0]
                                    [0 1]      [2]

                     [::](x1, x2) = [1 0] x2 + [1]
                                    [1 1]      [1]

              [findMin#2](x1, x2) = [1 0] x1 + [1]
                                    [1 1]      [1]

                            [nil] = [0]
                                    [0]

      [findMin#3](x1, x2, x3, x4) = [0 1] x1 + [1 0] x4 + [1]
                                    [0 0]      [2 1]      [3]

                         [#false] = [1]
                                    [1]

                          [#true] = [1]
                                    [1]

                            [#EQ] = [2]
                                    [1]

                            [#GT] = [1]
                                    [1]

                            [#LT] = [0]
                                    [0]

                             [#0] = [0]
                                    [0]

                       [#neg](x1) = [1 0] x1 + [0]
                                    [0 1]      [1]

                       [#pos](x1) = [1 0] x1 + [1]
                                    [1 1]      [2]

                         [#s](x1) = [1 0] x1 + [0]
                                    [0 1]      [0]

                [#less^#](x1, x2) = [0]
                                    [0]

                    [#cklt^#](x1) = [0]
                                    [0]

             [#compare^#](x1, x2) = [0]
                                    [0]

                  [findMin^#](x1) = [1 0] x1 + [0]
                                    [0 0]      [0]

                [findMin#1^#](x1) = [1 0] x1 + [0]
                                    [0 0]      [0]

            [findMin#2^#](x1, x2) = [0]
                                    [0]

    [findMin#3^#](x1, x2, x3, x4) = [0]
                                    [0]

                  [minSort^#](x1) = [3 1] x1 + [3]
                                    [0 0]      [0]

                [minSort#1^#](x1) = [2 1] x1 + [0]
                                    [0 0]      [0]

                    [c_1](x1, x2) = [1 1] x1 + [1 1] x2 + [0]
                                    [0 0]      [0 0]      [0]

  This order satisfies following ordering constraints

                       [#less(@x, @y)] =  [2 0] @x + [1]
                                          [0 0]      [1]
                                       >= [1]
                                          [1]
                                       =  [#cklt(#compare(@x, @y))]

                [#compare(#0(), #0())] =  [2]
                                          [3]
                                       >= [2]
                                          [1]
                                       =  [#EQ()]

            [#compare(#0(), #neg(@y))] =  [1 0] @y + [2]
                                          [2 1]      [4]
                                       >  [1]
                                          [1]
                                       =  [#GT()]

            [#compare(#0(), #pos(@y))] =  [1 0] @y + [3]
                                          [3 1]      [7]
                                       >  [0]
                                          [0]
                                       =  [#LT()]

              [#compare(#0(), #s(@y))] =  [1 0] @y + [2]
                                          [2 1]      [3]
                                       >  [0]
                                          [0]
                                       =  [#LT()]

            [#compare(#neg(@x), #0())] =  [1 0] @x + [2]
                                          [2 1]      [4]
                                       >  [0]
                                          [0]
                                       =  [#LT()]

        [#compare(#neg(@x), #neg(@y))] =  [1 0] @x + [1 0] @y + [2]
                                          [2 1]      [2 1]      [5]
                                       >= [1 0] @x + [1 0] @y + [2]
                                          [2 1]      [2 1]      [3]
                                       =  [#compare(@y, @x)]

        [#compare(#neg(@x), #pos(@y))] =  [1 0] @x + [1 0] @y + [3]
                                          [2 1]      [3 1]      [8]
                                       >  [0]
                                          [0]
                                       =  [#LT()]

            [#compare(#pos(@x), #0())] =  [1 0] @x + [3]
                                          [3 1]      [7]
                                       >  [1]
                                          [1]
                                       =  [#GT()]

        [#compare(#pos(@x), #neg(@y))] =  [1 0] @x + [1 0] @y + [3]
                                          [3 1]      [2 1]      [8]
                                       >  [1]
                                          [1]
                                       =  [#GT()]

        [#compare(#pos(@x), #pos(@y))] =  [1 0] @x + [1 0] @y + [4]
                                          [3 1]      [3 1]      [11]
                                       >  [1 0] @x + [1 0] @y + [2]
                                          [2 1]      [2 1]      [3]
                                       =  [#compare(@x, @y)]

              [#compare(#s(@x), #0())] =  [1 0] @x + [2]
                                          [2 1]      [3]
                                       >  [1]
                                          [1]
                                       =  [#GT()]

            [#compare(#s(@x), #s(@y))] =  [1 0] @x + [1 0] @y + [2]
                                          [2 1]      [2 1]      [3]
                                       >= [1 0] @x + [1 0] @y + [2]
                                          [2 1]      [2 1]      [3]
                                       =  [#compare(@x, @y)]

                        [#cklt(#EQ())] =  [1]
                                          [1]
                                       >= [1]
                                          [1]
                                       =  [#false()]

                        [#cklt(#GT())] =  [1]
                                          [1]
                                       >= [1]
                                          [1]
                                       =  [#false()]

                        [#cklt(#LT())] =  [1]
                                          [1]
                                       >= [1]
                                          [1]
                                       =  [#true()]

                         [findMin(@l)] =  [1 0] @l + [0]
                                          [0 1]      [2]
                                       >= [1 0] @l + [0]
                                          [0 1]      [2]
                                       =  [findMin#1(@l)]

              [findMin#1(::(@x, @xs))] =  [1 0] @xs + [1]
                                          [1 1]       [3]
                                       >= [1 0] @xs + [1]
                                          [1 1]       [3]
                                       =  [findMin#2(findMin(@xs), @x)]

                    [findMin#1(nil())] =  [0]
                                          [2]
                                       >= [0]
                                          [0]
                                       =  [nil()]

          [findMin#2(::(@y, @ys), @x)] =  [1 0] @ys + [2]
                                          [2 1]       [3]
                                       >= [1 0] @ys + [2]
                                          [2 1]       [3]
                                       =  [findMin#3(#less(@x, @y), @x, @y, @ys)]

                [findMin#2(nil(), @x)] =  [1]
                                          [1]
                                       >= [1]
                                          [1]
                                       =  [::(@x, nil())]

    [findMin#3(#false(), @x, @y, @ys)] =  [1 0] @ys + [2]
                                          [2 1]       [3]
                                       >= [1 0] @ys + [2]
                                          [2 1]       [3]
                                       =  [::(@y, ::(@x, @ys))]

     [findMin#3(#true(), @x, @y, @ys)] =  [1 0] @ys + [2]
                                          [2 1]       [3]
                                       >= [1 0] @ys + [2]
                                          [2 1]       [3]
                                       =  [::(@x, ::(@y, @ys))]

                       [findMin^#(@l)] =  [1 0] @l + [0]
                                          [0 0]      [0]
                                       >= [1 0] @l + [0]
                                          [0 0]      [0]
                                       =  [findMin#1^#(@l)]

            [findMin#1^#(::(@x, @xs))] =  [1 0] @xs + [1]
                                          [0 0]       [0]
                                       >  [1 0] @xs + [0]
                                          [0 0]       [0]
                                       =  [findMin^#(@xs)]

                       [minSort^#(@l)] =  [3 1] @l + [3]
                                          [0 0]      [0]
                                       >  [3 1] @l + [2]
                                          [0 0]      [0]
                                       =  [c_1(minSort#1^#(findMin(@l)), findMin^#(@l))]

            [minSort#1^#(::(@x, @xs))] =  [3 1] @xs + [3]
                                          [0 0]       [0]
                                       >= [3 1] @xs + [3]
                                          [0 0]       [0]
                                       =  [minSort^#(@xs)]


Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^2)) on application of rules {2,3}.
Here rules are labeled according to the (estimated) dependency
graph

  1: findMin^#(@l) -> findMin#1^#(@l)
     -->_1 findMin#1^#(::(@x, @xs)) -> findMin^#(@xs) :3

  2: minSort^#(@l) -> c_1(minSort#1^#(findMin(@l)), findMin^#(@l))
     -->_1 minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) :4
     -->_2 findMin^#(@l) -> findMin#1^#(@l) :1

  3: findMin#1^#(::(@x, @xs)) -> findMin^#(@xs)
     -->_1 findMin^#(@l) -> findMin#1^#(@l) :1

  4: minSort#1^#(::(@x, @xs)) -> minSort^#(@xs)
     -->_1 minSort^#(@l) ->
           c_1(minSort#1^#(findMin(@l)), findMin^#(@l)) :2


- The rules {2,3} have known complexity. These cover all
  predecessors of {1,4}, their complexity is equally bounded.

Overall, we obtain that the number of applications of rules
{1,2,3,4} is given by YES(?,O(n^2)).

We apply the transformation 'removetails' on the sub-problem:

Weak DPs:
  { findMin^#(@l) -> findMin#1^#(@l)
  , findMin#1^#(::(@x, @xs)) -> findMin^#(@xs)
  , minSort^#(@l) -> c_1(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> minSort^#(@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()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) }
StartTerms: basic terms
Strategy: innermost

We consider the the dependency graph

  ->1:{3,4}                                    Weak SCC
     |
     `->2:{1,2}                                Weak SCC


  Here dependency-pairs are as follows:

  Weak DPs:
    { 1: findMin^#(@l) -> findMin#1^#(@l)
    , 2: findMin#1^#(::(@x, @xs)) -> findMin^#(@xs)
    , 3: minSort^#(@l) -> c_1(minSort#1^#(findMin(@l)), findMin^#(@l))
    , 4: minSort#1^#(::(@x, @xs)) -> minSort^#(@xs) }

The following rules are part of trailing weak paths, and thus they
can be removed:

  { 3: minSort^#(@l) -> c_1(minSort#1^#(findMin(@l)), findMin^#(@l))
  , 4: minSort#1^#(::(@x, @xs)) -> minSort^#(@xs)
  , 1: findMin^#(@l) -> findMin#1^#(@l)
  , 2: findMin#1^#(::(@x, @xs)) -> findMin^#(@xs) }

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()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) }
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(1),O(n^2))

tct-popstar

Execution Time (secs)	4.774
Answer	YES(O(1),O(n^2))
Input	minsort.raml