WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            BSORT(.(z0,z1)) -> c1(LAST(.(bubble(.(z0,z1)),bsort(butlast(bubble(.(z0,z1)))))),BUBBLE(.(z0,z1)))
            BSORT(.(z0,z1)) -> c2(LAST(.(bubble(.(z0,z1)),bsort(butlast(bubble(.(z0,z1))))))
                                 ,BSORT(butlast(bubble(.(z0,z1))))
                                 ,BUTLAST(bubble(.(z0,z1)))
                                 ,BUBBLE(.(z0,z1)))
            BSORT(nil()) -> c()
            BUBBLE(.(z0,.(z1,z2))) -> c5(BUBBLE(.(z0,z2)))
            BUBBLE(.(z0,.(z1,z2))) -> c6(BUBBLE(.(z1,z2)))
            BUBBLE(.(z0,nil())) -> c4()
            BUBBLE(nil()) -> c3()
            BUTLAST(.(z0,.(z1,z2))) -> c12(BUTLAST(.(z1,z2)))
            BUTLAST(.(z0,nil())) -> c11()
            BUTLAST(nil()) -> c10()
            LAST(.(z0,.(z1,z2))) -> c9(LAST(.(z1,z2)))
            LAST(.(z0,nil())) -> c8()
            LAST(nil()) -> c7()
        - Weak TRS:
            bsort(.(z0,z1)) -> last(.(bubble(.(z0,z1)),bsort(butlast(bubble(.(z0,z1))))))
            bsort(nil()) -> nil()
            bubble(.(z0,.(z1,z2))) -> if(<=(z0,z1),.(z1,bubble(.(z0,z2))),.(z0,bubble(.(z1,z2))))
            bubble(.(z0,nil())) -> .(z0,nil())
            bubble(nil()) -> nil()
            butlast(.(z0,.(z1,z2))) -> .(z0,butlast(.(z1,z2)))
            butlast(.(z0,nil())) -> nil()
            butlast(nil()) -> nil()
            last(.(z0,.(z1,z2))) -> last(.(z1,z2))
            last(.(z0,nil())) -> z0
            last(nil()) -> 0()
        - Signature:
            {BSORT/1,BUBBLE/1,BUTLAST/1,LAST/1,bsort/1,bubble/1,butlast/1,last/1} / {./2,0/0,<=/2,c/0,c1/2,c10/0,c11/0
            ,c12/1,c2/4,c3/0,c4/0,c5/1,c6/1,c7/0,c8/0,c9/1,if/3,nil/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {BSORT,BUBBLE,BUTLAST,LAST,bsort,bubble,butlast
            ,last} and constructors {.,0,<=,c,c1,c10,c11,c12,c2,c3,c4,c5,c6,c7,c8,c9,if,nil}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            BSORT(.(z0,z1)) -> c1(LAST(.(bubble(.(z0,z1)),bsort(butlast(bubble(.(z0,z1)))))),BUBBLE(.(z0,z1)))
            BSORT(.(z0,z1)) -> c2(LAST(.(bubble(.(z0,z1)),bsort(butlast(bubble(.(z0,z1))))))
                                 ,BSORT(butlast(bubble(.(z0,z1))))
                                 ,BUTLAST(bubble(.(z0,z1)))
                                 ,BUBBLE(.(z0,z1)))
            BSORT(nil()) -> c()
            BUBBLE(.(z0,.(z1,z2))) -> c5(BUBBLE(.(z0,z2)))
            BUBBLE(.(z0,.(z1,z2))) -> c6(BUBBLE(.(z1,z2)))
            BUBBLE(.(z0,nil())) -> c4()
            BUBBLE(nil()) -> c3()
            BUTLAST(.(z0,.(z1,z2))) -> c12(BUTLAST(.(z1,z2)))
            BUTLAST(.(z0,nil())) -> c11()
            BUTLAST(nil()) -> c10()
            LAST(.(z0,.(z1,z2))) -> c9(LAST(.(z1,z2)))
            LAST(.(z0,nil())) -> c8()
            LAST(nil()) -> c7()
        - Weak TRS:
            bsort(.(z0,z1)) -> last(.(bubble(.(z0,z1)),bsort(butlast(bubble(.(z0,z1))))))
            bsort(nil()) -> nil()
            bubble(.(z0,.(z1,z2))) -> if(<=(z0,z1),.(z1,bubble(.(z0,z2))),.(z0,bubble(.(z1,z2))))
            bubble(.(z0,nil())) -> .(z0,nil())
            bubble(nil()) -> nil()
            butlast(.(z0,.(z1,z2))) -> .(z0,butlast(.(z1,z2)))
            butlast(.(z0,nil())) -> nil()
            butlast(nil()) -> nil()
            last(.(z0,.(z1,z2))) -> last(.(z1,z2))
            last(.(z0,nil())) -> z0
            last(nil()) -> 0()
        - Signature:
            {BSORT/1,BUBBLE/1,BUTLAST/1,LAST/1,bsort/1,bubble/1,butlast/1,last/1} / {./2,0/0,<=/2,c/0,c1/2,c10/0,c11/0
            ,c12/1,c2/4,c3/0,c4/0,c5/1,c6/1,c7/0,c8/0,c9/1,if/3,nil/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {BSORT,BUBBLE,BUTLAST,LAST,bsort,bubble,butlast
            ,last} and constructors {.,0,<=,c,c1,c10,c11,c12,c2,c3,c4,c5,c6,c7,c8,c9,if,nil}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            BSORT(.(z0,z1)) -> c1(LAST(.(bubble(.(z0,z1)),bsort(butlast(bubble(.(z0,z1)))))),BUBBLE(.(z0,z1)))
            BSORT(.(z0,z1)) -> c2(LAST(.(bubble(.(z0,z1)),bsort(butlast(bubble(.(z0,z1))))))
                                 ,BSORT(butlast(bubble(.(z0,z1))))
                                 ,BUTLAST(bubble(.(z0,z1)))
                                 ,BUBBLE(.(z0,z1)))
            BSORT(nil()) -> c()
            BUBBLE(.(z0,.(z1,z2))) -> c5(BUBBLE(.(z0,z2)))
            BUBBLE(.(z0,.(z1,z2))) -> c6(BUBBLE(.(z1,z2)))
            BUBBLE(.(z0,nil())) -> c4()
            BUBBLE(nil()) -> c3()
            BUTLAST(.(z0,.(z1,z2))) -> c12(BUTLAST(.(z1,z2)))
            BUTLAST(.(z0,nil())) -> c11()
            BUTLAST(nil()) -> c10()
            LAST(.(z0,.(z1,z2))) -> c9(LAST(.(z1,z2)))
            LAST(.(z0,nil())) -> c8()
            LAST(nil()) -> c7()
        - Weak TRS:
            bsort(.(z0,z1)) -> last(.(bubble(.(z0,z1)),bsort(butlast(bubble(.(z0,z1))))))
            bsort(nil()) -> nil()
            bubble(.(z0,.(z1,z2))) -> if(<=(z0,z1),.(z1,bubble(.(z0,z2))),.(z0,bubble(.(z1,z2))))
            bubble(.(z0,nil())) -> .(z0,nil())
            bubble(nil()) -> nil()
            butlast(.(z0,.(z1,z2))) -> .(z0,butlast(.(z1,z2)))
            butlast(.(z0,nil())) -> nil()
            butlast(nil()) -> nil()
            last(.(z0,.(z1,z2))) -> last(.(z1,z2))
            last(.(z0,nil())) -> z0
            last(nil()) -> 0()
        - Signature:
            {BSORT/1,BUBBLE/1,BUTLAST/1,LAST/1,bsort/1,bubble/1,butlast/1,last/1} / {./2,0/0,<=/2,c/0,c1/2,c10/0,c11/0
            ,c12/1,c2/4,c3/0,c4/0,c5/1,c6/1,c7/0,c8/0,c9/1,if/3,nil/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {BSORT,BUBBLE,BUTLAST,LAST,bsort,bubble,butlast
            ,last} and constructors {.,0,<=,c,c1,c10,c11,c12,c2,c3,c4,c5,c6,c7,c8,c9,if,nil}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          BUBBLE(.(x,z)){z -> .(y,z)} =
            BUBBLE(.(x,.(y,z))) ->^+ c5(BUBBLE(.(x,z)))
              = C[BUBBLE(.(x,z)) = BUBBLE(.(x,z)){}]

WORST_CASE(Omega(n^1),?)