WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            DOUBLE(0()) -> c7()
            DOUBLE(s(z0)) -> c8(DOUBLE(z0))
            EXP(0()) -> c5()
            EXP(s(z0)) -> c6(DOUBLE(exp(z0)),EXP(z0))
            F(a(),0(),z0) -> c1()
            F(a(),s(z0),z1) -> c2(F(b(),z1,s(z0)))
            F(b(),z0,z1) -> c3(F(a(),half(z1),exp(z0)),HALF(z1))
            F(b(),z0,z1) -> c4(F(a(),half(z1),exp(z0)),EXP(z0))
            HALF(0()) -> c9(DOUBLE(0()))
            HALF(s(0())) -> c10(HALF(0()))
            HALF(s(s(z0))) -> c11(HALF(z0))
            TOWER(z0) -> c(F(a(),z0,s(0())))
        - Weak TRS:
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            exp(0()) -> s(0())
            exp(s(z0)) -> double(exp(z0))
            f(a(),0(),z0) -> z0
            f(a(),s(z0),z1) -> f(b(),z1,s(z0))
            f(b(),z0,z1) -> f(a(),half(z1),exp(z0))
            half(0()) -> double(0())
            half(s(0())) -> half(0())
            half(s(s(z0))) -> s(half(z0))
            tower(z0) -> f(a(),z0,s(0()))
        - Signature:
            {DOUBLE/1,EXP/1,F/3,HALF/1,TOWER/1,double/1,exp/1,f/3,half/1,tower/1} / {0/0,a/0,b/0,c/1,c1/0,c10/1,c11/1
            ,c2/1,c3/2,c4/2,c5/0,c6/2,c7/0,c8/1,c9/1,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {DOUBLE,EXP,F,HALF,TOWER,double,exp,f,half
            ,tower} and constructors {0,a,b,c,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            DOUBLE(0()) -> c7()
            DOUBLE(s(z0)) -> c8(DOUBLE(z0))
            EXP(0()) -> c5()
            EXP(s(z0)) -> c6(DOUBLE(exp(z0)),EXP(z0))
            F(a(),0(),z0) -> c1()
            F(a(),s(z0),z1) -> c2(F(b(),z1,s(z0)))
            F(b(),z0,z1) -> c3(F(a(),half(z1),exp(z0)),HALF(z1))
            F(b(),z0,z1) -> c4(F(a(),half(z1),exp(z0)),EXP(z0))
            HALF(0()) -> c9(DOUBLE(0()))
            HALF(s(0())) -> c10(HALF(0()))
            HALF(s(s(z0))) -> c11(HALF(z0))
            TOWER(z0) -> c(F(a(),z0,s(0())))
        - Weak TRS:
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            exp(0()) -> s(0())
            exp(s(z0)) -> double(exp(z0))
            f(a(),0(),z0) -> z0
            f(a(),s(z0),z1) -> f(b(),z1,s(z0))
            f(b(),z0,z1) -> f(a(),half(z1),exp(z0))
            half(0()) -> double(0())
            half(s(0())) -> half(0())
            half(s(s(z0))) -> s(half(z0))
            tower(z0) -> f(a(),z0,s(0()))
        - Signature:
            {DOUBLE/1,EXP/1,F/3,HALF/1,TOWER/1,double/1,exp/1,f/3,half/1,tower/1} / {0/0,a/0,b/0,c/1,c1/0,c10/1,c11/1
            ,c2/1,c3/2,c4/2,c5/0,c6/2,c7/0,c8/1,c9/1,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {DOUBLE,EXP,F,HALF,TOWER,double,exp,f,half
            ,tower} and constructors {0,a,b,c,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            DOUBLE(0()) -> c7()
            DOUBLE(s(z0)) -> c8(DOUBLE(z0))
            EXP(0()) -> c5()
            EXP(s(z0)) -> c6(DOUBLE(exp(z0)),EXP(z0))
            F(a(),0(),z0) -> c1()
            F(a(),s(z0),z1) -> c2(F(b(),z1,s(z0)))
            F(b(),z0,z1) -> c3(F(a(),half(z1),exp(z0)),HALF(z1))
            F(b(),z0,z1) -> c4(F(a(),half(z1),exp(z0)),EXP(z0))
            HALF(0()) -> c9(DOUBLE(0()))
            HALF(s(0())) -> c10(HALF(0()))
            HALF(s(s(z0))) -> c11(HALF(z0))
            TOWER(z0) -> c(F(a(),z0,s(0())))
        - Weak TRS:
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            exp(0()) -> s(0())
            exp(s(z0)) -> double(exp(z0))
            f(a(),0(),z0) -> z0
            f(a(),s(z0),z1) -> f(b(),z1,s(z0))
            f(b(),z0,z1) -> f(a(),half(z1),exp(z0))
            half(0()) -> double(0())
            half(s(0())) -> half(0())
            half(s(s(z0))) -> s(half(z0))
            tower(z0) -> f(a(),z0,s(0()))
        - Signature:
            {DOUBLE/1,EXP/1,F/3,HALF/1,TOWER/1,double/1,exp/1,f/3,half/1,tower/1} / {0/0,a/0,b/0,c/1,c1/0,c10/1,c11/1
            ,c2/1,c3/2,c4/2,c5/0,c6/2,c7/0,c8/1,c9/1,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {DOUBLE,EXP,F,HALF,TOWER,double,exp,f,half
            ,tower} and constructors {0,a,b,c,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,s}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          DOUBLE(x){x -> s(x)} =
            DOUBLE(s(x)) ->^+ c8(DOUBLE(x))
              = C[DOUBLE(x) = DOUBLE(x){}]

WORST_CASE(Omega(n^1),?)