MAYBE

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

Strict Trs:
  { bsort(nil()) -> nil()
  , bsort(.(x, y)) ->
    last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
  , last(nil()) -> 0()
  , last(.(x, nil())) -> x
  , last(.(x, .(y, z))) -> last(.(y, z))
  , bubble(nil()) -> nil()
  , bubble(.(x, nil())) -> .(x, nil())
  , bubble(.(x, .(y, z))) ->
    if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
  , butlast(nil()) -> nil()
  , butlast(.(x, nil())) -> nil()
  , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { bsort^#(nil()) -> c_1()
  , bsort^#(.(x, y)) ->
    c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))),
        bubble^#(.(x, y)),
        bsort^#(butlast(bubble(.(x, y)))),
        butlast^#(bubble(.(x, y))),
        bubble^#(.(x, y)))
  , last^#(nil()) -> c_3()
  , last^#(.(x, nil())) -> c_4()
  , last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z)))
  , bubble^#(nil()) -> c_6()
  , bubble^#(.(x, nil())) -> c_7()
  , bubble^#(.(x, .(y, z))) ->
    c_8(bubble^#(.(x, z)), bubble^#(.(y, z)))
  , butlast^#(nil()) -> c_9()
  , butlast^#(.(x, nil())) -> c_10()
  , butlast^#(.(x, .(y, z))) -> c_11(butlast^#(.(y, z))) }

and mark the set of starting terms.

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

Strict DPs:
  { bsort^#(nil()) -> c_1()
  , bsort^#(.(x, y)) ->
    c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))),
        bubble^#(.(x, y)),
        bsort^#(butlast(bubble(.(x, y)))),
        butlast^#(bubble(.(x, y))),
        bubble^#(.(x, y)))
  , last^#(nil()) -> c_3()
  , last^#(.(x, nil())) -> c_4()
  , last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z)))
  , bubble^#(nil()) -> c_6()
  , bubble^#(.(x, nil())) -> c_7()
  , bubble^#(.(x, .(y, z))) ->
    c_8(bubble^#(.(x, z)), bubble^#(.(y, z)))
  , butlast^#(nil()) -> c_9()
  , butlast^#(.(x, nil())) -> c_10()
  , butlast^#(.(x, .(y, z))) -> c_11(butlast^#(.(y, z))) }
Weak Trs:
  { bsort(nil()) -> nil()
  , bsort(.(x, y)) ->
    last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
  , last(nil()) -> 0()
  , last(.(x, nil())) -> x
  , last(.(x, .(y, z))) -> last(.(y, z))
  , bubble(nil()) -> nil()
  , bubble(.(x, nil())) -> .(x, nil())
  , bubble(.(x, .(y, z))) ->
    if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
  , butlast(nil()) -> nil()
  , butlast(.(x, nil())) -> nil()
  , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: bsort^#(nil()) -> c_1()
    , 2: bsort^#(.(x, y)) ->
         c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))),
             bubble^#(.(x, y)),
             bsort^#(butlast(bubble(.(x, y)))),
             butlast^#(bubble(.(x, y))),
             bubble^#(.(x, y)))
    , 3: last^#(nil()) -> c_3()
    , 4: last^#(.(x, nil())) -> c_4()
    , 5: last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z)))
    , 6: bubble^#(nil()) -> c_6()
    , 7: bubble^#(.(x, nil())) -> c_7()
    , 8: bubble^#(.(x, .(y, z))) ->
         c_8(bubble^#(.(x, z)), bubble^#(.(y, z)))
    , 9: butlast^#(nil()) -> c_9()
    , 10: butlast^#(.(x, nil())) -> c_10()
    , 11: butlast^#(.(x, .(y, z))) -> c_11(butlast^#(.(y, z))) }

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

Strict DPs:
  { bsort^#(.(x, y)) ->
    c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))),
        bubble^#(.(x, y)),
        bsort^#(butlast(bubble(.(x, y)))),
        butlast^#(bubble(.(x, y))),
        bubble^#(.(x, y)))
  , last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z)))
  , bubble^#(.(x, .(y, z))) ->
    c_8(bubble^#(.(x, z)), bubble^#(.(y, z)))
  , butlast^#(.(x, .(y, z))) -> c_11(butlast^#(.(y, z))) }
Weak DPs:
  { bsort^#(nil()) -> c_1()
  , last^#(nil()) -> c_3()
  , last^#(.(x, nil())) -> c_4()
  , bubble^#(nil()) -> c_6()
  , bubble^#(.(x, nil())) -> c_7()
  , butlast^#(nil()) -> c_9()
  , butlast^#(.(x, nil())) -> c_10() }
Weak Trs:
  { bsort(nil()) -> nil()
  , bsort(.(x, y)) ->
    last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
  , last(nil()) -> 0()
  , last(.(x, nil())) -> x
  , last(.(x, .(y, z))) -> last(.(y, z))
  , bubble(nil()) -> nil()
  , bubble(.(x, nil())) -> .(x, nil())
  , bubble(.(x, .(y, z))) ->
    if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
  , butlast(nil()) -> nil()
  , butlast(.(x, nil())) -> nil()
  , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, 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.

{ bsort^#(nil()) -> c_1()
, last^#(nil()) -> c_3()
, last^#(.(x, nil())) -> c_4()
, bubble^#(nil()) -> c_6()
, bubble^#(.(x, nil())) -> c_7()
, butlast^#(nil()) -> c_9()
, butlast^#(.(x, nil())) -> c_10() }

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

Strict DPs:
  { bsort^#(.(x, y)) ->
    c_2(last^#(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y)))))),
        bubble^#(.(x, y)),
        bsort^#(butlast(bubble(.(x, y)))),
        butlast^#(bubble(.(x, y))),
        bubble^#(.(x, y)))
  , last^#(.(x, .(y, z))) -> c_5(last^#(.(y, z)))
  , bubble^#(.(x, .(y, z))) ->
    c_8(bubble^#(.(x, z)), bubble^#(.(y, z)))
  , butlast^#(.(x, .(y, z))) -> c_11(butlast^#(.(y, z))) }
Weak Trs:
  { bsort(nil()) -> nil()
  , bsort(.(x, y)) ->
    last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
  , last(nil()) -> 0()
  , last(.(x, nil())) -> x
  , last(.(x, .(y, z))) -> last(.(y, z))
  , bubble(nil()) -> nil()
  , bubble(.(x, nil())) -> .(x, nil())
  , bubble(.(x, .(y, z))) ->
    if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
  , butlast(nil()) -> nil()
  , butlast(.(x, nil())) -> nil()
  , butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..