WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            *'(z0,0()) -> c3()
            *'(0(),z0) -> c4()
            *'(s(z0),s(z1)) -> c5(+'(*(z0,z1),+(z0,z1)),*'(z0,z1))
            *'(s(z0),s(z1)) -> c6(+'(*(z0,z1),+(z0,z1)),+'(z0,z1))
            +'(z0,0()) -> c()
            +'(0(),z0) -> c1()
            +'(s(z0),s(z1)) -> c2(+'(z0,z1))
            PROD(cons(z0,z1)) -> c10(*'(z0,prod(z1)),PROD(z1))
            PROD(nil()) -> c9()
            SUM(cons(z0,z1)) -> c8(+'(z0,sum(z1)),SUM(z1))
            SUM(nil()) -> c7()
        - Weak TRS:
            *(z0,0()) -> 0()
            *(0(),z0) -> 0()
            *(s(z0),s(z1)) -> s(+(*(z0,z1),+(z0,z1)))
            +(z0,0()) -> z0
            +(0(),z0) -> z0
            +(s(z0),s(z1)) -> s(s(+(z0,z1)))
            prod(cons(z0,z1)) -> *(z0,prod(z1))
            prod(nil()) -> s(0())
            sum(cons(z0,z1)) -> +(z0,sum(z1))
            sum(nil()) -> 0()
        - Signature:
            {*/2,*'/2,+/2,+'/2,PROD/1,SUM/1,prod/1,sum/1} / {0/0,c/0,c1/0,c10/2,c2/1,c3/0,c4/0,c5/2,c6/2,c7/0,c8/2,c9/0
            ,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*,*',+,+',PROD,SUM,prod,sum} and constructors {0,c,c1,c10
            ,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            *'(z0,0()) -> c3()
            *'(0(),z0) -> c4()
            *'(s(z0),s(z1)) -> c5(+'(*(z0,z1),+(z0,z1)),*'(z0,z1))
            *'(s(z0),s(z1)) -> c6(+'(*(z0,z1),+(z0,z1)),+'(z0,z1))
            +'(z0,0()) -> c()
            +'(0(),z0) -> c1()
            +'(s(z0),s(z1)) -> c2(+'(z0,z1))
            PROD(cons(z0,z1)) -> c10(*'(z0,prod(z1)),PROD(z1))
            PROD(nil()) -> c9()
            SUM(cons(z0,z1)) -> c8(+'(z0,sum(z1)),SUM(z1))
            SUM(nil()) -> c7()
        - Weak TRS:
            *(z0,0()) -> 0()
            *(0(),z0) -> 0()
            *(s(z0),s(z1)) -> s(+(*(z0,z1),+(z0,z1)))
            +(z0,0()) -> z0
            +(0(),z0) -> z0
            +(s(z0),s(z1)) -> s(s(+(z0,z1)))
            prod(cons(z0,z1)) -> *(z0,prod(z1))
            prod(nil()) -> s(0())
            sum(cons(z0,z1)) -> +(z0,sum(z1))
            sum(nil()) -> 0()
        - Signature:
            {*/2,*'/2,+/2,+'/2,PROD/1,SUM/1,prod/1,sum/1} / {0/0,c/0,c1/0,c10/2,c2/1,c3/0,c4/0,c5/2,c6/2,c7/0,c8/2,c9/0
            ,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*,*',+,+',PROD,SUM,prod,sum} and constructors {0,c,c1,c10
            ,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            *'(z0,0()) -> c3()
            *'(0(),z0) -> c4()
            *'(s(z0),s(z1)) -> c5(+'(*(z0,z1),+(z0,z1)),*'(z0,z1))
            *'(s(z0),s(z1)) -> c6(+'(*(z0,z1),+(z0,z1)),+'(z0,z1))
            +'(z0,0()) -> c()
            +'(0(),z0) -> c1()
            +'(s(z0),s(z1)) -> c2(+'(z0,z1))
            PROD(cons(z0,z1)) -> c10(*'(z0,prod(z1)),PROD(z1))
            PROD(nil()) -> c9()
            SUM(cons(z0,z1)) -> c8(+'(z0,sum(z1)),SUM(z1))
            SUM(nil()) -> c7()
        - Weak TRS:
            *(z0,0()) -> 0()
            *(0(),z0) -> 0()
            *(s(z0),s(z1)) -> s(+(*(z0,z1),+(z0,z1)))
            +(z0,0()) -> z0
            +(0(),z0) -> z0
            +(s(z0),s(z1)) -> s(s(+(z0,z1)))
            prod(cons(z0,z1)) -> *(z0,prod(z1))
            prod(nil()) -> s(0())
            sum(cons(z0,z1)) -> +(z0,sum(z1))
            sum(nil()) -> 0()
        - Signature:
            {*/2,*'/2,+/2,+'/2,PROD/1,SUM/1,prod/1,sum/1} / {0/0,c/0,c1/0,c10/2,c2/1,c3/0,c4/0,c5/2,c6/2,c7/0,c8/2,c9/0
            ,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*,*',+,+',PROD,SUM,prod,sum} and constructors {0,c,c1,c10
            ,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,s}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          *'(x,y){x -> s(x),y -> s(y)} =
            *'(s(x),s(y)) ->^+ c5(+'(*(x,y),+(x,y)),*'(x,y))
              = C[*'(x,y) = *'(x,y){}]

WORST_CASE(Omega(n^1),?)