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:
            COND1(true(),z0,z1,z2) -> c(COND2(gr(z0,0()),z0,z1,z2),GR(z0,0()))
            COND2(false(),z0,z1,z2) -> c4(COND3(gr(z1,0()),z0,z1,z2),GR(z1,0()))
            COND2(true(),z0,z1,z2) -> c1(COND1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z0,z2))
            COND2(true(),z0,z1,z2) -> c2(COND1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z1,z2))
            COND2(true(),z0,z1,z2) -> c3(COND1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2),P(z0))
            COND3(false(),z0,z1,z2) -> c8(COND1(or(gr(z0,z2),gr(z1,z2)),z0,z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z0,z2))
            COND3(false(),z0,z1,z2) -> c9(COND1(or(gr(z0,z2),gr(z1,z2)),z0,z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z1,z2))
            COND3(true(),z0,z1,z2) -> c5(COND1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2),OR(gr(z0,z2),gr(z1,z2)),GR(z0,z2))
            COND3(true(),z0,z1,z2) -> c6(COND1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2),OR(gr(z0,z2),gr(z1,z2)),GR(z1,z2))
            COND3(true(),z0,z1,z2) -> c7(COND1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2),P(z1))
            GR(0(),z0) -> c10()
            GR(s(z0),0()) -> c11()
            GR(s(z0),s(z1)) -> c12(GR(z0,z1))
            OR(z0,true()) -> c15()
            OR(false(),false()) -> c13()
            OR(true(),z0) -> c14()
            P(0()) -> c16()
            P(s(z0)) -> c17()
        - Weak TRS:
            cond1(true(),z0,z1,z2) -> cond2(gr(z0,0()),z0,z1,z2)
            cond2(false(),z0,z1,z2) -> cond3(gr(z1,0()),z0,z1,z2)
            cond2(true(),z0,z1,z2) -> cond1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2)
            cond3(false(),z0,z1,z2) -> cond1(or(gr(z0,z2),gr(z1,z2)),z0,z1,z2)
            cond3(true(),z0,z1,z2) -> cond1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2)
            gr(0(),z0) -> false()
            gr(s(z0),0()) -> true()
            gr(s(z0),s(z1)) -> gr(z0,z1)
            or(z0,true()) -> true()
            or(false(),false()) -> false()
            or(true(),z0) -> true()
            p(0()) -> 0()
            p(s(z0)) -> z0
        - Signature:
            {COND1/4,COND2/4,COND3/4,GR/2,OR/2,P/1,cond1/4,cond2/4,cond3/4,gr/2,or/2,p/1} / {0/0,c/2,c1/3,c10/0,c11/0
            ,c12/1,c13/0,c14/0,c15/0,c16/0,c17/0,c2/3,c3/2,c4/2,c5/3,c6/3,c7/2,c8/3,c9/3,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {COND1,COND2,COND3,GR,OR,P,cond1,cond2,cond3,gr,or
            ,p} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            COND1(true(),z0,z1,z2) -> c(COND2(gr(z0,0()),z0,z1,z2),GR(z0,0()))
            COND2(false(),z0,z1,z2) -> c4(COND3(gr(z1,0()),z0,z1,z2),GR(z1,0()))
            COND2(true(),z0,z1,z2) -> c1(COND1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z0,z2))
            COND2(true(),z0,z1,z2) -> c2(COND1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z1,z2))
            COND2(true(),z0,z1,z2) -> c3(COND1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2),P(z0))
            COND3(false(),z0,z1,z2) -> c8(COND1(or(gr(z0,z2),gr(z1,z2)),z0,z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z0,z2))
            COND3(false(),z0,z1,z2) -> c9(COND1(or(gr(z0,z2),gr(z1,z2)),z0,z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z1,z2))
            COND3(true(),z0,z1,z2) -> c5(COND1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2),OR(gr(z0,z2),gr(z1,z2)),GR(z0,z2))
            COND3(true(),z0,z1,z2) -> c6(COND1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2),OR(gr(z0,z2),gr(z1,z2)),GR(z1,z2))
            COND3(true(),z0,z1,z2) -> c7(COND1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2),P(z1))
            GR(0(),z0) -> c10()
            GR(s(z0),0()) -> c11()
            GR(s(z0),s(z1)) -> c12(GR(z0,z1))
            OR(z0,true()) -> c15()
            OR(false(),false()) -> c13()
            OR(true(),z0) -> c14()
            P(0()) -> c16()
            P(s(z0)) -> c17()
        - Weak TRS:
            cond1(true(),z0,z1,z2) -> cond2(gr(z0,0()),z0,z1,z2)
            cond2(false(),z0,z1,z2) -> cond3(gr(z1,0()),z0,z1,z2)
            cond2(true(),z0,z1,z2) -> cond1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2)
            cond3(false(),z0,z1,z2) -> cond1(or(gr(z0,z2),gr(z1,z2)),z0,z1,z2)
            cond3(true(),z0,z1,z2) -> cond1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2)
            gr(0(),z0) -> false()
            gr(s(z0),0()) -> true()
            gr(s(z0),s(z1)) -> gr(z0,z1)
            or(z0,true()) -> true()
            or(false(),false()) -> false()
            or(true(),z0) -> true()
            p(0()) -> 0()
            p(s(z0)) -> z0
        - Signature:
            {COND1/4,COND2/4,COND3/4,GR/2,OR/2,P/1,cond1/4,cond2/4,cond3/4,gr/2,or/2,p/1} / {0/0,c/2,c1/3,c10/0,c11/0
            ,c12/1,c13/0,c14/0,c15/0,c16/0,c17/0,c2/3,c3/2,c4/2,c5/3,c6/3,c7/2,c8/3,c9/3,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {COND1,COND2,COND3,GR,OR,P,cond1,cond2,cond3,gr,or
            ,p} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            COND1(true(),z0,z1,z2) -> c(COND2(gr(z0,0()),z0,z1,z2),GR(z0,0()))
            COND2(false(),z0,z1,z2) -> c4(COND3(gr(z1,0()),z0,z1,z2),GR(z1,0()))
            COND2(true(),z0,z1,z2) -> c1(COND1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z0,z2))
            COND2(true(),z0,z1,z2) -> c2(COND1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z1,z2))
            COND2(true(),z0,z1,z2) -> c3(COND1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2),P(z0))
            COND3(false(),z0,z1,z2) -> c8(COND1(or(gr(z0,z2),gr(z1,z2)),z0,z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z0,z2))
            COND3(false(),z0,z1,z2) -> c9(COND1(or(gr(z0,z2),gr(z1,z2)),z0,z1,z2),OR(gr(z0,z2),gr(z1,z2)),GR(z1,z2))
            COND3(true(),z0,z1,z2) -> c5(COND1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2),OR(gr(z0,z2),gr(z1,z2)),GR(z0,z2))
            COND3(true(),z0,z1,z2) -> c6(COND1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2),OR(gr(z0,z2),gr(z1,z2)),GR(z1,z2))
            COND3(true(),z0,z1,z2) -> c7(COND1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2),P(z1))
            GR(0(),z0) -> c10()
            GR(s(z0),0()) -> c11()
            GR(s(z0),s(z1)) -> c12(GR(z0,z1))
            OR(z0,true()) -> c15()
            OR(false(),false()) -> c13()
            OR(true(),z0) -> c14()
            P(0()) -> c16()
            P(s(z0)) -> c17()
        - Weak TRS:
            cond1(true(),z0,z1,z2) -> cond2(gr(z0,0()),z0,z1,z2)
            cond2(false(),z0,z1,z2) -> cond3(gr(z1,0()),z0,z1,z2)
            cond2(true(),z0,z1,z2) -> cond1(or(gr(z0,z2),gr(z1,z2)),p(z0),z1,z2)
            cond3(false(),z0,z1,z2) -> cond1(or(gr(z0,z2),gr(z1,z2)),z0,z1,z2)
            cond3(true(),z0,z1,z2) -> cond1(or(gr(z0,z2),gr(z1,z2)),z0,p(z1),z2)
            gr(0(),z0) -> false()
            gr(s(z0),0()) -> true()
            gr(s(z0),s(z1)) -> gr(z0,z1)
            or(z0,true()) -> true()
            or(false(),false()) -> false()
            or(true(),z0) -> true()
            p(0()) -> 0()
            p(s(z0)) -> z0
        - Signature:
            {COND1/4,COND2/4,COND3/4,GR/2,OR/2,P/1,cond1/4,cond2/4,cond3/4,gr/2,or/2,p/1} / {0/0,c/2,c1/3,c10/0,c11/0
            ,c12/1,c13/0,c14/0,c15/0,c16/0,c17/0,c2/3,c3/2,c4/2,c5/3,c6/3,c7/2,c8/3,c9/3,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {COND1,COND2,COND3,GR,OR,P,cond1,cond2,cond3,gr,or
            ,p} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          GR(x,y){x -> s(x),y -> s(y)} =
            GR(s(x),s(y)) ->^+ c12(GR(x,y))
              = C[GR(x,y) = GR(x,y){}]

WORST_CASE(Omega(n^1),?)