MAYBE

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

Strict Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(m)) -> false()
  , eq(s(n), 0()) -> false()
  , eq(s(n), s(m)) -> eq(n, m)
  , le(0(), m) -> true()
  , le(s(n), 0()) -> false()
  , le(s(n), s(m)) -> le(n, m)
  , min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
  , min(cons(0(), nil())) -> 0()
  , min(cons(s(n), nil())) -> s(n)
  , if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x))
  , if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x))
  , replace(n, m, cons(k, x)) ->
    if_replace(eq(n, k), n, m, cons(k, x))
  , replace(n, m, nil()) -> nil()
  , if_replace(true(), n, m, cons(k, x)) -> cons(m, x)
  , if_replace(false(), n, m, cons(k, x)) ->
    cons(k, replace(n, m, x))
  , sort(cons(n, x)) ->
    cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))
  , sort(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { eq^#(0(), 0()) -> c_1()
  , eq^#(0(), s(m)) -> c_2()
  , eq^#(s(n), 0()) -> c_3()
  , eq^#(s(n), s(m)) -> c_4(eq^#(n, m))
  , le^#(0(), m) -> c_5()
  , le^#(s(n), 0()) -> c_6()
  , le^#(s(n), s(m)) -> c_7(le^#(n, m))
  , min^#(cons(n, cons(m, x))) ->
    c_8(if_min^#(le(n, m), cons(n, cons(m, x))), le^#(n, m))
  , min^#(cons(0(), nil())) -> c_9()
  , min^#(cons(s(n), nil())) -> c_10()
  , if_min^#(true(), cons(n, cons(m, x))) -> c_11(min^#(cons(n, x)))
  , if_min^#(false(), cons(n, cons(m, x))) -> c_12(min^#(cons(m, x)))
  , replace^#(n, m, cons(k, x)) ->
    c_13(if_replace^#(eq(n, k), n, m, cons(k, x)), eq^#(n, k))
  , replace^#(n, m, nil()) -> c_14()
  , if_replace^#(true(), n, m, cons(k, x)) -> c_15()
  , if_replace^#(false(), n, m, cons(k, x)) ->
    c_16(replace^#(n, m, x))
  , sort^#(cons(n, x)) ->
    c_17(min^#(cons(n, x)),
         sort^#(replace(min(cons(n, x)), n, x)),
         replace^#(min(cons(n, x)), n, x),
         min^#(cons(n, x)))
  , sort^#(nil()) -> c_18() }

and mark the set of starting terms.

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

Strict DPs:
  { eq^#(0(), 0()) -> c_1()
  , eq^#(0(), s(m)) -> c_2()
  , eq^#(s(n), 0()) -> c_3()
  , eq^#(s(n), s(m)) -> c_4(eq^#(n, m))
  , le^#(0(), m) -> c_5()
  , le^#(s(n), 0()) -> c_6()
  , le^#(s(n), s(m)) -> c_7(le^#(n, m))
  , min^#(cons(n, cons(m, x))) ->
    c_8(if_min^#(le(n, m), cons(n, cons(m, x))), le^#(n, m))
  , min^#(cons(0(), nil())) -> c_9()
  , min^#(cons(s(n), nil())) -> c_10()
  , if_min^#(true(), cons(n, cons(m, x))) -> c_11(min^#(cons(n, x)))
  , if_min^#(false(), cons(n, cons(m, x))) -> c_12(min^#(cons(m, x)))
  , replace^#(n, m, cons(k, x)) ->
    c_13(if_replace^#(eq(n, k), n, m, cons(k, x)), eq^#(n, k))
  , replace^#(n, m, nil()) -> c_14()
  , if_replace^#(true(), n, m, cons(k, x)) -> c_15()
  , if_replace^#(false(), n, m, cons(k, x)) ->
    c_16(replace^#(n, m, x))
  , sort^#(cons(n, x)) ->
    c_17(min^#(cons(n, x)),
         sort^#(replace(min(cons(n, x)), n, x)),
         replace^#(min(cons(n, x)), n, x),
         min^#(cons(n, x)))
  , sort^#(nil()) -> c_18() }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(m)) -> false()
  , eq(s(n), 0()) -> false()
  , eq(s(n), s(m)) -> eq(n, m)
  , le(0(), m) -> true()
  , le(s(n), 0()) -> false()
  , le(s(n), s(m)) -> le(n, m)
  , min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
  , min(cons(0(), nil())) -> 0()
  , min(cons(s(n), nil())) -> s(n)
  , if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x))
  , if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x))
  , replace(n, m, cons(k, x)) ->
    if_replace(eq(n, k), n, m, cons(k, x))
  , replace(n, m, nil()) -> nil()
  , if_replace(true(), n, m, cons(k, x)) -> cons(m, x)
  , if_replace(false(), n, m, cons(k, x)) ->
    cons(k, replace(n, m, x))
  , sort(cons(n, x)) ->
    cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))
  , sort(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: eq^#(0(), 0()) -> c_1()
    , 2: eq^#(0(), s(m)) -> c_2()
    , 3: eq^#(s(n), 0()) -> c_3()
    , 4: eq^#(s(n), s(m)) -> c_4(eq^#(n, m))
    , 5: le^#(0(), m) -> c_5()
    , 6: le^#(s(n), 0()) -> c_6()
    , 7: le^#(s(n), s(m)) -> c_7(le^#(n, m))
    , 8: min^#(cons(n, cons(m, x))) ->
         c_8(if_min^#(le(n, m), cons(n, cons(m, x))), le^#(n, m))
    , 9: min^#(cons(0(), nil())) -> c_9()
    , 10: min^#(cons(s(n), nil())) -> c_10()
    , 11: if_min^#(true(), cons(n, cons(m, x))) ->
          c_11(min^#(cons(n, x)))
    , 12: if_min^#(false(), cons(n, cons(m, x))) ->
          c_12(min^#(cons(m, x)))
    , 13: replace^#(n, m, cons(k, x)) ->
          c_13(if_replace^#(eq(n, k), n, m, cons(k, x)), eq^#(n, k))
    , 14: replace^#(n, m, nil()) -> c_14()
    , 15: if_replace^#(true(), n, m, cons(k, x)) -> c_15()
    , 16: if_replace^#(false(), n, m, cons(k, x)) ->
          c_16(replace^#(n, m, x))
    , 17: sort^#(cons(n, x)) ->
          c_17(min^#(cons(n, x)),
               sort^#(replace(min(cons(n, x)), n, x)),
               replace^#(min(cons(n, x)), n, x),
               min^#(cons(n, x)))
    , 18: sort^#(nil()) -> c_18() }

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

Strict DPs:
  { eq^#(s(n), s(m)) -> c_4(eq^#(n, m))
  , le^#(s(n), s(m)) -> c_7(le^#(n, m))
  , min^#(cons(n, cons(m, x))) ->
    c_8(if_min^#(le(n, m), cons(n, cons(m, x))), le^#(n, m))
  , if_min^#(true(), cons(n, cons(m, x))) -> c_11(min^#(cons(n, x)))
  , if_min^#(false(), cons(n, cons(m, x))) -> c_12(min^#(cons(m, x)))
  , replace^#(n, m, cons(k, x)) ->
    c_13(if_replace^#(eq(n, k), n, m, cons(k, x)), eq^#(n, k))
  , if_replace^#(false(), n, m, cons(k, x)) ->
    c_16(replace^#(n, m, x))
  , sort^#(cons(n, x)) ->
    c_17(min^#(cons(n, x)),
         sort^#(replace(min(cons(n, x)), n, x)),
         replace^#(min(cons(n, x)), n, x),
         min^#(cons(n, x))) }
Weak DPs:
  { eq^#(0(), 0()) -> c_1()
  , eq^#(0(), s(m)) -> c_2()
  , eq^#(s(n), 0()) -> c_3()
  , le^#(0(), m) -> c_5()
  , le^#(s(n), 0()) -> c_6()
  , min^#(cons(0(), nil())) -> c_9()
  , min^#(cons(s(n), nil())) -> c_10()
  , replace^#(n, m, nil()) -> c_14()
  , if_replace^#(true(), n, m, cons(k, x)) -> c_15()
  , sort^#(nil()) -> c_18() }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(m)) -> false()
  , eq(s(n), 0()) -> false()
  , eq(s(n), s(m)) -> eq(n, m)
  , le(0(), m) -> true()
  , le(s(n), 0()) -> false()
  , le(s(n), s(m)) -> le(n, m)
  , min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
  , min(cons(0(), nil())) -> 0()
  , min(cons(s(n), nil())) -> s(n)
  , if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x))
  , if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x))
  , replace(n, m, cons(k, x)) ->
    if_replace(eq(n, k), n, m, cons(k, x))
  , replace(n, m, nil()) -> nil()
  , if_replace(true(), n, m, cons(k, x)) -> cons(m, x)
  , if_replace(false(), n, m, cons(k, x)) ->
    cons(k, replace(n, m, x))
  , sort(cons(n, x)) ->
    cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))
  , sort(nil()) -> nil() }
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.

{ eq^#(0(), 0()) -> c_1()
, eq^#(0(), s(m)) -> c_2()
, eq^#(s(n), 0()) -> c_3()
, le^#(0(), m) -> c_5()
, le^#(s(n), 0()) -> c_6()
, min^#(cons(0(), nil())) -> c_9()
, min^#(cons(s(n), nil())) -> c_10()
, replace^#(n, m, nil()) -> c_14()
, if_replace^#(true(), n, m, cons(k, x)) -> c_15()
, sort^#(nil()) -> c_18() }

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

Strict DPs:
  { eq^#(s(n), s(m)) -> c_4(eq^#(n, m))
  , le^#(s(n), s(m)) -> c_7(le^#(n, m))
  , min^#(cons(n, cons(m, x))) ->
    c_8(if_min^#(le(n, m), cons(n, cons(m, x))), le^#(n, m))
  , if_min^#(true(), cons(n, cons(m, x))) -> c_11(min^#(cons(n, x)))
  , if_min^#(false(), cons(n, cons(m, x))) -> c_12(min^#(cons(m, x)))
  , replace^#(n, m, cons(k, x)) ->
    c_13(if_replace^#(eq(n, k), n, m, cons(k, x)), eq^#(n, k))
  , if_replace^#(false(), n, m, cons(k, x)) ->
    c_16(replace^#(n, m, x))
  , sort^#(cons(n, x)) ->
    c_17(min^#(cons(n, x)),
         sort^#(replace(min(cons(n, x)), n, x)),
         replace^#(min(cons(n, x)), n, x),
         min^#(cons(n, x))) }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(m)) -> false()
  , eq(s(n), 0()) -> false()
  , eq(s(n), s(m)) -> eq(n, m)
  , le(0(), m) -> true()
  , le(s(n), 0()) -> false()
  , le(s(n), s(m)) -> le(n, m)
  , min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
  , min(cons(0(), nil())) -> 0()
  , min(cons(s(n), nil())) -> s(n)
  , if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x))
  , if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x))
  , replace(n, m, cons(k, x)) ->
    if_replace(eq(n, k), n, m, cons(k, x))
  , replace(n, m, nil()) -> nil()
  , if_replace(true(), n, m, cons(k, x)) -> cons(m, x)
  , if_replace(false(), n, m, cons(k, x)) ->
    cons(k, replace(n, m, x))
  , sort(cons(n, x)) ->
    cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))
  , sort(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { eq(0(), 0()) -> true()
    , eq(0(), s(m)) -> false()
    , eq(s(n), 0()) -> false()
    , eq(s(n), s(m)) -> eq(n, m)
    , le(0(), m) -> true()
    , le(s(n), 0()) -> false()
    , le(s(n), s(m)) -> le(n, m)
    , min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
    , min(cons(0(), nil())) -> 0()
    , min(cons(s(n), nil())) -> s(n)
    , if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x))
    , if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x))
    , replace(n, m, cons(k, x)) ->
      if_replace(eq(n, k), n, m, cons(k, x))
    , replace(n, m, nil()) -> nil()
    , if_replace(true(), n, m, cons(k, x)) -> cons(m, x)
    , if_replace(false(), n, m, cons(k, x)) ->
      cons(k, replace(n, m, x)) }

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

Strict DPs:
  { eq^#(s(n), s(m)) -> c_4(eq^#(n, m))
  , le^#(s(n), s(m)) -> c_7(le^#(n, m))
  , min^#(cons(n, cons(m, x))) ->
    c_8(if_min^#(le(n, m), cons(n, cons(m, x))), le^#(n, m))
  , if_min^#(true(), cons(n, cons(m, x))) -> c_11(min^#(cons(n, x)))
  , if_min^#(false(), cons(n, cons(m, x))) -> c_12(min^#(cons(m, x)))
  , replace^#(n, m, cons(k, x)) ->
    c_13(if_replace^#(eq(n, k), n, m, cons(k, x)), eq^#(n, k))
  , if_replace^#(false(), n, m, cons(k, x)) ->
    c_16(replace^#(n, m, x))
  , sort^#(cons(n, x)) ->
    c_17(min^#(cons(n, x)),
         sort^#(replace(min(cons(n, x)), n, x)),
         replace^#(min(cons(n, x)), n, x),
         min^#(cons(n, x))) }
Weak Trs:
  { eq(0(), 0()) -> true()
  , eq(0(), s(m)) -> false()
  , eq(s(n), 0()) -> false()
  , eq(s(n), s(m)) -> eq(n, m)
  , le(0(), m) -> true()
  , le(s(n), 0()) -> false()
  , le(s(n), s(m)) -> le(n, m)
  , min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
  , min(cons(0(), nil())) -> 0()
  , min(cons(s(n), nil())) -> s(n)
  , if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x))
  , if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x))
  , replace(n, m, cons(k, x)) ->
    if_replace(eq(n, k), n, m, cons(k, x))
  , replace(n, m, nil()) -> nil()
  , if_replace(true(), n, m, cons(k, x)) -> cons(m, x)
  , if_replace(false(), n, m, cons(k, x)) ->
    cons(k, replace(n, m, x)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..