MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { max(nil()) -> 0()
  , max(cons(x, nil())) -> x
  , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs)
  , if1(true(), x, y, xs) -> max(cons(x, xs))
  , if1(false(), x, y, xs) -> max(cons(y, xs))
  , ge(x, 0()) -> true()
  , ge(0(), s(x)) -> false()
  , ge(s(x), s(y)) -> ge(x, y)
  , del(x, nil()) -> nil()
  , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs)
  , if2(true(), x, y, xs) -> xs
  , if2(false(), x, y, xs) -> cons(y, del(x, xs))
  , eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , sort(xs) -> if3(empty(xs), xs)
  , if3(true(), xs) -> nil()
  , if3(false(), xs) -> sort(del(max(xs), xs))
  , empty(nil()) -> true()
  , empty(cons(x, xs)) -> false() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { max^#(nil()) -> c_1()
  , max^#(cons(x, nil())) -> c_2()
  , max^#(cons(x, cons(y, xs))) ->
    c_3(if1^#(ge(x, y), x, y, xs), ge^#(x, y))
  , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs)))
  , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs)))
  , ge^#(x, 0()) -> c_6()
  , ge^#(0(), s(x)) -> c_7()
  , ge^#(s(x), s(y)) -> c_8(ge^#(x, y))
  , del^#(x, nil()) -> c_9()
  , del^#(x, cons(y, xs)) ->
    c_10(if2^#(eq(x, y), x, y, xs), eq^#(x, y))
  , if2^#(true(), x, y, xs) -> c_11()
  , if2^#(false(), x, y, xs) -> c_12(del^#(x, xs))
  , eq^#(0(), 0()) -> c_13()
  , eq^#(0(), s(y)) -> c_14()
  , eq^#(s(x), 0()) -> c_15()
  , eq^#(s(x), s(y)) -> c_16(eq^#(x, y))
  , sort^#(xs) -> c_17(if3^#(empty(xs), xs), empty^#(xs))
  , if3^#(true(), xs) -> c_18()
  , if3^#(false(), xs) ->
    c_19(sort^#(del(max(xs), xs)), del^#(max(xs), xs), max^#(xs))
  , empty^#(nil()) -> c_20()
  , empty^#(cons(x, xs)) -> c_21() }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { max^#(nil()) -> c_1()
  , max^#(cons(x, nil())) -> c_2()
  , max^#(cons(x, cons(y, xs))) ->
    c_3(if1^#(ge(x, y), x, y, xs), ge^#(x, y))
  , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs)))
  , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs)))
  , ge^#(x, 0()) -> c_6()
  , ge^#(0(), s(x)) -> c_7()
  , ge^#(s(x), s(y)) -> c_8(ge^#(x, y))
  , del^#(x, nil()) -> c_9()
  , del^#(x, cons(y, xs)) ->
    c_10(if2^#(eq(x, y), x, y, xs), eq^#(x, y))
  , if2^#(true(), x, y, xs) -> c_11()
  , if2^#(false(), x, y, xs) -> c_12(del^#(x, xs))
  , eq^#(0(), 0()) -> c_13()
  , eq^#(0(), s(y)) -> c_14()
  , eq^#(s(x), 0()) -> c_15()
  , eq^#(s(x), s(y)) -> c_16(eq^#(x, y))
  , sort^#(xs) -> c_17(if3^#(empty(xs), xs), empty^#(xs))
  , if3^#(true(), xs) -> c_18()
  , if3^#(false(), xs) ->
    c_19(sort^#(del(max(xs), xs)), del^#(max(xs), xs), max^#(xs))
  , empty^#(nil()) -> c_20()
  , empty^#(cons(x, xs)) -> c_21() }
Weak Trs:
  { max(nil()) -> 0()
  , max(cons(x, nil())) -> x
  , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs)
  , if1(true(), x, y, xs) -> max(cons(x, xs))
  , if1(false(), x, y, xs) -> max(cons(y, xs))
  , ge(x, 0()) -> true()
  , ge(0(), s(x)) -> false()
  , ge(s(x), s(y)) -> ge(x, y)
  , del(x, nil()) -> nil()
  , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs)
  , if2(true(), x, y, xs) -> xs
  , if2(false(), x, y, xs) -> cons(y, del(x, xs))
  , eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , sort(xs) -> if3(empty(xs), xs)
  , if3(true(), xs) -> nil()
  , if3(false(), xs) -> sort(del(max(xs), xs))
  , empty(nil()) -> true()
  , empty(cons(x, xs)) -> false() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{1,2,6,7,9,11,13,14,15,18,20,21} by applications of
Pre({1,2,6,7,9,11,13,14,15,18,20,21}) = {3,4,5,8,10,12,16,17,19}.
Here rules are labeled as follows:

  DPs:
    { 1: max^#(nil()) -> c_1()
    , 2: max^#(cons(x, nil())) -> c_2()
    , 3: max^#(cons(x, cons(y, xs))) ->
         c_3(if1^#(ge(x, y), x, y, xs), ge^#(x, y))
    , 4: if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs)))
    , 5: if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs)))
    , 6: ge^#(x, 0()) -> c_6()
    , 7: ge^#(0(), s(x)) -> c_7()
    , 8: ge^#(s(x), s(y)) -> c_8(ge^#(x, y))
    , 9: del^#(x, nil()) -> c_9()
    , 10: del^#(x, cons(y, xs)) ->
          c_10(if2^#(eq(x, y), x, y, xs), eq^#(x, y))
    , 11: if2^#(true(), x, y, xs) -> c_11()
    , 12: if2^#(false(), x, y, xs) -> c_12(del^#(x, xs))
    , 13: eq^#(0(), 0()) -> c_13()
    , 14: eq^#(0(), s(y)) -> c_14()
    , 15: eq^#(s(x), 0()) -> c_15()
    , 16: eq^#(s(x), s(y)) -> c_16(eq^#(x, y))
    , 17: sort^#(xs) -> c_17(if3^#(empty(xs), xs), empty^#(xs))
    , 18: if3^#(true(), xs) -> c_18()
    , 19: if3^#(false(), xs) ->
          c_19(sort^#(del(max(xs), xs)), del^#(max(xs), xs), max^#(xs))
    , 20: empty^#(nil()) -> c_20()
    , 21: empty^#(cons(x, xs)) -> c_21() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { max^#(cons(x, cons(y, xs))) ->
    c_3(if1^#(ge(x, y), x, y, xs), ge^#(x, y))
  , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs)))
  , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs)))
  , ge^#(s(x), s(y)) -> c_8(ge^#(x, y))
  , del^#(x, cons(y, xs)) ->
    c_10(if2^#(eq(x, y), x, y, xs), eq^#(x, y))
  , if2^#(false(), x, y, xs) -> c_12(del^#(x, xs))
  , eq^#(s(x), s(y)) -> c_16(eq^#(x, y))
  , sort^#(xs) -> c_17(if3^#(empty(xs), xs), empty^#(xs))
  , if3^#(false(), xs) ->
    c_19(sort^#(del(max(xs), xs)), del^#(max(xs), xs), max^#(xs)) }
Weak DPs:
  { max^#(nil()) -> c_1()
  , max^#(cons(x, nil())) -> c_2()
  , ge^#(x, 0()) -> c_6()
  , ge^#(0(), s(x)) -> c_7()
  , del^#(x, nil()) -> c_9()
  , if2^#(true(), x, y, xs) -> c_11()
  , eq^#(0(), 0()) -> c_13()
  , eq^#(0(), s(y)) -> c_14()
  , eq^#(s(x), 0()) -> c_15()
  , if3^#(true(), xs) -> c_18()
  , empty^#(nil()) -> c_20()
  , empty^#(cons(x, xs)) -> c_21() }
Weak Trs:
  { max(nil()) -> 0()
  , max(cons(x, nil())) -> x
  , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs)
  , if1(true(), x, y, xs) -> max(cons(x, xs))
  , if1(false(), x, y, xs) -> max(cons(y, xs))
  , ge(x, 0()) -> true()
  , ge(0(), s(x)) -> false()
  , ge(s(x), s(y)) -> ge(x, y)
  , del(x, nil()) -> nil()
  , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs)
  , if2(true(), x, y, xs) -> xs
  , if2(false(), x, y, xs) -> cons(y, del(x, xs))
  , eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , sort(xs) -> if3(empty(xs), xs)
  , if3(true(), xs) -> nil()
  , if3(false(), xs) -> sort(del(max(xs), xs))
  , empty(nil()) -> true()
  , empty(cons(x, xs)) -> false() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ max^#(nil()) -> c_1()
, max^#(cons(x, nil())) -> c_2()
, ge^#(x, 0()) -> c_6()
, ge^#(0(), s(x)) -> c_7()
, del^#(x, nil()) -> c_9()
, if2^#(true(), x, y, xs) -> c_11()
, eq^#(0(), 0()) -> c_13()
, eq^#(0(), s(y)) -> c_14()
, eq^#(s(x), 0()) -> c_15()
, if3^#(true(), xs) -> c_18()
, empty^#(nil()) -> c_20()
, empty^#(cons(x, xs)) -> c_21() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { max^#(cons(x, cons(y, xs))) ->
    c_3(if1^#(ge(x, y), x, y, xs), ge^#(x, y))
  , if1^#(true(), x, y, xs) -> c_4(max^#(cons(x, xs)))
  , if1^#(false(), x, y, xs) -> c_5(max^#(cons(y, xs)))
  , ge^#(s(x), s(y)) -> c_8(ge^#(x, y))
  , del^#(x, cons(y, xs)) ->
    c_10(if2^#(eq(x, y), x, y, xs), eq^#(x, y))
  , if2^#(false(), x, y, xs) -> c_12(del^#(x, xs))
  , eq^#(s(x), s(y)) -> c_16(eq^#(x, y))
  , sort^#(xs) -> c_17(if3^#(empty(xs), xs), empty^#(xs))
  , if3^#(false(), xs) ->
    c_19(sort^#(del(max(xs), xs)), del^#(max(xs), xs), max^#(xs)) }
Weak Trs:
  { max(nil()) -> 0()
  , max(cons(x, nil())) -> x
  , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs)
  , if1(true(), x, y, xs) -> max(cons(x, xs))
  , if1(false(), x, y, xs) -> max(cons(y, xs))
  , ge(x, 0()) -> true()
  , ge(0(), s(x)) -> false()
  , ge(s(x), s(y)) -> ge(x, y)
  , del(x, nil()) -> nil()
  , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs)
  , if2(true(), x, y, xs) -> xs
  , if2(false(), x, y, xs) -> cons(y, del(x, xs))
  , eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , sort(xs) -> if3(empty(xs), xs)
  , if3(true(), xs) -> nil()
  , if3(false(), xs) -> sort(del(max(xs), xs))
  , empty(nil()) -> true()
  , empty(cons(x, xs)) -> false() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { sort^#(xs) -> c_17(if3^#(empty(xs), xs), empty^#(xs)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { max^#(cons(x, cons(y, xs))) ->
    c_1(if1^#(ge(x, y), x, y, xs), ge^#(x, y))
  , if1^#(true(), x, y, xs) -> c_2(max^#(cons(x, xs)))
  , if1^#(false(), x, y, xs) -> c_3(max^#(cons(y, xs)))
  , ge^#(s(x), s(y)) -> c_4(ge^#(x, y))
  , del^#(x, cons(y, xs)) ->
    c_5(if2^#(eq(x, y), x, y, xs), eq^#(x, y))
  , if2^#(false(), x, y, xs) -> c_6(del^#(x, xs))
  , eq^#(s(x), s(y)) -> c_7(eq^#(x, y))
  , sort^#(xs) -> c_8(if3^#(empty(xs), xs))
  , if3^#(false(), xs) ->
    c_9(sort^#(del(max(xs), xs)), del^#(max(xs), xs), max^#(xs)) }
Weak Trs:
  { max(nil()) -> 0()
  , max(cons(x, nil())) -> x
  , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs)
  , if1(true(), x, y, xs) -> max(cons(x, xs))
  , if1(false(), x, y, xs) -> max(cons(y, xs))
  , ge(x, 0()) -> true()
  , ge(0(), s(x)) -> false()
  , ge(s(x), s(y)) -> ge(x, y)
  , del(x, nil()) -> nil()
  , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs)
  , if2(true(), x, y, xs) -> xs
  , if2(false(), x, y, xs) -> cons(y, del(x, xs))
  , eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , sort(xs) -> if3(empty(xs), xs)
  , if3(true(), xs) -> nil()
  , if3(false(), xs) -> sort(del(max(xs), xs))
  , empty(nil()) -> true()
  , empty(cons(x, xs)) -> false() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { max(nil()) -> 0()
    , max(cons(x, nil())) -> x
    , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs)
    , if1(true(), x, y, xs) -> max(cons(x, xs))
    , if1(false(), x, y, xs) -> max(cons(y, xs))
    , ge(x, 0()) -> true()
    , ge(0(), s(x)) -> false()
    , ge(s(x), s(y)) -> ge(x, y)
    , del(x, nil()) -> nil()
    , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs)
    , if2(true(), x, y, xs) -> xs
    , if2(false(), x, y, xs) -> cons(y, del(x, xs))
    , eq(0(), 0()) -> true()
    , eq(0(), s(y)) -> false()
    , eq(s(x), 0()) -> false()
    , eq(s(x), s(y)) -> eq(x, y)
    , empty(nil()) -> true()
    , empty(cons(x, xs)) -> false() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { max^#(cons(x, cons(y, xs))) ->
    c_1(if1^#(ge(x, y), x, y, xs), ge^#(x, y))
  , if1^#(true(), x, y, xs) -> c_2(max^#(cons(x, xs)))
  , if1^#(false(), x, y, xs) -> c_3(max^#(cons(y, xs)))
  , ge^#(s(x), s(y)) -> c_4(ge^#(x, y))
  , del^#(x, cons(y, xs)) ->
    c_5(if2^#(eq(x, y), x, y, xs), eq^#(x, y))
  , if2^#(false(), x, y, xs) -> c_6(del^#(x, xs))
  , eq^#(s(x), s(y)) -> c_7(eq^#(x, y))
  , sort^#(xs) -> c_8(if3^#(empty(xs), xs))
  , if3^#(false(), xs) ->
    c_9(sort^#(del(max(xs), xs)), del^#(max(xs), xs), max^#(xs)) }
Weak Trs:
  { max(nil()) -> 0()
  , max(cons(x, nil())) -> x
  , max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs)
  , if1(true(), x, y, xs) -> max(cons(x, xs))
  , if1(false(), x, y, xs) -> max(cons(y, xs))
  , ge(x, 0()) -> true()
  , ge(0(), s(x)) -> false()
  , ge(s(x), s(y)) -> ge(x, y)
  , del(x, nil()) -> nil()
  , del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs)
  , if2(true(), x, y, xs) -> xs
  , if2(false(), x, y, xs) -> cons(y, del(x, xs))
  , eq(0(), 0()) -> true()
  , eq(0(), s(y)) -> false()
  , eq(s(x), 0()) -> false()
  , eq(s(x), s(y)) -> eq(x, y)
  , empty(nil()) -> true()
  , empty(cons(x, xs)) -> false() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'matrices' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      Following exception was raised:
        stack overflow
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   

2) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.


Arrrr..