WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            EVEN(0()) -> c()
            EVEN(s(0())) -> c1()
            EVEN(s(s(z0))) -> c2(EVEN(z0))
            HALF(0()) -> c3()
            HALF(s(s(z0))) -> c4(HALF(z0))
            IF_TIMES(false(),s(z0),z1) -> c11(PLUS(z1,times(z0,z1)),TIMES(z0,z1))
            IF_TIMES(true(),s(z0),z1) -> c10(PLUS(times(half(s(z0)),z1),times(half(s(z0)),z1))
                                            ,TIMES(half(s(z0)),z1)
                                            ,HALF(s(z0)))
            IF_TIMES(true(),s(z0),z1) -> c9(PLUS(times(half(s(z0)),z1),times(half(s(z0)),z1))
                                           ,TIMES(half(s(z0)),z1)
                                           ,HALF(s(z0)))
            PLUS(0(),z0) -> c5()
            PLUS(s(z0),z1) -> c6(PLUS(z0,z1))
            TIMES(0(),z0) -> c7()
            TIMES(s(z0),z1) -> c8(IF_TIMES(even(s(z0)),s(z0),z1),EVEN(s(z0)))
        - Weak TRS:
            even(0()) -> true()
            even(s(0())) -> false()
            even(s(s(z0))) -> even(z0)
            half(0()) -> 0()
            half(s(s(z0))) -> s(half(z0))
            if_times(false(),s(z0),z1) -> plus(z1,times(z0,z1))
            if_times(true(),s(z0),z1) -> plus(times(half(s(z0)),z1),times(half(s(z0)),z1))
            plus(0(),z0) -> z0
            plus(s(z0),z1) -> s(plus(z0,z1))
            times(0(),z0) -> 0()
            times(s(z0),z1) -> if_times(even(s(z0)),s(z0),z1)
        - Signature:
            {EVEN/1,HALF/1,IF_TIMES/3,PLUS/2,TIMES/2,even/1,half/1,if_times/3,plus/2,times/2} / {0/0,c/0,c1/0,c10/3
            ,c11/2,c2/1,c3/0,c4/1,c5/0,c6/1,c7/0,c8/2,c9/3,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {EVEN,HALF,IF_TIMES,PLUS,TIMES,even,half,if_times,plus
            ,times} and constructors {0,c,c1,c10,c11,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:
            EVEN(0()) -> c()
            EVEN(s(0())) -> c1()
            EVEN(s(s(z0))) -> c2(EVEN(z0))
            HALF(0()) -> c3()
            HALF(s(s(z0))) -> c4(HALF(z0))
            IF_TIMES(false(),s(z0),z1) -> c11(PLUS(z1,times(z0,z1)),TIMES(z0,z1))
            IF_TIMES(true(),s(z0),z1) -> c10(PLUS(times(half(s(z0)),z1),times(half(s(z0)),z1))
                                            ,TIMES(half(s(z0)),z1)
                                            ,HALF(s(z0)))
            IF_TIMES(true(),s(z0),z1) -> c9(PLUS(times(half(s(z0)),z1),times(half(s(z0)),z1))
                                           ,TIMES(half(s(z0)),z1)
                                           ,HALF(s(z0)))
            PLUS(0(),z0) -> c5()
            PLUS(s(z0),z1) -> c6(PLUS(z0,z1))
            TIMES(0(),z0) -> c7()
            TIMES(s(z0),z1) -> c8(IF_TIMES(even(s(z0)),s(z0),z1),EVEN(s(z0)))
        - Weak TRS:
            even(0()) -> true()
            even(s(0())) -> false()
            even(s(s(z0))) -> even(z0)
            half(0()) -> 0()
            half(s(s(z0))) -> s(half(z0))
            if_times(false(),s(z0),z1) -> plus(z1,times(z0,z1))
            if_times(true(),s(z0),z1) -> plus(times(half(s(z0)),z1),times(half(s(z0)),z1))
            plus(0(),z0) -> z0
            plus(s(z0),z1) -> s(plus(z0,z1))
            times(0(),z0) -> 0()
            times(s(z0),z1) -> if_times(even(s(z0)),s(z0),z1)
        - Signature:
            {EVEN/1,HALF/1,IF_TIMES/3,PLUS/2,TIMES/2,even/1,half/1,if_times/3,plus/2,times/2} / {0/0,c/0,c1/0,c10/3
            ,c11/2,c2/1,c3/0,c4/1,c5/0,c6/1,c7/0,c8/2,c9/3,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {EVEN,HALF,IF_TIMES,PLUS,TIMES,even,half,if_times,plus
            ,times} and constructors {0,c,c1,c10,c11,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:
            EVEN(0()) -> c()
            EVEN(s(0())) -> c1()
            EVEN(s(s(z0))) -> c2(EVEN(z0))
            HALF(0()) -> c3()
            HALF(s(s(z0))) -> c4(HALF(z0))
            IF_TIMES(false(),s(z0),z1) -> c11(PLUS(z1,times(z0,z1)),TIMES(z0,z1))
            IF_TIMES(true(),s(z0),z1) -> c10(PLUS(times(half(s(z0)),z1),times(half(s(z0)),z1))
                                            ,TIMES(half(s(z0)),z1)
                                            ,HALF(s(z0)))
            IF_TIMES(true(),s(z0),z1) -> c9(PLUS(times(half(s(z0)),z1),times(half(s(z0)),z1))
                                           ,TIMES(half(s(z0)),z1)
                                           ,HALF(s(z0)))
            PLUS(0(),z0) -> c5()
            PLUS(s(z0),z1) -> c6(PLUS(z0,z1))
            TIMES(0(),z0) -> c7()
            TIMES(s(z0),z1) -> c8(IF_TIMES(even(s(z0)),s(z0),z1),EVEN(s(z0)))
        - Weak TRS:
            even(0()) -> true()
            even(s(0())) -> false()
            even(s(s(z0))) -> even(z0)
            half(0()) -> 0()
            half(s(s(z0))) -> s(half(z0))
            if_times(false(),s(z0),z1) -> plus(z1,times(z0,z1))
            if_times(true(),s(z0),z1) -> plus(times(half(s(z0)),z1),times(half(s(z0)),z1))
            plus(0(),z0) -> z0
            plus(s(z0),z1) -> s(plus(z0,z1))
            times(0(),z0) -> 0()
            times(s(z0),z1) -> if_times(even(s(z0)),s(z0),z1)
        - Signature:
            {EVEN/1,HALF/1,IF_TIMES/3,PLUS/2,TIMES/2,even/1,half/1,if_times/3,plus/2,times/2} / {0/0,c/0,c1/0,c10/3
            ,c11/2,c2/1,c3/0,c4/1,c5/0,c6/1,c7/0,c8/2,c9/3,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {EVEN,HALF,IF_TIMES,PLUS,TIMES,even,half,if_times,plus
            ,times} and constructors {0,c,c1,c10,c11,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:
          EVEN(x){x -> s(s(x))} =
            EVEN(s(s(x))) ->^+ c2(EVEN(x))
              = C[EVEN(x) = EVEN(x){}]

WORST_CASE(Omega(n^1),?)