WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            F0(z0,z1,z2) -> c23()
            F0(0(),z0,z1) -> c22(F1(z1,z0,z1))
            F1(z0,z1,z2) -> c24(F2(z0,z1,z2))
            F1(z0,z1,z2) -> c25()
            F2(z0,1(),z1) -> c26(F0(z0,z1,z1))
            GE(z0,0()) -> c19()
            GE(0(),s(z0)) -> c20()
            GE(s(z0),s(z1)) -> c21(GE(z0,z1))
            IFPLUS(false(),z0,z1) -> c4(PLUS(p(z0),z1),P(z0))
            IFPLUS(true(),z0,z1) -> c3(P(z1))
            IFTIMES(false(),z0,z1,z2,z3) -> c8(TIMESITER(inc(z0),z1,z2,plus(z3,z2)),INC(z0))
            IFTIMES(false(),z0,z1,z2,z3) -> c9(TIMESITER(inc(z0),z1,z2,plus(z3,z2)),PLUS(z3,z2))
            IFTIMES(true(),z0,z1,z2,z3) -> c7()
            INC(z0) -> c15()
            INC(0()) -> c13()
            INC(s(z0)) -> c14(INC(z0))
            ISZERO(0()) -> c10()
            ISZERO(s(0())) -> c11()
            ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
            P(0()) -> c16()
            P(s(z0)) -> c17()
            P(s(s(z0))) -> c18(P(s(z0)))
            PLUS(z0,z1) -> c1(IFPLUS(isZero(z0),z0,inc(z1)),ISZERO(z0))
            PLUS(z0,z1) -> c2(IFPLUS(isZero(z0),z0,inc(z1)),INC(z1))
            TIMES(z0,z1) -> c5(TIMESITER(0(),z0,z1,0()))
            TIMESITER(z0,z1,z2,z3) -> c6(IFTIMES(ge(z0,z1),z0,z1,z2,z3),GE(z0,z1))
        - Weak TRS:
            f0(z0,z1,z2) -> d()
            f0(0(),z0,z1) -> f1(z1,z0,z1)
            f1(z0,z1,z2) -> c()
            f1(z0,z1,z2) -> f2(z0,z1,z2)
            f2(z0,1(),z1) -> f0(z0,z1,z1)
            ge(z0,0()) -> true()
            ge(0(),s(z0)) -> false()
            ge(s(z0),s(z1)) -> ge(z0,z1)
            ifPlus(false(),z0,z1) -> plus(p(z0),z1)
            ifPlus(true(),z0,z1) -> p(z1)
            ifTimes(false(),z0,z1,z2,z3) -> timesIter(inc(z0),z1,z2,plus(z3,z2))
            ifTimes(true(),z0,z1,z2,z3) -> z3
            inc(z0) -> s(z0)
            inc(0()) -> s(0())
            inc(s(z0)) -> s(inc(z0))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(z0))) -> isZero(s(z0))
            p(0()) -> 0()
            p(s(z0)) -> z0
            p(s(s(z0))) -> s(p(s(z0)))
            plus(z0,z1) -> ifPlus(isZero(z0),z0,inc(z1))
            times(z0,z1) -> timesIter(0(),z0,z1,0())
            timesIter(z0,z1,z2,z3) -> ifTimes(ge(z0,z1),z0,z1,z2,z3)
        - Signature:
            {F0/3,F1/3,F2/3,GE/2,IFPLUS/3,IFTIMES/5,INC/1,ISZERO/1,P/1,PLUS/2,TIMES/2,TIMESITER/4,f0/3,f1/3,f2/3,ge/2
            ,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4} / {0/0,1/0,c/0,c1/2,c10/0,c11/0,c12/1
            ,c13/0,c14/1,c15/0,c16/0,c17/0,c18/1,c19/0,c2/2,c20/0,c21/1,c22/1,c23/0,c24/1,c25/0,c26/1,c3/1,c4/2,c5/1
            ,c6/2,c7/0,c8/2,c9/2,d/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {F0,F1,F2,GE,IFPLUS,IFTIMES,INC,ISZERO,P,PLUS,TIMES
            ,TIMESITER,f0,f1,f2,ge,ifPlus,ifTimes,inc,isZero,p,plus,times,timesIter} and constructors {0,1,c,c1,c10,c11
            ,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c3,c4,c5,c6,c7,c8,c9,d,false,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            F0(z0,z1,z2) -> c23()
            F0(0(),z0,z1) -> c22(F1(z1,z0,z1))
            F1(z0,z1,z2) -> c24(F2(z0,z1,z2))
            F1(z0,z1,z2) -> c25()
            F2(z0,1(),z1) -> c26(F0(z0,z1,z1))
            GE(z0,0()) -> c19()
            GE(0(),s(z0)) -> c20()
            GE(s(z0),s(z1)) -> c21(GE(z0,z1))
            IFPLUS(false(),z0,z1) -> c4(PLUS(p(z0),z1),P(z0))
            IFPLUS(true(),z0,z1) -> c3(P(z1))
            IFTIMES(false(),z0,z1,z2,z3) -> c8(TIMESITER(inc(z0),z1,z2,plus(z3,z2)),INC(z0))
            IFTIMES(false(),z0,z1,z2,z3) -> c9(TIMESITER(inc(z0),z1,z2,plus(z3,z2)),PLUS(z3,z2))
            IFTIMES(true(),z0,z1,z2,z3) -> c7()
            INC(z0) -> c15()
            INC(0()) -> c13()
            INC(s(z0)) -> c14(INC(z0))
            ISZERO(0()) -> c10()
            ISZERO(s(0())) -> c11()
            ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
            P(0()) -> c16()
            P(s(z0)) -> c17()
            P(s(s(z0))) -> c18(P(s(z0)))
            PLUS(z0,z1) -> c1(IFPLUS(isZero(z0),z0,inc(z1)),ISZERO(z0))
            PLUS(z0,z1) -> c2(IFPLUS(isZero(z0),z0,inc(z1)),INC(z1))
            TIMES(z0,z1) -> c5(TIMESITER(0(),z0,z1,0()))
            TIMESITER(z0,z1,z2,z3) -> c6(IFTIMES(ge(z0,z1),z0,z1,z2,z3),GE(z0,z1))
        - Weak TRS:
            f0(z0,z1,z2) -> d()
            f0(0(),z0,z1) -> f1(z1,z0,z1)
            f1(z0,z1,z2) -> c()
            f1(z0,z1,z2) -> f2(z0,z1,z2)
            f2(z0,1(),z1) -> f0(z0,z1,z1)
            ge(z0,0()) -> true()
            ge(0(),s(z0)) -> false()
            ge(s(z0),s(z1)) -> ge(z0,z1)
            ifPlus(false(),z0,z1) -> plus(p(z0),z1)
            ifPlus(true(),z0,z1) -> p(z1)
            ifTimes(false(),z0,z1,z2,z3) -> timesIter(inc(z0),z1,z2,plus(z3,z2))
            ifTimes(true(),z0,z1,z2,z3) -> z3
            inc(z0) -> s(z0)
            inc(0()) -> s(0())
            inc(s(z0)) -> s(inc(z0))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(z0))) -> isZero(s(z0))
            p(0()) -> 0()
            p(s(z0)) -> z0
            p(s(s(z0))) -> s(p(s(z0)))
            plus(z0,z1) -> ifPlus(isZero(z0),z0,inc(z1))
            times(z0,z1) -> timesIter(0(),z0,z1,0())
            timesIter(z0,z1,z2,z3) -> ifTimes(ge(z0,z1),z0,z1,z2,z3)
        - Signature:
            {F0/3,F1/3,F2/3,GE/2,IFPLUS/3,IFTIMES/5,INC/1,ISZERO/1,P/1,PLUS/2,TIMES/2,TIMESITER/4,f0/3,f1/3,f2/3,ge/2
            ,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4} / {0/0,1/0,c/0,c1/2,c10/0,c11/0,c12/1
            ,c13/0,c14/1,c15/0,c16/0,c17/0,c18/1,c19/0,c2/2,c20/0,c21/1,c22/1,c23/0,c24/1,c25/0,c26/1,c3/1,c4/2,c5/1
            ,c6/2,c7/0,c8/2,c9/2,d/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {F0,F1,F2,GE,IFPLUS,IFTIMES,INC,ISZERO,P,PLUS,TIMES
            ,TIMESITER,f0,f1,f2,ge,ifPlus,ifTimes,inc,isZero,p,plus,times,timesIter} and constructors {0,1,c,c1,c10,c11
            ,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c3,c4,c5,c6,c7,c8,c9,d,false,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            F0(z0,z1,z2) -> c23()
            F0(0(),z0,z1) -> c22(F1(z1,z0,z1))
            F1(z0,z1,z2) -> c24(F2(z0,z1,z2))
            F1(z0,z1,z2) -> c25()
            F2(z0,1(),z1) -> c26(F0(z0,z1,z1))
            GE(z0,0()) -> c19()
            GE(0(),s(z0)) -> c20()
            GE(s(z0),s(z1)) -> c21(GE(z0,z1))
            IFPLUS(false(),z0,z1) -> c4(PLUS(p(z0),z1),P(z0))
            IFPLUS(true(),z0,z1) -> c3(P(z1))
            IFTIMES(false(),z0,z1,z2,z3) -> c8(TIMESITER(inc(z0),z1,z2,plus(z3,z2)),INC(z0))
            IFTIMES(false(),z0,z1,z2,z3) -> c9(TIMESITER(inc(z0),z1,z2,plus(z3,z2)),PLUS(z3,z2))
            IFTIMES(true(),z0,z1,z2,z3) -> c7()
            INC(z0) -> c15()
            INC(0()) -> c13()
            INC(s(z0)) -> c14(INC(z0))
            ISZERO(0()) -> c10()
            ISZERO(s(0())) -> c11()
            ISZERO(s(s(z0))) -> c12(ISZERO(s(z0)))
            P(0()) -> c16()
            P(s(z0)) -> c17()
            P(s(s(z0))) -> c18(P(s(z0)))
            PLUS(z0,z1) -> c1(IFPLUS(isZero(z0),z0,inc(z1)),ISZERO(z0))
            PLUS(z0,z1) -> c2(IFPLUS(isZero(z0),z0,inc(z1)),INC(z1))
            TIMES(z0,z1) -> c5(TIMESITER(0(),z0,z1,0()))
            TIMESITER(z0,z1,z2,z3) -> c6(IFTIMES(ge(z0,z1),z0,z1,z2,z3),GE(z0,z1))
        - Weak TRS:
            f0(z0,z1,z2) -> d()
            f0(0(),z0,z1) -> f1(z1,z0,z1)
            f1(z0,z1,z2) -> c()
            f1(z0,z1,z2) -> f2(z0,z1,z2)
            f2(z0,1(),z1) -> f0(z0,z1,z1)
            ge(z0,0()) -> true()
            ge(0(),s(z0)) -> false()
            ge(s(z0),s(z1)) -> ge(z0,z1)
            ifPlus(false(),z0,z1) -> plus(p(z0),z1)
            ifPlus(true(),z0,z1) -> p(z1)
            ifTimes(false(),z0,z1,z2,z3) -> timesIter(inc(z0),z1,z2,plus(z3,z2))
            ifTimes(true(),z0,z1,z2,z3) -> z3
            inc(z0) -> s(z0)
            inc(0()) -> s(0())
            inc(s(z0)) -> s(inc(z0))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(z0))) -> isZero(s(z0))
            p(0()) -> 0()
            p(s(z0)) -> z0
            p(s(s(z0))) -> s(p(s(z0)))
            plus(z0,z1) -> ifPlus(isZero(z0),z0,inc(z1))
            times(z0,z1) -> timesIter(0(),z0,z1,0())
            timesIter(z0,z1,z2,z3) -> ifTimes(ge(z0,z1),z0,z1,z2,z3)
        - Signature:
            {F0/3,F1/3,F2/3,GE/2,IFPLUS/3,IFTIMES/5,INC/1,ISZERO/1,P/1,PLUS/2,TIMES/2,TIMESITER/4,f0/3,f1/3,f2/3,ge/2
            ,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4} / {0/0,1/0,c/0,c1/2,c10/0,c11/0,c12/1
            ,c13/0,c14/1,c15/0,c16/0,c17/0,c18/1,c19/0,c2/2,c20/0,c21/1,c22/1,c23/0,c24/1,c25/0,c26/1,c3/1,c4/2,c5/1
            ,c6/2,c7/0,c8/2,c9/2,d/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {F0,F1,F2,GE,IFPLUS,IFTIMES,INC,ISZERO,P,PLUS,TIMES
            ,TIMESITER,f0,f1,f2,ge,ifPlus,ifTimes,inc,isZero,p,plus,times,timesIter} and constructors {0,1,c,c1,c10,c11
            ,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c3,c4,c5,c6,c7,c8,c9,d,false,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          GE(x,y){x -> s(x),y -> s(y)} =
            GE(s(x),s(y)) ->^+ c21(GE(x,y))
              = C[GE(x,y) = GE(x,y){}]

WORST_CASE(Omega(n^1),?)