WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            DBL(0()) -> c()
            DBL(s(z0)) -> c1(DBL(z0))
            DBLS(cons(z0,z1)) -> c3(DBL(z0))
            DBLS(cons(z0,z1)) -> c4(DBLS(z1))
            DBLS(nil()) -> c2()
            FROM(z0) -> c10(FROM(s(z0)))
            INDX(cons(z0,z1),z2) -> c8(SEL(z0,z2))
            INDX(cons(z0,z1),z2) -> c9(INDX(z1,z2))
            INDX(nil(),z0) -> c7()
            SEL(0(),cons(z0,z1)) -> c5()
            SEL(s(z0),cons(z1,z2)) -> c6(SEL(z0,z2))
        - Weak TRS:
            dbl(0()) -> 0()
            dbl(s(z0)) -> s(s(dbl(z0)))
            dbls(cons(z0,z1)) -> cons(dbl(z0),dbls(z1))
            dbls(nil()) -> nil()
            from(z0) -> cons(z0,from(s(z0)))
            indx(cons(z0,z1),z2) -> cons(sel(z0,z2),indx(z1,z2))
            indx(nil(),z0) -> nil()
            sel(0(),cons(z0,z1)) -> z0
            sel(s(z0),cons(z1,z2)) -> sel(z0,z2)
        - Signature:
            {DBL/1,DBLS/1,FROM/1,INDX/2,SEL/2,dbl/1,dbls/1,from/1,indx/2,sel/2} / {0/0,c/0,c1/1,c10/1,c2/0,c3/1,c4/1
            ,c5/0,c6/1,c7/0,c8/1,c9/1,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {DBL,DBLS,FROM,INDX,SEL,dbl,dbls,from,indx
            ,sel} and constructors {0,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            DBL(0()) -> c()
            DBL(s(z0)) -> c1(DBL(z0))
            DBLS(cons(z0,z1)) -> c3(DBL(z0))
            DBLS(cons(z0,z1)) -> c4(DBLS(z1))
            DBLS(nil()) -> c2()
            FROM(z0) -> c10(FROM(s(z0)))
            INDX(cons(z0,z1),z2) -> c8(SEL(z0,z2))
            INDX(cons(z0,z1),z2) -> c9(INDX(z1,z2))
            INDX(nil(),z0) -> c7()
            SEL(0(),cons(z0,z1)) -> c5()
            SEL(s(z0),cons(z1,z2)) -> c6(SEL(z0,z2))
        - Weak TRS:
            dbl(0()) -> 0()
            dbl(s(z0)) -> s(s(dbl(z0)))
            dbls(cons(z0,z1)) -> cons(dbl(z0),dbls(z1))
            dbls(nil()) -> nil()
            from(z0) -> cons(z0,from(s(z0)))
            indx(cons(z0,z1),z2) -> cons(sel(z0,z2),indx(z1,z2))
            indx(nil(),z0) -> nil()
            sel(0(),cons(z0,z1)) -> z0
            sel(s(z0),cons(z1,z2)) -> sel(z0,z2)
        - Signature:
            {DBL/1,DBLS/1,FROM/1,INDX/2,SEL/2,dbl/1,dbls/1,from/1,indx/2,sel/2} / {0/0,c/0,c1/1,c10/1,c2/0,c3/1,c4/1
            ,c5/0,c6/1,c7/0,c8/1,c9/1,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {DBL,DBLS,FROM,INDX,SEL,dbl,dbls,from,indx
            ,sel} and constructors {0,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            DBL(0()) -> c()
            DBL(s(z0)) -> c1(DBL(z0))
            DBLS(cons(z0,z1)) -> c3(DBL(z0))
            DBLS(cons(z0,z1)) -> c4(DBLS(z1))
            DBLS(nil()) -> c2()
            FROM(z0) -> c10(FROM(s(z0)))
            INDX(cons(z0,z1),z2) -> c8(SEL(z0,z2))
            INDX(cons(z0,z1),z2) -> c9(INDX(z1,z2))
            INDX(nil(),z0) -> c7()
            SEL(0(),cons(z0,z1)) -> c5()
            SEL(s(z0),cons(z1,z2)) -> c6(SEL(z0,z2))
        - Weak TRS:
            dbl(0()) -> 0()
            dbl(s(z0)) -> s(s(dbl(z0)))
            dbls(cons(z0,z1)) -> cons(dbl(z0),dbls(z1))
            dbls(nil()) -> nil()
            from(z0) -> cons(z0,from(s(z0)))
            indx(cons(z0,z1),z2) -> cons(sel(z0,z2),indx(z1,z2))
            indx(nil(),z0) -> nil()
            sel(0(),cons(z0,z1)) -> z0
            sel(s(z0),cons(z1,z2)) -> sel(z0,z2)
        - Signature:
            {DBL/1,DBLS/1,FROM/1,INDX/2,SEL/2,dbl/1,dbls/1,from/1,indx/2,sel/2} / {0/0,c/0,c1/1,c10/1,c2/0,c3/1,c4/1
            ,c5/0,c6/1,c7/0,c8/1,c9/1,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {DBL,DBLS,FROM,INDX,SEL,dbl,dbls,from,indx
            ,sel} and constructors {0,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,s}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          DBL(x){x -> s(x)} =
            DBL(s(x)) ->^+ c1(DBL(x))
              = C[DBL(x) = DBL(x){}]

WORST_CASE(Omega(n^1),?)