WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            FUNCTION(if(),false(),z0,z1) -> c7(FUNCTION(plus(),function(third(),z0,z1,z1),function(p(),z0,z0,z1),s(z1))
                                              ,FUNCTION(third(),z0,z1,z1))
            FUNCTION(if(),false(),z0,z1) -> c8(FUNCTION(plus(),function(third(),z0,z1,z1),function(p(),z0,z0,z1),s(z1))
                                              ,FUNCTION(p(),z0,z0,z1))
            FUNCTION(if(),true(),z0,z1) -> c6()
            FUNCTION(iszero(),0(),z0,z1) -> c()
            FUNCTION(iszero(),s(z0),z1,z2) -> c1()
            FUNCTION(p(),0(),z0,z1) -> c2()
            FUNCTION(p(),s(0()),z0,z1) -> c3()
            FUNCTION(p(),s(s(z0)),z1,z2) -> c4(FUNCTION(p(),s(z0),z0,z0))
            FUNCTION(plus(),z0,z1,z2) -> c5(FUNCTION(if(),function(iszero(),z1,z1,z1),z1,z2)
                                           ,FUNCTION(iszero(),z1,z1,z1))
            FUNCTION(third(),z0,z1,z2) -> c9()
        - Weak TRS:
            function(if(),false(),z0,z1) -> function(plus(),function(third(),z0,z1,z1),function(p(),z0,z0,z1),s(z1))
            function(if(),true(),z0,z1) -> z1
            function(iszero(),0(),z0,z1) -> true()
            function(iszero(),s(z0),z1,z2) -> false()
            function(p(),0(),z0,z1) -> 0()
            function(p(),s(0()),z0,z1) -> 0()
            function(p(),s(s(z0)),z1,z2) -> s(function(p(),s(z0),z0,z0))
            function(plus(),z0,z1,z2) -> function(if(),function(iszero(),z1,z1,z1),z1,z2)
            function(third(),z0,z1,z2) -> z2
        - Signature:
            {FUNCTION/4,function/4} / {0/0,c/0,c1/0,c2/0,c3/0,c4/1,c5/2,c6/0,c7/2,c8/2,c9/0,false/0,if/0,iszero/0,p/0
            ,plus/0,s/1,third/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {FUNCTION,function} and constructors {0,c,c1,c2,c3,c4,c5
            ,c6,c7,c8,c9,false,if,iszero,p,plus,s,third,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            FUNCTION(if(),false(),z0,z1) -> c7(FUNCTION(plus(),function(third(),z0,z1,z1),function(p(),z0,z0,z1),s(z1))
                                              ,FUNCTION(third(),z0,z1,z1))
            FUNCTION(if(),false(),z0,z1) -> c8(FUNCTION(plus(),function(third(),z0,z1,z1),function(p(),z0,z0,z1),s(z1))
                                              ,FUNCTION(p(),z0,z0,z1))
            FUNCTION(if(),true(),z0,z1) -> c6()
            FUNCTION(iszero(),0(),z0,z1) -> c()
            FUNCTION(iszero(),s(z0),z1,z2) -> c1()
            FUNCTION(p(),0(),z0,z1) -> c2()
            FUNCTION(p(),s(0()),z0,z1) -> c3()
            FUNCTION(p(),s(s(z0)),z1,z2) -> c4(FUNCTION(p(),s(z0),z0,z0))
            FUNCTION(plus(),z0,z1,z2) -> c5(FUNCTION(if(),function(iszero(),z1,z1,z1),z1,z2)
                                           ,FUNCTION(iszero(),z1,z1,z1))
            FUNCTION(third(),z0,z1,z2) -> c9()
        - Weak TRS:
            function(if(),false(),z0,z1) -> function(plus(),function(third(),z0,z1,z1),function(p(),z0,z0,z1),s(z1))
            function(if(),true(),z0,z1) -> z1
            function(iszero(),0(),z0,z1) -> true()
            function(iszero(),s(z0),z1,z2) -> false()
            function(p(),0(),z0,z1) -> 0()
            function(p(),s(0()),z0,z1) -> 0()
            function(p(),s(s(z0)),z1,z2) -> s(function(p(),s(z0),z0,z0))
            function(plus(),z0,z1,z2) -> function(if(),function(iszero(),z1,z1,z1),z1,z2)
            function(third(),z0,z1,z2) -> z2
        - Signature:
            {FUNCTION/4,function/4} / {0/0,c/0,c1/0,c2/0,c3/0,c4/1,c5/2,c6/0,c7/2,c8/2,c9/0,false/0,if/0,iszero/0,p/0
            ,plus/0,s/1,third/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {FUNCTION,function} and constructors {0,c,c1,c2,c3,c4,c5
            ,c6,c7,c8,c9,false,if,iszero,p,plus,s,third,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            FUNCTION(if(),false(),z0,z1) -> c7(FUNCTION(plus(),function(third(),z0,z1,z1),function(p(),z0,z0,z1),s(z1))
                                              ,FUNCTION(third(),z0,z1,z1))
            FUNCTION(if(),false(),z0,z1) -> c8(FUNCTION(plus(),function(third(),z0,z1,z1),function(p(),z0,z0,z1),s(z1))
                                              ,FUNCTION(p(),z0,z0,z1))
            FUNCTION(if(),true(),z0,z1) -> c6()
            FUNCTION(iszero(),0(),z0,z1) -> c()
            FUNCTION(iszero(),s(z0),z1,z2) -> c1()
            FUNCTION(p(),0(),z0,z1) -> c2()
            FUNCTION(p(),s(0()),z0,z1) -> c3()
            FUNCTION(p(),s(s(z0)),z1,z2) -> c4(FUNCTION(p(),s(z0),z0,z0))
            FUNCTION(plus(),z0,z1,z2) -> c5(FUNCTION(if(),function(iszero(),z1,z1,z1),z1,z2)
                                           ,FUNCTION(iszero(),z1,z1,z1))
            FUNCTION(third(),z0,z1,z2) -> c9()
        - Weak TRS:
            function(if(),false(),z0,z1) -> function(plus(),function(third(),z0,z1,z1),function(p(),z0,z0,z1),s(z1))
            function(if(),true(),z0,z1) -> z1
            function(iszero(),0(),z0,z1) -> true()
            function(iszero(),s(z0),z1,z2) -> false()
            function(p(),0(),z0,z1) -> 0()
            function(p(),s(0()),z0,z1) -> 0()
            function(p(),s(s(z0)),z1,z2) -> s(function(p(),s(z0),z0,z0))
            function(plus(),z0,z1,z2) -> function(if(),function(iszero(),z1,z1,z1),z1,z2)
            function(third(),z0,z1,z2) -> z2
        - Signature:
            {FUNCTION/4,function/4} / {0/0,c/0,c1/0,c2/0,c3/0,c4/1,c5/2,c6/0,c7/2,c8/2,c9/0,false/0,if/0,iszero/0,p/0
            ,plus/0,s/1,third/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {FUNCTION,function} and constructors {0,c,c1,c2,c3,c4,c5
            ,c6,c7,c8,c9,false,if,iszero,p,plus,s,third,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          FUNCTION(p(),s(x),y,z){x -> s(x)} =
            FUNCTION(p(),s(s(x)),y,z) ->^+ c4(FUNCTION(p(),s(x),x,x))
              = C[FUNCTION(p(),s(x),x,x) = FUNCTION(p(),s(x),y,z){y -> x,z -> x}]

WORST_CASE(Omega(n^1),?)