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

Strict Trs:
  { bubble(x, Nil()) -> Cons(x, Nil())
  , bubble(x', Cons(x, xs)) ->
    bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
  , bsort(S(x'), Cons(x, xs)) -> bsort(x', bubble(x, xs))
  , bsort(0(), xs) -> xs
  , bubblesort(xs) -> bsort(len(xs), xs)
  , len(Nil()) -> 0()
  , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
Weak Trs:
  { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
    Cons(x', bubble(x, xs))
  , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
    Cons(x, bubble(x', xs))
  , +(x, S(0())) -> S(x)
  , +(S(0()), y) -> S(y)
  , <(x, 0()) -> False()
  , <(S(x), S(y)) -> <(x, y)
  , <(0(), S(y)) -> True() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We add the following dependency tuples:

Strict DPs:
  { bubble^#(x, Nil()) -> c_1()
  , bubble^#(x', Cons(x, xs)) ->
    c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
        <^#(x', x))
  , bsort^#(S(x'), Cons(x, xs)) ->
    c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
  , bsort^#(0(), xs) -> c_4()
  , bubblesort^#(xs) -> c_5(bsort^#(len(xs), xs), len^#(xs))
  , len^#(Nil()) -> c_6()
  , len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs)) }
Weak DPs:
  { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
    c_8(bubble^#(x, xs))
  , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
    c_9(bubble^#(x', xs))
  , <^#(x, 0()) -> c_12()
  , <^#(S(x), S(y)) -> c_13(<^#(x, y))
  , <^#(0(), S(y)) -> c_14()
  , +^#(x, S(0())) -> c_10()
  , +^#(S(0()), y) -> c_11() }

and mark the set of starting terms.

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

Strict DPs:
  { bubble^#(x, Nil()) -> c_1()
  , bubble^#(x', Cons(x, xs)) ->
    c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
        <^#(x', x))
  , bsort^#(S(x'), Cons(x, xs)) ->
    c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
  , bsort^#(0(), xs) -> c_4()
  , bubblesort^#(xs) -> c_5(bsort^#(len(xs), xs), len^#(xs))
  , len^#(Nil()) -> c_6()
  , len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs)) }
Weak DPs:
  { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
    c_8(bubble^#(x, xs))
  , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
    c_9(bubble^#(x', xs))
  , <^#(x, 0()) -> c_12()
  , <^#(S(x), S(y)) -> c_13(<^#(x, y))
  , <^#(0(), S(y)) -> c_14()
  , +^#(x, S(0())) -> c_10()
  , +^#(S(0()), y) -> c_11() }
Weak Trs:
  { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
    Cons(x', bubble(x, xs))
  , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
    Cons(x, bubble(x', xs))
  , bubble(x, Nil()) -> Cons(x, Nil())
  , bubble(x', Cons(x, xs)) ->
    bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
  , +(x, S(0())) -> S(x)
  , +(S(0()), y) -> S(y)
  , <(x, 0()) -> False()
  , <(S(x), S(y)) -> <(x, y)
  , <(0(), S(y)) -> True()
  , bsort(S(x'), Cons(x, xs)) -> bsort(x', bubble(x, xs))
  , bsort(0(), xs) -> xs
  , bubblesort(xs) -> bsort(len(xs), xs)
  , len(Nil()) -> 0()
  , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

  DPs:
    { 1: bubble^#(x, Nil()) -> c_1()
    , 2: bubble^#(x', Cons(x, xs)) ->
         c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
             <^#(x', x))
    , 3: bsort^#(S(x'), Cons(x, xs)) ->
         c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
    , 4: bsort^#(0(), xs) -> c_4()
    , 5: bubblesort^#(xs) -> c_5(bsort^#(len(xs), xs), len^#(xs))
    , 6: len^#(Nil()) -> c_6()
    , 7: len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs))
    , 8: bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
         c_8(bubble^#(x, xs))
    , 9: bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
         c_9(bubble^#(x', xs))
    , 10: <^#(x, 0()) -> c_12()
    , 11: <^#(S(x), S(y)) -> c_13(<^#(x, y))
    , 12: <^#(0(), S(y)) -> c_14()
    , 13: +^#(x, S(0())) -> c_10()
    , 14: +^#(S(0()), y) -> c_11() }

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

Strict DPs:
  { bubble^#(x, Nil()) -> c_1()
  , bubble^#(x', Cons(x, xs)) ->
    c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
        <^#(x', x))
  , bsort^#(S(x'), Cons(x, xs)) ->
    c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
  , bubblesort^#(xs) -> c_5(bsort^#(len(xs), xs), len^#(xs))
  , len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs)) }
Weak DPs:
  { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
    c_8(bubble^#(x, xs))
  , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
    c_9(bubble^#(x', xs))
  , <^#(x, 0()) -> c_12()
  , <^#(S(x), S(y)) -> c_13(<^#(x, y))
  , <^#(0(), S(y)) -> c_14()
  , bsort^#(0(), xs) -> c_4()
  , len^#(Nil()) -> c_6()
  , +^#(x, S(0())) -> c_10()
  , +^#(S(0()), y) -> c_11() }
Weak Trs:
  { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
    Cons(x', bubble(x, xs))
  , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
    Cons(x, bubble(x', xs))
  , bubble(x, Nil()) -> Cons(x, Nil())
  , bubble(x', Cons(x, xs)) ->
    bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
  , +(x, S(0())) -> S(x)
  , +(S(0()), y) -> S(y)
  , <(x, 0()) -> False()
  , <(S(x), S(y)) -> <(x, y)
  , <(0(), S(y)) -> True()
  , bsort(S(x'), Cons(x, xs)) -> bsort(x', bubble(x, xs))
  , bsort(0(), xs) -> xs
  , bubblesort(xs) -> bsort(len(xs), xs)
  , len(Nil()) -> 0()
  , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

{ <^#(x, 0()) -> c_12()
, <^#(S(x), S(y)) -> c_13(<^#(x, y))
, <^#(0(), S(y)) -> c_14()
, bsort^#(0(), xs) -> c_4()
, len^#(Nil()) -> c_6()
, +^#(x, S(0())) -> c_10()
, +^#(S(0()), y) -> c_11() }

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

Strict DPs:
  { bubble^#(x, Nil()) -> c_1()
  , bubble^#(x', Cons(x, xs)) ->
    c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
        <^#(x', x))
  , bsort^#(S(x'), Cons(x, xs)) ->
    c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
  , bubblesort^#(xs) -> c_5(bsort^#(len(xs), xs), len^#(xs))
  , len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs)) }
Weak DPs:
  { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
    c_8(bubble^#(x, xs))
  , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
    c_9(bubble^#(x', xs)) }
Weak Trs:
  { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
    Cons(x', bubble(x, xs))
  , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
    Cons(x, bubble(x', xs))
  , bubble(x, Nil()) -> Cons(x, Nil())
  , bubble(x', Cons(x, xs)) ->
    bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
  , +(x, S(0())) -> S(x)
  , +(S(0()), y) -> S(y)
  , <(x, 0()) -> False()
  , <(S(x), S(y)) -> <(x, y)
  , <(0(), S(y)) -> True()
  , bsort(S(x'), Cons(x, xs)) -> bsort(x', bubble(x, xs))
  , bsort(0(), xs) -> xs
  , bubblesort(xs) -> bsort(len(xs), xs)
  , len(Nil()) -> 0()
  , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

  { bubble^#(x', Cons(x, xs)) ->
    c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
        <^#(x', x))
  , len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs)) }

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

Strict DPs:
  { bubble^#(x, Nil()) -> c_1()
  , bubble^#(x', Cons(x, xs)) ->
    c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
  , bsort^#(S(x'), Cons(x, xs)) ->
    c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
  , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs))
  , len^#(Cons(x, xs)) -> c_5(len^#(xs)) }
Weak DPs:
  { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
    c_6(bubble^#(x, xs))
  , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
    c_7(bubble^#(x', xs)) }
Weak Trs:
  { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
    Cons(x', bubble(x, xs))
  , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
    Cons(x, bubble(x', xs))
  , bubble(x, Nil()) -> Cons(x, Nil())
  , bubble(x', Cons(x, xs)) ->
    bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
  , +(x, S(0())) -> S(x)
  , +(S(0()), y) -> S(y)
  , <(x, 0()) -> False()
  , <(S(x), S(y)) -> <(x, y)
  , <(0(), S(y)) -> True()
  , bsort(S(x'), Cons(x, xs)) -> bsort(x', bubble(x, xs))
  , bsort(0(), xs) -> xs
  , bubblesort(xs) -> bsort(len(xs), xs)
  , len(Nil()) -> 0()
  , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
      Cons(x', bubble(x, xs))
    , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
      Cons(x, bubble(x', xs))
    , bubble(x, Nil()) -> Cons(x, Nil())
    , bubble(x', Cons(x, xs)) ->
      bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
    , +(x, S(0())) -> S(x)
    , +(S(0()), y) -> S(y)
    , <(x, 0()) -> False()
    , <(S(x), S(y)) -> <(x, y)
    , <(0(), S(y)) -> True()
    , len(Nil()) -> 0()
    , len(Cons(x, xs)) -> +(S(0()), len(xs)) }

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

Strict DPs:
  { bubble^#(x, Nil()) -> c_1()
  , bubble^#(x', Cons(x, xs)) ->
    c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
  , bsort^#(S(x'), Cons(x, xs)) ->
    c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
  , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs))
  , len^#(Cons(x, xs)) -> c_5(len^#(xs)) }
Weak DPs:
  { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
    c_6(bubble^#(x, xs))
  , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
    c_7(bubble^#(x', xs)) }
Weak Trs:
  { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
    Cons(x', bubble(x, xs))
  , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
    Cons(x, bubble(x', xs))
  , bubble(x, Nil()) -> Cons(x, Nil())
  , bubble(x', Cons(x, xs)) ->
    bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
  , +(x, S(0())) -> S(x)
  , +(S(0()), y) -> S(y)
  , <(x, 0()) -> False()
  , <(S(x), S(y)) -> <(x, y)
  , <(0(), S(y)) -> True()
  , len(Nil()) -> 0()
  , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict
rules from (R) into the weak component:

Problem (R):
------------
  Strict DPs:
    { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs))
    , len^#(Cons(x, xs)) -> c_5(len^#(xs)) }
  Weak DPs:
    { bubble^#(x, Nil()) -> c_1()
    , bubble^#(x', Cons(x, xs)) ->
      c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
    , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
      c_6(bubble^#(x, xs))
    , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
      c_7(bubble^#(x', xs))
    , bsort^#(S(x'), Cons(x, xs)) ->
      c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) }
  Weak Trs:
    { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
      Cons(x', bubble(x, xs))
    , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
      Cons(x, bubble(x', xs))
    , bubble(x, Nil()) -> Cons(x, Nil())
    , bubble(x', Cons(x, xs)) ->
      bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
    , +(x, S(0())) -> S(x)
    , +(S(0()), y) -> S(y)
    , <(x, 0()) -> False()
    , <(S(x), S(y)) -> <(x, y)
    , <(0(), S(y)) -> True()
    , len(Nil()) -> 0()
    , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
  StartTerms: basic terms
  Strategy: innermost

Problem (S):
------------
  Strict DPs:
    { bubble^#(x, Nil()) -> c_1()
    , bubble^#(x', Cons(x, xs)) ->
      c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
    , bsort^#(S(x'), Cons(x, xs)) ->
      c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) }
  Weak DPs:
    { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
      c_6(bubble^#(x, xs))
    , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
      c_7(bubble^#(x', xs))
    , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs))
    , len^#(Cons(x, xs)) -> c_5(len^#(xs)) }
  Weak Trs:
    { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
      Cons(x', bubble(x, xs))
    , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
      Cons(x, bubble(x', xs))
    , bubble(x, Nil()) -> Cons(x, Nil())
    , bubble(x', Cons(x, xs)) ->
      bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
    , +(x, S(0())) -> S(x)
    , +(S(0()), y) -> S(y)
    , <(x, 0()) -> False()
    , <(S(x), S(y)) -> <(x, y)
    , <(0(), S(y)) -> True()
    , len(Nil()) -> 0()
    , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
  StartTerms: basic terms
  Strategy: innermost

Overall, the transformation results in the following sub-problem(s):

Generated new problems:
-----------------------
R) Strict DPs:
     { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs))
     , len^#(Cons(x, xs)) -> c_5(len^#(xs)) }
   Weak DPs:
     { bubble^#(x, Nil()) -> c_1()
     , bubble^#(x', Cons(x, xs)) ->
       c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
     , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
       c_6(bubble^#(x, xs))
     , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
       c_7(bubble^#(x', xs))
     , bsort^#(S(x'), Cons(x, xs)) ->
       c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   StartTerms: basic terms
   Strategy: innermost
   
   This problem was proven YES(O(1),O(n^1)).

S) Strict DPs:
     { bubble^#(x, Nil()) -> c_1()
     , bubble^#(x', Cons(x, xs)) ->
       c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
     , bsort^#(S(x'), Cons(x, xs)) ->
       c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) }
   Weak DPs:
     { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
       c_6(bubble^#(x, xs))
     , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
       c_7(bubble^#(x', xs))
     , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs))
     , len^#(Cons(x, xs)) -> c_5(len^#(xs)) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   StartTerms: basic terms
   Strategy: innermost
   
   This problem was proven YES(O(1),O(n^2)).


Proofs for generated problems:
------------------------------
R) We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^1)).
   
   Strict DPs:
     { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs))
     , len^#(Cons(x, xs)) -> c_5(len^#(xs)) }
   Weak DPs:
     { bubble^#(x, Nil()) -> c_1()
     , bubble^#(x', Cons(x, xs)) ->
       c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
     , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
       c_6(bubble^#(x, xs))
     , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
       c_7(bubble^#(x', xs))
     , bsort^#(S(x'), Cons(x, xs)) ->
       c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^1))
   
   The following weak DPs constitute a sub-graph of the DG that is
   closed under successors. The DPs are removed.
   
   { bubble^#(x, Nil()) -> c_1()
   , bubble^#(x', Cons(x, xs)) ->
     c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
   , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
     c_6(bubble^#(x, xs))
   , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
     c_7(bubble^#(x', xs))
   , bsort^#(S(x'), Cons(x, xs)) ->
     c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^1)).
   
   Strict DPs:
     { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs))
     , len^#(Cons(x, xs)) -> c_5(len^#(xs)) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^1))
   
   Due to missing edges in the dependency-graph, the right-hand sides
   of following rules could be simplified:
   
     { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^1)).
   
   Strict DPs:
     { bubblesort^#(xs) -> c_1(len^#(xs))
     , len^#(Cons(x, xs)) -> c_2(len^#(xs)) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^1))
   
   No rule is usable, rules are removed from the input problem.
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^1)).
   
   Strict DPs:
     { bubblesort^#(xs) -> c_1(len^#(xs))
     , len^#(Cons(x, xs)) -> c_2(len^#(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^1))
   
   We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
   to orient following rules strictly.
   
   DPs:
     { 1: bubblesort^#(xs) -> c_1(len^#(xs))
     , 2: len^#(Cons(x, xs)) -> c_2(len^#(xs)) }
   
   Sub-proof:
   ----------
     The input was oriented with the instance of 'Small Polynomial Path
     Order (PS,1-bounded)' as induced by the safe mapping
     
      safe(Cons) = {1, 2}, safe(bubblesort^#) = {}, safe(len^#) = {},
      safe(c_1) = {}, safe(c_2) = {}
     
     and precedence
     
      bubblesort^# > len^# .
     
     Following symbols are considered recursive:
     
      {len^#}
     
     The recursion depth is 1.
     
     Further, following argument filtering is employed:
     
      pi(Cons) = [2], pi(bubblesort^#) = [1], pi(len^#) = [1],
      pi(c_1) = [1], pi(c_2) = [1]
     
     Usable defined function symbols are a subset of:
     
      {bubblesort^#, len^#}
     
     For your convenience, here are the satisfied ordering constraints:
     
         pi(bubblesort^#(xs)) = bubblesort^#(xs;) 
                              > c_1(len^#(xs;);)  
                              = pi(c_1(len^#(xs)))
                                                  
       pi(len^#(Cons(x, xs))) = len^#(Cons(; xs);)
                              > c_2(len^#(xs;);)  
                              = pi(c_2(len^#(xs)))
                                                  
   
   The strictly oriented rules are moved into the weak component.
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Weak DPs:
     { bubblesort^#(xs) -> c_1(len^#(xs))
     , len^#(Cons(x, xs)) -> c_2(len^#(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   The following weak DPs constitute a sub-graph of the DG that is
   closed under successors. The DPs are removed.
   
   { bubblesort^#(xs) -> c_1(len^#(xs))
   , len^#(Cons(x, xs)) -> c_2(len^#(xs)) }
   
   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

S) We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^2)).
   
   Strict DPs:
     { bubble^#(x, Nil()) -> c_1()
     , bubble^#(x', Cons(x, xs)) ->
       c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
     , bsort^#(S(x'), Cons(x, xs)) ->
       c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) }
   Weak DPs:
     { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
       c_6(bubble^#(x, xs))
     , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
       c_7(bubble^#(x', xs))
     , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs))
     , len^#(Cons(x, xs)) -> c_5(len^#(xs)) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^2))
   
   The following weak DPs constitute a sub-graph of the DG that is
   closed under successors. The DPs are removed.
   
   { len^#(Cons(x, xs)) -> c_5(len^#(xs)) }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^2)).
   
   Strict DPs:
     { bubble^#(x, Nil()) -> c_1()
     , bubble^#(x', Cons(x, xs)) ->
       c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
     , bsort^#(S(x'), Cons(x, xs)) ->
       c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) }
   Weak DPs:
     { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
       c_6(bubble^#(x, xs))
     , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
       c_7(bubble^#(x', xs))
     , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^2))
   
   Due to missing edges in the dependency-graph, the right-hand sides
   of following rules could be simplified:
   
     { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^2)).
   
   Strict DPs:
     { bubble^#(x, Nil()) -> c_1()
     , bubble^#(x', Cons(x, xs)) ->
       c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
     , bsort^#(S(x'), Cons(x, xs)) ->
       c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) }
   Weak DPs:
     { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
       c_4(bubble^#(x, xs))
     , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
       c_5(bubble^#(x', xs))
     , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^2))
   
   We use the processor 'matrix interpretation of dimension 1' to
   orient following rules strictly.
   
   DPs:
     { 1: bubble^#(x, Nil()) -> c_1()
     , 3: bsort^#(S(x'), Cons(x, xs)) ->
          c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
     , 6: bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) }
   Trs: { bubble(x, Nil()) -> Cons(x, Nil()) }
   
   Sub-proof:
   ----------
     The following argument positions are usable:
       Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1},
       Uargs(c_5) = {1}, Uargs(c_6) = {1}
     
     TcT has computed the following constructor-based matrix
     interpretation satisfying not(EDA).
     
         [bubble[Ite][False][Ite]](x1, x2, x3) = [1] x3 + [5]         
                                                                      
                              [bubble](x1, x2) = [1] x2 + [5]         
                                                                      
                                        [True] = [1]                  
                                                                      
                                         [Nil] = [0]                  
                                                                      
                                   [+](x1, x2) = [1] x1 + [1] x2 + [0]
                                                                      
                                       [S](x1) = [1] x1 + [2]         
                                                                      
                                [<](x1, x2) = [1]                  
                                                                      
                                [Cons](x1, x2) = [1] x2 + [2]         
                                                                      
                                           [0] = [0]                  
                                                                      
                                     [len](x1) = [1] x1 + [0]         
                                                                      
                                       [False] = [1]                  
                                                                      
                            [bubble^#](x1, x2) = [2]                  
                                                                      
       [bubble[Ite][False][Ite]^#](x1, x2, x3) = [1] x1 + [1]         
                                                                      
                             [bsort^#](x1, x2) = [5] x1 + [1] x2 + [2]
                                                                      
                            [bubblesort^#](x1) = [7] x1 + [7]         
                                                                      
                                         [c_1] = [1]                  
                                                                      
                                     [c_2](x1) = [1] x1 + [0]         
                                                                      
                                 [c_3](x1, x2) = [1] x1 + [2] x2 + [0]
                                                                      
                                     [c_4](x1) = [1] x1 + [0]         
                                                                      
                                     [c_5](x1) = [1] x1 + [0]         
                                                                      
                                     [c_6](x1) = [1] x1 + [4]         
     
     The order satisfies the following ordering constraints:
     
          [bubble[Ite][False][Ite](True(), x', Cons(x, xs))] =  [1] xs + [7]                                                  
                                                             >= [1] xs + [7]                                                  
                                                             =  [Cons(x', bubble(x, xs))]                                     
                                                                                                                              
         [bubble[Ite][False][Ite](False(), x', Cons(x, xs))] =  [1] xs + [7]                                                  
                                                             >= [1] xs + [7]                                                  
                                                             =  [Cons(x, bubble(x', xs))]                                     
                                                                                                                              
                                          [bubble(x, Nil())] =  [5]                                                           
                                                             >  [2]                                                           
                                                             =  [Cons(x, Nil())]                                              
                                                                                                                              
                                   [bubble(x', Cons(x, xs))] =  [1] xs + [7]                                                  
                                                             >= [1] xs + [7]                                                  
                                                             =  [bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))]       
                                                                                                                              
                                              [+(x, S(0()))] =  [1] x + [2]                                                   
                                                             >= [1] x + [2]                                                   
                                                             =  [S(x)]                                                        
                                                                                                                              
                                              [+(S(0()), y)] =  [1] y + [2]                                                   
                                                             >= [1] y + [2]                                                   
                                                             =  [S(y)]                                                        
                                                                                                                              
                                              [<(x, 0())] =  [1]                                                           
                                                             >= [1]                                                           
                                                             =  [False()]                                                     
                                                                                                                              
                                          [<(S(x), S(y))] =  [1]                                                           
                                                             >= [1]                                                           
                                                             =  [<(x, y)]                                                  
                                                                                                                              
                                           [<(0(), S(y))] =  [1]                                                           
                                                             >= [1]                                                           
                                                             =  [True()]                                                      
                                                                                                                              
                                                [len(Nil())] =  [0]                                                           
                                                             >= [0]                                                           
                                                             =  [0()]                                                         
                                                                                                                              
                                          [len(Cons(x, xs))] =  [1] xs + [2]                                                  
                                                             >= [1] xs + [2]                                                  
                                                             =  [+(S(0()), len(xs))]                                          
                                                                                                                              
                                        [bubble^#(x, Nil())] =  [2]                                                           
                                                             >  [1]                                                           
                                                             =  [c_1()]                                                       
                                                                                                                              
                                 [bubble^#(x', Cons(x, xs))] =  [2]                                                           
                                                             >= [2]                                                           
                                                             =  [c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))]
                                                                                                                              
        [bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs))] =  [2]                                                           
                                                             >= [2]                                                           
                                                             =  [c_4(bubble^#(x, xs))]                                        
                                                                                                                              
       [bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs))] =  [2]                                                           
                                                             >= [2]                                                           
                                                             =  [c_5(bubble^#(x', xs))]                                       
                                                                                                                              
                               [bsort^#(S(x'), Cons(x, xs))] =  [5] x' + [1] xs + [14]                                        
                                                             >  [5] x' + [1] xs + [11]                                        
                                                             =  [c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))]            
                                                                                                                              
                                          [bubblesort^#(xs)] =  [7] xs + [7]                                                  
                                                             >  [6] xs + [6]                                                  
                                                             =  [c_6(bsort^#(len(xs), xs))]                                   
                                                                                                                              
   
   The strictly oriented rules are moved into the weak component.
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^2)).
   
   Strict DPs:
     { bubble^#(x', Cons(x, xs)) ->
       c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) }
   Weak DPs:
     { bubble^#(x, Nil()) -> c_1()
     , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
       c_4(bubble^#(x, xs))
     , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
       c_5(bubble^#(x', xs))
     , bsort^#(S(x'), Cons(x, xs)) ->
       c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
     , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^2))
   
   The following weak DPs constitute a sub-graph of the DG that is
   closed under successors. The DPs are removed.
   
   { bubble^#(x, Nil()) -> c_1() }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^2)).
   
   Strict DPs:
     { bubble^#(x', Cons(x, xs)) ->
       c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) }
   Weak DPs:
     { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
       c_4(bubble^#(x, xs))
     , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
       c_5(bubble^#(x', xs))
     , bsort^#(S(x'), Cons(x, xs)) ->
       c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
     , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^2))
   
   We decompose the input problem according to the dependency graph
   into the upper component
   
     { bsort^#(S(x'), Cons(x, xs)) ->
       c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
     , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) }
   
   and lower component
   
     { bubble^#(x', Cons(x, xs)) ->
       c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
     , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
       c_4(bubble^#(x, xs))
     , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
       c_5(bubble^#(x', xs)) }
   
   Further, following extension rules are added to the lower
   component.
   
   { bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs)
   , bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs))
   , bubblesort^#(xs) -> bsort^#(len(xs), xs) }
   
   TcT solves the upper component with certificate YES(O(1),O(n^1)).
   
   Sub-proof:
   ----------
     We are left with following problem, upon which TcT provides the
     certificate YES(O(1),O(n^1)).
     
     Strict DPs:
       { bsort^#(S(x'), Cons(x, xs)) ->
         c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) }
     Weak DPs: { bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) }
     Weak Trs:
       { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
         Cons(x', bubble(x, xs))
       , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
         Cons(x, bubble(x', xs))
       , bubble(x, Nil()) -> Cons(x, Nil())
       , bubble(x', Cons(x, xs)) ->
         bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
       , +(x, S(0())) -> S(x)
       , +(S(0()), y) -> S(y)
       , <(x, 0()) -> False()
       , <(S(x), S(y)) -> <(x, y)
       , <(0(), S(y)) -> True()
       , len(Nil()) -> 0()
       , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
     Obligation:
       innermost runtime complexity
     Answer:
       YES(O(1),O(n^1))
     
     We use the processor 'matrix interpretation of dimension 1' to
     orient following rules strictly.
     
     DPs:
       { 1: bsort^#(S(x'), Cons(x, xs)) ->
            c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
       , 2: bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) }
     Trs:
       { +(x, S(0())) -> S(x)
       , +(S(0()), y) -> S(y)
       , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
     
     Sub-proof:
     ----------
       The following argument positions are usable:
         Uargs(c_3) = {1}, Uargs(c_6) = {1}
       
       TcT has computed the following constructor-based matrix
       interpretation satisfying not(EDA).
       
         [bubble[Ite][False][Ite]](x1, x2, x3) = [1] x2 + [0]         
                                                                      
                              [bubble](x1, x2) = [0]                  
                                                                      
                                        [True] = [0]                  
                                                                      
                                         [Nil] = [0]                  
                                                                      
                                   [+](x1, x2) = [4] x1 + [1] x2 + [2]
                                                                      
                                       [S](x1) = [1] x1 + [2]         
                                                                      
                                [<](x1, x2) = [0]                  
                                                                      
                                [Cons](x1, x2) = [1] x2 + [5]         
                                                                      
                                           [0] = [0]                  
                                                                      
                                     [len](x1) = [3] x1 + [0]         
                                                                      
                                       [False] = [0]                  
                                                                      
                            [bubble^#](x1, x2) = [0]                  
                                                                      
                             [bsort^#](x1, x2) = [1] x1 + [0]         
                                                                      
                            [bubblesort^#](x1) = [7] x1 + [7]         
                                                                      
                                 [c_3](x1, x2) = [1] x1 + [1] x2 + [1]
                                                                      
                                     [c_6](x1) = [1] x1 + [0]         
       
       The order satisfies the following ordering constraints:
       
          [bubble[Ite][False][Ite](True(), x', Cons(x, xs))] =  [1] x' + [0]                                           
                                                             ?  [5]                                                    
                                                             =  [Cons(x', bubble(x, xs))]                              
                                                                                                                       
         [bubble[Ite][False][Ite](False(), x', Cons(x, xs))] =  [1] x' + [0]                                           
                                                             ?  [5]                                                    
                                                             =  [Cons(x, bubble(x', xs))]                              
                                                                                                                       
                                          [bubble(x, Nil())] =  [0]                                                    
                                                             ?  [5]                                                    
                                                             =  [Cons(x, Nil())]                                       
                                                                                                                       
                                   [bubble(x', Cons(x, xs))] =  [0]                                                    
                                                             ?  [1] x' + [0]                                           
                                                             =  [bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))]
                                                                                                                       
                                              [+(x, S(0()))] =  [4] x + [4]                                            
                                                             >  [1] x + [2]                                            
                                                             =  [S(x)]                                                 
                                                                                                                       
                                              [+(S(0()), y)] =  [1] y + [10]                                           
                                                             >  [1] y + [2]                                            
                                                             =  [S(y)]                                                 
                                                                                                                       
                                              [<(x, 0())] =  [0]                                                    
                                                             >= [0]                                                    
                                                             =  [False()]                                              
                                                                                                                       
                                          [<(S(x), S(y))] =  [0]                                                    
                                                             >= [0]                                                    
                                                             =  [<(x, y)]                                           
                                                                                                                       
                                           [<(0(), S(y))] =  [0]                                                    
                                                             >= [0]                                                    
                                                             =  [True()]                                               
                                                                                                                       
                                                [len(Nil())] =  [0]                                                    
                                                             >= [0]                                                    
                                                             =  [0()]                                                  
                                                                                                                       
                                          [len(Cons(x, xs))] =  [3] xs + [15]                                          
                                                             >  [3] xs + [10]                                          
                                                             =  [+(S(0()), len(xs))]                                   
                                                                                                                       
                               [bsort^#(S(x'), Cons(x, xs))] =  [1] x' + [2]                                           
                                                             >  [1] x' + [1]                                           
                                                             =  [c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))]     
                                                                                                                       
                                          [bubblesort^#(xs)] =  [7] xs + [7]                                           
                                                             >  [3] xs + [0]                                           
                                                             =  [c_6(bsort^#(len(xs), xs))]                            
                                                                                                                       
     
     The strictly oriented rules are moved into the weak component.
     
     We are left with following problem, upon which TcT provides the
     certificate YES(O(1),O(1)).
     
     Weak DPs:
       { bsort^#(S(x'), Cons(x, xs)) ->
         c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
       , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) }
     Weak Trs:
       { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
         Cons(x', bubble(x, xs))
       , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
         Cons(x, bubble(x', xs))
       , bubble(x, Nil()) -> Cons(x, Nil())
       , bubble(x', Cons(x, xs)) ->
         bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
       , +(x, S(0())) -> S(x)
       , +(S(0()), y) -> S(y)
       , <(x, 0()) -> False()
       , <(S(x), S(y)) -> <(x, y)
       , <(0(), S(y)) -> True()
       , len(Nil()) -> 0()
       , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
     Obligation:
       innermost runtime complexity
     Answer:
       YES(O(1),O(1))
     
     The following weak DPs constitute a sub-graph of the DG that is
     closed under successors. The DPs are removed.
     
     { bsort^#(S(x'), Cons(x, xs)) ->
       c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))
     , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) }
     
     We are left with following problem, upon which TcT provides the
     certificate YES(O(1),O(1)).
     
     Weak Trs:
       { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
         Cons(x', bubble(x, xs))
       , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
         Cons(x, bubble(x', xs))
       , bubble(x, Nil()) -> Cons(x, Nil())
       , bubble(x', Cons(x, xs)) ->
         bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
       , +(x, S(0())) -> S(x)
       , +(S(0()), y) -> S(y)
       , <(x, 0()) -> False()
       , <(S(x), S(y)) -> <(x, y)
       , <(0(), S(y)) -> True()
       , len(Nil()) -> 0()
       , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
     Obligation:
       innermost runtime complexity
     Answer:
       YES(O(1),O(1))
     
     No rule is usable, rules are removed from the input problem.
     
     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
   
   We return to the main proof.
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(n^1)).
   
   Strict DPs:
     { bubble^#(x', Cons(x, xs)) ->
       c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) }
   Weak DPs:
     { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
       c_4(bubble^#(x, xs))
     , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
       c_5(bubble^#(x', xs))
     , bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs)
     , bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs))
     , bubblesort^#(xs) -> bsort^#(len(xs), xs) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(n^1))
   
   We use the processor 'matrix interpretation of dimension 1' to
   orient following rules strictly.
   
   DPs:
     { 2: bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
          c_4(bubble^#(x, xs))
     , 3: bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
          c_5(bubble^#(x', xs))
     , 4: bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs)
     , 5: bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs))
     , 6: bubblesort^#(xs) -> bsort^#(len(xs), xs) }
   Trs: { bubble(x, Nil()) -> Cons(x, Nil()) }
   
   Sub-proof:
   ----------
     The following argument positions are usable:
       Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}
     
     TcT has computed the following constructor-based matrix
     interpretation satisfying not(EDA).
     
         [bubble[Ite][False][Ite]](x1, x2, x3) = [1] x1 + [1] x3 + [0]
                                                                      
                              [bubble](x1, x2) = [1] x2 + [2]         
                                                                      
                                        [True] = [2]                  
                                                                      
                                         [Nil] = [0]                  
                                                                      
                                   [+](x1, x2) = [1] x1 + [1] x2 + [0]
                                                                      
                                       [S](x1) = [1] x1 + [1]         
                                                                      
                                [<](x1, x2) = [2]                  
                                                                      
                                [Cons](x1, x2) = [1] x2 + [1]         
                                                                      
                                           [0] = [0]                  
                                                                      
                                     [len](x1) = [1] x1 + [0]         
                                                                      
                                       [False] = [2]                  
                                                                      
                            [bubble^#](x1, x2) = [1] x2 + [0]         
                                                                      
       [bubble[Ite][False][Ite]^#](x1, x2, x3) = [1] x3 + [0]         
                                                                      
                             [bsort^#](x1, x2) = [4] x1 + [3] x2 + [5]
                                                                      
                            [bubblesort^#](x1) = [7] x1 + [7]         
                                                                      
                                     [c_2](x1) = [1] x1 + [0]         
                                                                      
                                     [c_4](x1) = [1] x1 + [0]         
                                                                      
                                     [c_5](x1) = [1] x1 + [0]         
     
     The order satisfies the following ordering constraints:
     
          [bubble[Ite][False][Ite](True(), x', Cons(x, xs))] =  [1] xs + [3]                                                  
                                                             >= [1] xs + [3]                                                  
                                                             =  [Cons(x', bubble(x, xs))]                                     
                                                                                                                              
         [bubble[Ite][False][Ite](False(), x', Cons(x, xs))] =  [1] xs + [3]                                                  
                                                             >= [1] xs + [3]                                                  
                                                             =  [Cons(x, bubble(x', xs))]                                     
                                                                                                                              
                                          [bubble(x, Nil())] =  [2]                                                           
                                                             >  [1]                                                           
                                                             =  [Cons(x, Nil())]                                              
                                                                                                                              
                                   [bubble(x', Cons(x, xs))] =  [1] xs + [3]                                                  
                                                             >= [1] xs + [3]                                                  
                                                             =  [bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))]       
                                                                                                                              
                                              [+(x, S(0()))] =  [1] x + [1]                                                   
                                                             >= [1] x + [1]                                                   
                                                             =  [S(x)]                                                        
                                                                                                                              
                                              [+(S(0()), y)] =  [1] y + [1]                                                   
                                                             >= [1] y + [1]                                                   
                                                             =  [S(y)]                                                        
                                                                                                                              
                                              [<(x, 0())] =  [2]                                                           
                                                             >= [2]                                                           
                                                             =  [False()]                                                     
                                                                                                                              
                                          [<(S(x), S(y))] =  [2]                                                           
                                                             >= [2]                                                           
                                                             =  [<(x, y)]                                                  
                                                                                                                              
                                           [<(0(), S(y))] =  [2]                                                           
                                                             >= [2]                                                           
                                                             =  [True()]                                                      
                                                                                                                              
                                                [len(Nil())] =  [0]                                                           
                                                             >= [0]                                                           
                                                             =  [0()]                                                         
                                                                                                                              
                                          [len(Cons(x, xs))] =  [1] xs + [1]                                                  
                                                             >= [1] xs + [1]                                                  
                                                             =  [+(S(0()), len(xs))]                                          
                                                                                                                              
                                 [bubble^#(x', Cons(x, xs))] =  [1] xs + [1]                                                  
                                                             >= [1] xs + [1]                                                  
                                                             =  [c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))]
                                                                                                                              
        [bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs))] =  [1] xs + [1]                                                  
                                                             >  [1] xs + [0]                                                  
                                                             =  [c_4(bubble^#(x, xs))]                                        
                                                                                                                              
       [bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs))] =  [1] xs + [1]                                                  
                                                             >  [1] xs + [0]                                                  
                                                             =  [c_5(bubble^#(x', xs))]                                       
                                                                                                                              
                               [bsort^#(S(x'), Cons(x, xs))] =  [4] x' + [3] xs + [12]                                        
                                                             >  [1] xs + [0]                                                  
                                                             =  [bubble^#(x, xs)]                                             
                                                                                                                              
                               [bsort^#(S(x'), Cons(x, xs))] =  [4] x' + [3] xs + [12]                                        
                                                             >  [4] x' + [3] xs + [11]                                        
                                                             =  [bsort^#(x', bubble(x, xs))]                                  
                                                                                                                              
                                          [bubblesort^#(xs)] =  [7] xs + [7]                                                  
                                                             >  [7] xs + [5]                                                  
                                                             =  [bsort^#(len(xs), xs)]                                        
                                                                                                                              
   
   We return to the main proof. Consider the set of all dependency
   pairs
   
   :
     { 1: bubble^#(x', Cons(x, xs)) ->
          c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
     , 2: bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
          c_4(bubble^#(x, xs))
     , 3: bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
          c_5(bubble^#(x', xs))
     , 4: bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs)
     , 5: bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs))
     , 6: bubblesort^#(xs) -> bsort^#(len(xs), xs) }
   
   Processor 'matrix interpretation of dimension 1' induces the
   complexity certificate YES(?,O(n^1)) on application of dependency
   pairs {2,3,4,5,6}. These cover all (indirect) predecessors of
   dependency pairs {1,2,3,4,5,6}, their number of application is
   equally bounded. The dependency pairs are shifted into the weak
   component.
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Weak DPs:
     { bubble^#(x', Cons(x, xs)) ->
       c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
     , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
       c_4(bubble^#(x, xs))
     , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
       c_5(bubble^#(x', xs))
     , bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs)
     , bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs))
     , bubblesort^#(xs) -> bsort^#(len(xs), xs) }
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   The following weak DPs constitute a sub-graph of the DG that is
   closed under successors. The DPs are removed.
   
   { bubble^#(x', Cons(x, xs)) ->
     c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
   , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) ->
     c_4(bubble^#(x, xs))
   , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
     c_5(bubble^#(x', xs))
   , bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs)
   , bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs))
   , bubblesort^#(xs) -> bsort^#(len(xs), xs) }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Weak Trs:
     { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) ->
       Cons(x', bubble(x, xs))
     , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) ->
       Cons(x, bubble(x', xs))
     , bubble(x, Nil()) -> Cons(x, Nil())
     , bubble(x', Cons(x, xs)) ->
       bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))
     , +(x, S(0())) -> S(x)
     , +(S(0()), y) -> S(y)
     , <(x, 0()) -> False()
     , <(S(x), S(y)) -> <(x, y)
     , <(0(), S(y)) -> True()
     , len(Nil()) -> 0()
     , len(Cons(x, xs)) -> +(S(0()), len(xs)) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   No rule is usable, rules are removed from the input problem.
   
   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))