MAYBE

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

Strict Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , quot(0(), s(y)) -> 0()
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(nil()) -> nil()
  , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y))
  , less_leaves(x, leaf()) -> false()
  , less_leaves(leaf(), cons(w, z)) -> true()
  , less_leaves(cons(u, v), cons(w, z)) ->
    less_leaves(concat(u, v), concat(w, z)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { minus^#(x, 0()) -> c_1()
  , minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(0(), s(y)) -> c_3()
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(nil(), y) -> c_5()
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(nil()) -> c_7()
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(nil()) -> c_9()
  , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x))
  , concat^#(leaf(), y) -> c_11()
  , concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , less_leaves^#(x, leaf()) -> c_13()
  , less_leaves^#(leaf(), cons(w, z)) -> c_14()
  , less_leaves^#(cons(u, v), cons(w, z)) ->
    c_15(less_leaves^#(concat(u, v), concat(w, z)),
         concat^#(u, v),
         concat^#(w, z)) }

and mark the set of starting terms.

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

Strict DPs:
  { minus^#(x, 0()) -> c_1()
  , minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(0(), s(y)) -> c_3()
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(nil(), y) -> c_5()
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(nil()) -> c_7()
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(nil()) -> c_9()
  , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x))
  , concat^#(leaf(), y) -> c_11()
  , concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , less_leaves^#(x, leaf()) -> c_13()
  , less_leaves^#(leaf(), cons(w, z)) -> c_14()
  , less_leaves^#(cons(u, v), cons(w, z)) ->
    c_15(less_leaves^#(concat(u, v), concat(w, z)),
         concat^#(u, v),
         concat^#(w, z)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , quot(0(), s(y)) -> 0()
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(nil()) -> nil()
  , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y))
  , less_leaves(x, leaf()) -> false()
  , less_leaves(leaf(), cons(w, z)) -> true()
  , less_leaves(cons(u, v), cons(w, z)) ->
    less_leaves(concat(u, v), concat(w, z)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: minus^#(x, 0()) -> c_1()
    , 2: minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
    , 3: quot^#(0(), s(y)) -> c_3()
    , 4: quot^#(s(x), s(y)) ->
         c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
    , 5: app^#(nil(), y) -> c_5()
    , 6: app^#(add(n, x), y) -> c_6(app^#(x, y))
    , 7: reverse^#(nil()) -> c_7()
    , 8: reverse^#(add(n, x)) ->
         c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
    , 9: shuffle^#(nil()) -> c_9()
    , 10: shuffle^#(add(n, x)) ->
          c_10(shuffle^#(reverse(x)), reverse^#(x))
    , 11: concat^#(leaf(), y) -> c_11()
    , 12: concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
    , 13: less_leaves^#(x, leaf()) -> c_13()
    , 14: less_leaves^#(leaf(), cons(w, z)) -> c_14()
    , 15: less_leaves^#(cons(u, v), cons(w, z)) ->
          c_15(less_leaves^#(concat(u, v), concat(w, z)),
               concat^#(u, v),
               concat^#(w, z)) }

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

Strict DPs:
  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x))
  , concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , less_leaves^#(cons(u, v), cons(w, z)) ->
    c_15(less_leaves^#(concat(u, v), concat(w, z)),
         concat^#(u, v),
         concat^#(w, z)) }
Weak DPs:
  { minus^#(x, 0()) -> c_1()
  , quot^#(0(), s(y)) -> c_3()
  , app^#(nil(), y) -> c_5()
  , reverse^#(nil()) -> c_7()
  , shuffle^#(nil()) -> c_9()
  , concat^#(leaf(), y) -> c_11()
  , less_leaves^#(x, leaf()) -> c_13()
  , less_leaves^#(leaf(), cons(w, z)) -> c_14() }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , quot(0(), s(y)) -> 0()
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(nil()) -> nil()
  , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y))
  , less_leaves(x, leaf()) -> false()
  , less_leaves(leaf(), cons(w, z)) -> true()
  , less_leaves(cons(u, v), cons(w, z)) ->
    less_leaves(concat(u, v), concat(w, z)) }
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.

{ minus^#(x, 0()) -> c_1()
, quot^#(0(), s(y)) -> c_3()
, app^#(nil(), y) -> c_5()
, reverse^#(nil()) -> c_7()
, shuffle^#(nil()) -> c_9()
, concat^#(leaf(), y) -> c_11()
, less_leaves^#(x, leaf()) -> c_13()
, less_leaves^#(leaf(), cons(w, z)) -> c_14() }

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

Strict DPs:
  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x))
  , concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , less_leaves^#(cons(u, v), cons(w, z)) ->
    c_15(less_leaves^#(concat(u, v), concat(w, z)),
         concat^#(u, v),
         concat^#(w, z)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , quot(0(), s(y)) -> 0()
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(nil()) -> nil()
  , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y))
  , less_leaves(x, leaf()) -> false()
  , less_leaves(leaf(), cons(w, z)) -> true()
  , less_leaves(cons(u, v), cons(w, z)) ->
    less_leaves(concat(u, v), concat(w, z)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { minus(x, 0()) -> x
    , minus(s(x), s(y)) -> minus(x, y)
    , app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
    , concat(leaf(), y) -> y
    , concat(cons(u, v), y) -> cons(u, concat(v, y)) }

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

Strict DPs:
  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x))
  , concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , less_leaves^#(cons(u, v), cons(w, z)) ->
    c_15(less_leaves^#(concat(u, v), concat(w, z)),
         concat^#(u, v),
         concat^#(w, z)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..