WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            COND(false(),z0,z1) -> c2(DOUBLE(log(z0,square(s(s(z1))))),LOG(z0,square(s(s(z1)))),SQUARE(s(s(z1))))
            COND(true(),z0,z1) -> c1()
            DOUBLE(0()) -> c6()
            DOUBLE(s(z0)) -> c7(DOUBLE(z0))
            LE(0(),z0) -> c3()
            LE(s(z0),0()) -> c4()
            LE(s(z0),s(z1)) -> c5(LE(z0,z1))
            LOG(z0,s(s(z1))) -> c(COND(le(z0,s(s(z1))),z0,z1),LE(z0,s(s(z1))))
            PLUS(z0,0()) -> c11()
            PLUS(z0,s(z1)) -> c12(PLUS(z0,z1))
            SQUARE(0()) -> c8()
            SQUARE(s(z0)) -> c10(PLUS(square(z0),double(z0)),DOUBLE(z0))
            SQUARE(s(z0)) -> c9(PLUS(square(z0),double(z0)),SQUARE(z0))
        - Weak TRS:
            cond(false(),z0,z1) -> double(log(z0,square(s(s(z1)))))
            cond(true(),z0,z1) -> s(0())
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            log(z0,s(s(z1))) -> cond(le(z0,s(s(z1))),z0,z1)
            plus(z0,0()) -> z0
            plus(z0,s(z1)) -> s(plus(z0,z1))
            square(0()) -> 0()
            square(s(z0)) -> s(plus(square(z0),double(z0)))
        - Signature:
            {COND/3,DOUBLE/1,LE/2,LOG/2,PLUS/2,SQUARE/1,cond/3,double/1,le/2,log/2,plus/2,square/1} / {0/0,c/2,c1/0
            ,c10/2,c11/0,c12/1,c2/3,c3/0,c4/0,c5/1,c6/0,c7/1,c8/0,c9/2,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {COND,DOUBLE,LE,LOG,PLUS,SQUARE,cond,double,le,log,plus
            ,square} and constructors {0,c,c1,c10,c11,c12,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            COND(false(),z0,z1) -> c2(DOUBLE(log(z0,square(s(s(z1))))),LOG(z0,square(s(s(z1)))),SQUARE(s(s(z1))))
            COND(true(),z0,z1) -> c1()
            DOUBLE(0()) -> c6()
            DOUBLE(s(z0)) -> c7(DOUBLE(z0))
            LE(0(),z0) -> c3()
            LE(s(z0),0()) -> c4()
            LE(s(z0),s(z1)) -> c5(LE(z0,z1))
            LOG(z0,s(s(z1))) -> c(COND(le(z0,s(s(z1))),z0,z1),LE(z0,s(s(z1))))
            PLUS(z0,0()) -> c11()
            PLUS(z0,s(z1)) -> c12(PLUS(z0,z1))
            SQUARE(0()) -> c8()
            SQUARE(s(z0)) -> c10(PLUS(square(z0),double(z0)),DOUBLE(z0))
            SQUARE(s(z0)) -> c9(PLUS(square(z0),double(z0)),SQUARE(z0))
        - Weak TRS:
            cond(false(),z0,z1) -> double(log(z0,square(s(s(z1)))))
            cond(true(),z0,z1) -> s(0())
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            log(z0,s(s(z1))) -> cond(le(z0,s(s(z1))),z0,z1)
            plus(z0,0()) -> z0
            plus(z0,s(z1)) -> s(plus(z0,z1))
            square(0()) -> 0()
            square(s(z0)) -> s(plus(square(z0),double(z0)))
        - Signature:
            {COND/3,DOUBLE/1,LE/2,LOG/2,PLUS/2,SQUARE/1,cond/3,double/1,le/2,log/2,plus/2,square/1} / {0/0,c/2,c1/0
            ,c10/2,c11/0,c12/1,c2/3,c3/0,c4/0,c5/1,c6/0,c7/1,c8/0,c9/2,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {COND,DOUBLE,LE,LOG,PLUS,SQUARE,cond,double,le,log,plus
            ,square} and constructors {0,c,c1,c10,c11,c12,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            COND(false(),z0,z1) -> c2(DOUBLE(log(z0,square(s(s(z1))))),LOG(z0,square(s(s(z1)))),SQUARE(s(s(z1))))
            COND(true(),z0,z1) -> c1()
            DOUBLE(0()) -> c6()
            DOUBLE(s(z0)) -> c7(DOUBLE(z0))
            LE(0(),z0) -> c3()
            LE(s(z0),0()) -> c4()
            LE(s(z0),s(z1)) -> c5(LE(z0,z1))
            LOG(z0,s(s(z1))) -> c(COND(le(z0,s(s(z1))),z0,z1),LE(z0,s(s(z1))))
            PLUS(z0,0()) -> c11()
            PLUS(z0,s(z1)) -> c12(PLUS(z0,z1))
            SQUARE(0()) -> c8()
            SQUARE(s(z0)) -> c10(PLUS(square(z0),double(z0)),DOUBLE(z0))
            SQUARE(s(z0)) -> c9(PLUS(square(z0),double(z0)),SQUARE(z0))
        - Weak TRS:
            cond(false(),z0,z1) -> double(log(z0,square(s(s(z1)))))
            cond(true(),z0,z1) -> s(0())
            double(0()) -> 0()
            double(s(z0)) -> s(s(double(z0)))
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            log(z0,s(s(z1))) -> cond(le(z0,s(s(z1))),z0,z1)
            plus(z0,0()) -> z0
            plus(z0,s(z1)) -> s(plus(z0,z1))
            square(0()) -> 0()
            square(s(z0)) -> s(plus(square(z0),double(z0)))
        - Signature:
            {COND/3,DOUBLE/1,LE/2,LOG/2,PLUS/2,SQUARE/1,cond/3,double/1,le/2,log/2,plus/2,square/1} / {0/0,c/2,c1/0
            ,c10/2,c11/0,c12/1,c2/3,c3/0,c4/0,c5/1,c6/0,c7/1,c8/0,c9/2,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {COND,DOUBLE,LE,LOG,PLUS,SQUARE,cond,double,le,log,plus
            ,square} and constructors {0,c,c1,c10,c11,c12,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          DOUBLE(x){x -> s(x)} =
            DOUBLE(s(x)) ->^+ c7(DOUBLE(x))
              = C[DOUBLE(x) = DOUBLE(x){}]

WORST_CASE(Omega(n^1),?)