WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            +'(z0,0()) -> c15()
            +'(z0,s(z1)) -> c16(+'(z0,z1))
            F(0()) -> c()
            F(s(0())) -> c1()
            F(s(s(z0))) -> c2(P(h(g(z0))),H(g(z0)),G(z0))
            F(s(s(z0))) -> c3(+'(p(g(z0)),q(g(z0))),P(g(z0)),G(z0))
            F(s(s(z0))) -> c4(+'(p(g(z0)),q(g(z0))),Q(g(z0)),G(z0))
            G(0()) -> c5()
            G(s(z0)) -> c6(H(g(z0)),G(z0))
            G(s(z0)) -> c7(+'(p(g(z0)),q(g(z0))),P(g(z0)),G(z0))
            G(s(z0)) -> c8(+'(p(g(z0)),q(g(z0))),Q(g(z0)),G(z0))
            G(s(z0)) -> c9(P(g(z0)),G(z0))
            H(z0) -> c10(+'(p(z0),q(z0)),P(z0))
            H(z0) -> c11(+'(p(z0),q(z0)),Q(z0))
            H(z0) -> c12(P(z0))
            P(pair(z0,z1)) -> c13()
            Q(pair(z0,z1)) -> c14()
        - Weak TRS:
            +(z0,0()) -> z0
            +(z0,s(z1)) -> s(+(z0,z1))
            f(0()) -> 0()
            f(s(0())) -> s(0())
            f(s(s(z0))) -> +(p(g(z0)),q(g(z0)))
            f(s(s(z0))) -> p(h(g(z0)))
            g(0()) -> pair(s(0()),s(0()))
            g(s(z0)) -> h(g(z0))
            g(s(z0)) -> pair(+(p(g(z0)),q(g(z0))),p(g(z0)))
            h(z0) -> pair(+(p(z0),q(z0)),p(z0))
            p(pair(z0,z1)) -> z0
            q(pair(z0,z1)) -> z1
        - Signature:
            {+/2,+'/2,F/1,G/1,H/1,P/1,Q/1,f/1,g/1,h/1,p/1,q/1} / {0/0,c/0,c1/0,c10/2,c11/2,c12/1,c13/0,c14/0,c15/0,c16/1
            ,c2/3,c3/3,c4/3,c5/0,c6/2,c7/3,c8/3,c9/2,pair/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {+,+',F,G,H,P,Q,f,g,h,p,q} and constructors {0,c,c1,c10
            ,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,pair,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            +'(z0,0()) -> c15()
            +'(z0,s(z1)) -> c16(+'(z0,z1))
            F(0()) -> c()
            F(s(0())) -> c1()
            F(s(s(z0))) -> c2(P(h(g(z0))),H(g(z0)),G(z0))
            F(s(s(z0))) -> c3(+'(p(g(z0)),q(g(z0))),P(g(z0)),G(z0))
            F(s(s(z0))) -> c4(+'(p(g(z0)),q(g(z0))),Q(g(z0)),G(z0))
            G(0()) -> c5()
            G(s(z0)) -> c6(H(g(z0)),G(z0))
            G(s(z0)) -> c7(+'(p(g(z0)),q(g(z0))),P(g(z0)),G(z0))
            G(s(z0)) -> c8(+'(p(g(z0)),q(g(z0))),Q(g(z0)),G(z0))
            G(s(z0)) -> c9(P(g(z0)),G(z0))
            H(z0) -> c10(+'(p(z0),q(z0)),P(z0))
            H(z0) -> c11(+'(p(z0),q(z0)),Q(z0))
            H(z0) -> c12(P(z0))
            P(pair(z0,z1)) -> c13()
            Q(pair(z0,z1)) -> c14()
        - Weak TRS:
            +(z0,0()) -> z0
            +(z0,s(z1)) -> s(+(z0,z1))
            f(0()) -> 0()
            f(s(0())) -> s(0())
            f(s(s(z0))) -> +(p(g(z0)),q(g(z0)))
            f(s(s(z0))) -> p(h(g(z0)))
            g(0()) -> pair(s(0()),s(0()))
            g(s(z0)) -> h(g(z0))
            g(s(z0)) -> pair(+(p(g(z0)),q(g(z0))),p(g(z0)))
            h(z0) -> pair(+(p(z0),q(z0)),p(z0))
            p(pair(z0,z1)) -> z0
            q(pair(z0,z1)) -> z1
        - Signature:
            {+/2,+'/2,F/1,G/1,H/1,P/1,Q/1,f/1,g/1,h/1,p/1,q/1} / {0/0,c/0,c1/0,c10/2,c11/2,c12/1,c13/0,c14/0,c15/0,c16/1
            ,c2/3,c3/3,c4/3,c5/0,c6/2,c7/3,c8/3,c9/2,pair/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {+,+',F,G,H,P,Q,f,g,h,p,q} and constructors {0,c,c1,c10
            ,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,pair,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            +'(z0,0()) -> c15()
            +'(z0,s(z1)) -> c16(+'(z0,z1))
            F(0()) -> c()
            F(s(0())) -> c1()
            F(s(s(z0))) -> c2(P(h(g(z0))),H(g(z0)),G(z0))
            F(s(s(z0))) -> c3(+'(p(g(z0)),q(g(z0))),P(g(z0)),G(z0))
            F(s(s(z0))) -> c4(+'(p(g(z0)),q(g(z0))),Q(g(z0)),G(z0))
            G(0()) -> c5()
            G(s(z0)) -> c6(H(g(z0)),G(z0))
            G(s(z0)) -> c7(+'(p(g(z0)),q(g(z0))),P(g(z0)),G(z0))
            G(s(z0)) -> c8(+'(p(g(z0)),q(g(z0))),Q(g(z0)),G(z0))
            G(s(z0)) -> c9(P(g(z0)),G(z0))
            H(z0) -> c10(+'(p(z0),q(z0)),P(z0))
            H(z0) -> c11(+'(p(z0),q(z0)),Q(z0))
            H(z0) -> c12(P(z0))
            P(pair(z0,z1)) -> c13()
            Q(pair(z0,z1)) -> c14()
        - Weak TRS:
            +(z0,0()) -> z0
            +(z0,s(z1)) -> s(+(z0,z1))
            f(0()) -> 0()
            f(s(0())) -> s(0())
            f(s(s(z0))) -> +(p(g(z0)),q(g(z0)))
            f(s(s(z0))) -> p(h(g(z0)))
            g(0()) -> pair(s(0()),s(0()))
            g(s(z0)) -> h(g(z0))
            g(s(z0)) -> pair(+(p(g(z0)),q(g(z0))),p(g(z0)))
            h(z0) -> pair(+(p(z0),q(z0)),p(z0))
            p(pair(z0,z1)) -> z0
            q(pair(z0,z1)) -> z1
        - Signature:
            {+/2,+'/2,F/1,G/1,H/1,P/1,Q/1,f/1,g/1,h/1,p/1,q/1} / {0/0,c/0,c1/0,c10/2,c11/2,c12/1,c13/0,c14/0,c15/0,c16/1
            ,c2/3,c3/3,c4/3,c5/0,c6/2,c7/3,c8/3,c9/2,pair/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {+,+',F,G,H,P,Q,f,g,h,p,q} and constructors {0,c,c1,c10
            ,c11,c12,c13,c14,c15,c16,c2,c3,c4,c5,c6,c7,c8,c9,pair,s}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          +'(x,y){y -> s(y)} =
            +'(x,s(y)) ->^+ c16(+'(x,y))
              = C[+'(x,y) = +'(x,y){}]

WORST_CASE(Omega(n^1),?)