tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
tct-trs: Prelude.head: empty list
WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            CHECK(0()) -> c()
            CHECK(s(0())) -> c1()
            CHECK(s(s(0()))) -> c2()
            CHECK(s(s(s(z0)))) -> c3(CHECK(s(z0)))
            HALF(0()) -> c4()
            HALF(s(0())) -> c5()
            HALF(s(s(z0))) -> c6(HALF(z0))
            IF(even(),z0,z1,z2,z3) -> c16(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(z2))
                                         ,HALF(z0))
            IF(even(),z0,z1,z2,z3) -> c17(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(z2))
                                         ,HALF(z2))
            IF(even(),z0,z1,z2,z3) -> c18(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(s(z2)))
                                         ,HALF(z0))
            IF(even(),z0,z1,z2,z3) -> c19(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(s(z2)))
                                         ,HALF(s(z2)))
            IF(odd(),z0,z1,z2,z3) -> c15(TIMESITER(p(z0),z1,z3),P(z0))
            IF(zero(),z0,z1,z2,z3) -> c14()
            P(0()) -> c13()
            P(s(z0)) -> c12()
            PLUS(0(),z0) -> c7()
            PLUS(s(z0),z1) -> c8(PLUS(z0,z1))
            TIMES(z0,z1) -> c9(TIMESITER(z0,z1,0()))
            TIMESITER(z0,z1,z2) -> c10(IF(check(z0),z0,z1,z2,plus(z2,z1)),CHECK(z0))
            TIMESITER(z0,z1,z2) -> c11(IF(check(z0),z0,z1,z2,plus(z2,z1)),PLUS(z2,z1))
        - Weak TRS:
            check(0()) -> zero()
            check(s(0())) -> odd()
            check(s(s(0()))) -> even()
            check(s(s(s(z0)))) -> check(s(z0))
            half(0()) -> 0()
            half(s(0())) -> 0()
            half(s(s(z0))) -> s(half(z0))
            if(even(),z0,z1,z2,z3) -> plus(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
            if(odd(),z0,z1,z2,z3) -> timesIter(p(z0),z1,z3)
            if(zero(),z0,z1,z2,z3) -> z2
            p(0()) -> 0()
            p(s(z0)) -> z0
            plus(0(),z0) -> z0
            plus(s(z0),z1) -> s(plus(z0,z1))
            times(z0,z1) -> timesIter(z0,z1,0())
            timesIter(z0,z1,z2) -> if(check(z0),z0,z1,z2,plus(z2,z1))
        - Signature:
            {CHECK/1,HALF/1,IF/5,P/1,PLUS/2,TIMES/2,TIMESITER/3,check/1,half/1,if/5,p/1,plus/2,times/2
            ,timesIter/3} / {0/0,c/0,c1/0,c10/2,c11/2,c12/0,c13/0,c14/0,c15/2,c16/3,c17/3,c18/3,c19/3,c2/0,c3/1,c4/0
            ,c5/0,c6/1,c7/0,c8/1,c9/1,even/0,odd/0,s/1,zero/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {CHECK,HALF,IF,P,PLUS,TIMES,TIMESITER,check,half,if,p,plus
            ,times,timesIter} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c3,c4,c5,c6,c7,c8,c9
            ,even,odd,s,zero}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            CHECK(0()) -> c()
            CHECK(s(0())) -> c1()
            CHECK(s(s(0()))) -> c2()
            CHECK(s(s(s(z0)))) -> c3(CHECK(s(z0)))
            HALF(0()) -> c4()
            HALF(s(0())) -> c5()
            HALF(s(s(z0))) -> c6(HALF(z0))
            IF(even(),z0,z1,z2,z3) -> c16(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(z2))
                                         ,HALF(z0))
            IF(even(),z0,z1,z2,z3) -> c17(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(z2))
                                         ,HALF(z2))
            IF(even(),z0,z1,z2,z3) -> c18(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(s(z2)))
                                         ,HALF(z0))
            IF(even(),z0,z1,z2,z3) -> c19(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(s(z2)))
                                         ,HALF(s(z2)))
            IF(odd(),z0,z1,z2,z3) -> c15(TIMESITER(p(z0),z1,z3),P(z0))
            IF(zero(),z0,z1,z2,z3) -> c14()
            P(0()) -> c13()
            P(s(z0)) -> c12()
            PLUS(0(),z0) -> c7()
            PLUS(s(z0),z1) -> c8(PLUS(z0,z1))
            TIMES(z0,z1) -> c9(TIMESITER(z0,z1,0()))
            TIMESITER(z0,z1,z2) -> c10(IF(check(z0),z0,z1,z2,plus(z2,z1)),CHECK(z0))
            TIMESITER(z0,z1,z2) -> c11(IF(check(z0),z0,z1,z2,plus(z2,z1)),PLUS(z2,z1))
        - Weak TRS:
            check(0()) -> zero()
            check(s(0())) -> odd()
            check(s(s(0()))) -> even()
            check(s(s(s(z0)))) -> check(s(z0))
            half(0()) -> 0()
            half(s(0())) -> 0()
            half(s(s(z0))) -> s(half(z0))
            if(even(),z0,z1,z2,z3) -> plus(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
            if(odd(),z0,z1,z2,z3) -> timesIter(p(z0),z1,z3)
            if(zero(),z0,z1,z2,z3) -> z2
            p(0()) -> 0()
            p(s(z0)) -> z0
            plus(0(),z0) -> z0
            plus(s(z0),z1) -> s(plus(z0,z1))
            times(z0,z1) -> timesIter(z0,z1,0())
            timesIter(z0,z1,z2) -> if(check(z0),z0,z1,z2,plus(z2,z1))
        - Signature:
            {CHECK/1,HALF/1,IF/5,P/1,PLUS/2,TIMES/2,TIMESITER/3,check/1,half/1,if/5,p/1,plus/2,times/2
            ,timesIter/3} / {0/0,c/0,c1/0,c10/2,c11/2,c12/0,c13/0,c14/0,c15/2,c16/3,c17/3,c18/3,c19/3,c2/0,c3/1,c4/0
            ,c5/0,c6/1,c7/0,c8/1,c9/1,even/0,odd/0,s/1,zero/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {CHECK,HALF,IF,P,PLUS,TIMES,TIMESITER,check,half,if,p,plus
            ,times,timesIter} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c3,c4,c5,c6,c7,c8,c9
            ,even,odd,s,zero}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            CHECK(0()) -> c()
            CHECK(s(0())) -> c1()
            CHECK(s(s(0()))) -> c2()
            CHECK(s(s(s(z0)))) -> c3(CHECK(s(z0)))
            HALF(0()) -> c4()
            HALF(s(0())) -> c5()
            HALF(s(s(z0))) -> c6(HALF(z0))
            IF(even(),z0,z1,z2,z3) -> c16(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(z2))
                                         ,HALF(z0))
            IF(even(),z0,z1,z2,z3) -> c17(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(z2))
                                         ,HALF(z2))
            IF(even(),z0,z1,z2,z3) -> c18(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(s(z2)))
                                         ,HALF(z0))
            IF(even(),z0,z1,z2,z3) -> c19(PLUS(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
                                         ,TIMESITER(half(z0),z1,half(s(z2)))
                                         ,HALF(s(z2)))
            IF(odd(),z0,z1,z2,z3) -> c15(TIMESITER(p(z0),z1,z3),P(z0))
            IF(zero(),z0,z1,z2,z3) -> c14()
            P(0()) -> c13()
            P(s(z0)) -> c12()
            PLUS(0(),z0) -> c7()
            PLUS(s(z0),z1) -> c8(PLUS(z0,z1))
            TIMES(z0,z1) -> c9(TIMESITER(z0,z1,0()))
            TIMESITER(z0,z1,z2) -> c10(IF(check(z0),z0,z1,z2,plus(z2,z1)),CHECK(z0))
            TIMESITER(z0,z1,z2) -> c11(IF(check(z0),z0,z1,z2,plus(z2,z1)),PLUS(z2,z1))
        - Weak TRS:
            check(0()) -> zero()
            check(s(0())) -> odd()
            check(s(s(0()))) -> even()
            check(s(s(s(z0)))) -> check(s(z0))
            half(0()) -> 0()
            half(s(0())) -> 0()
            half(s(s(z0))) -> s(half(z0))
            if(even(),z0,z1,z2,z3) -> plus(timesIter(half(z0),z1,half(z2)),timesIter(half(z0),z1,half(s(z2))))
            if(odd(),z0,z1,z2,z3) -> timesIter(p(z0),z1,z3)
            if(zero(),z0,z1,z2,z3) -> z2
            p(0()) -> 0()
            p(s(z0)) -> z0
            plus(0(),z0) -> z0
            plus(s(z0),z1) -> s(plus(z0,z1))
            times(z0,z1) -> timesIter(z0,z1,0())
            timesIter(z0,z1,z2) -> if(check(z0),z0,z1,z2,plus(z2,z1))
        - Signature:
            {CHECK/1,HALF/1,IF/5,P/1,PLUS/2,TIMES/2,TIMESITER/3,check/1,half/1,if/5,p/1,plus/2,times/2
            ,timesIter/3} / {0/0,c/0,c1/0,c10/2,c11/2,c12/0,c13/0,c14/0,c15/2,c16/3,c17/3,c18/3,c19/3,c2/0,c3/1,c4/0
            ,c5/0,c6/1,c7/0,c8/1,c9/1,even/0,odd/0,s/1,zero/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {CHECK,HALF,IF,P,PLUS,TIMES,TIMESITER,check,half,if,p,plus
            ,times,timesIter} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c3,c4,c5,c6,c7,c8,c9
            ,even,odd,s,zero}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          CHECK(s(x)){x -> s(s(x))} =
            CHECK(s(s(s(x)))) ->^+ c3(CHECK(s(x)))
              = C[CHECK(s(x)) = CHECK(s(x)){}]

WORST_CASE(Omega(n^1),?)