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:
            AVERAGE(z0,z1) -> c5(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z0,0()))
            AVERAGE(z0,z1) -> c6(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z1,0()))
            AVERAGE(z0,z1) -> c7(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z1,s(0())))
            AVERAGE(z0,z1) -> c8(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z1,s(s(0()))))
            IF(false(),z0,z1,z2,z3,z4) -> c10(AVERAGE(p(z3),s(z4)),P(z3))
            IF(true(),z0,z1,z2,z3,z4) -> c9(IF2(z0,z1,z2,z3,z4))
            IF2(false(),z0,z1,z2,z3) -> c12(IF3(z0,z1,z2,z3))
            IF2(true(),z0,z1,z2,z3) -> c11()
            IF3(false(),z0,z1,z2) -> c14(IF4(z0,z1,z2))
            IF3(true(),z0,z1,z2) -> c13()
            IF4(false(),z0,z1) -> c16(AVERAGE(s(z0),p(p(z1))),P(p(z1)),P(z1))
            IF4(true(),z0,z1) -> c15()
            LE(0(),z0) -> c2()
            LE(s(z0),0()) -> c3()
            LE(s(z0),s(z1)) -> c4(LE(z0,z1))
            P(0()) -> c1()
            P(s(z0)) -> c()
        - Weak TRS:
            average(z0,z1) -> if(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1)
            if(false(),z0,z1,z2,z3,z4) -> average(p(z3),s(z4))
            if(true(),z0,z1,z2,z3,z4) -> if2(z0,z1,z2,z3,z4)
            if2(false(),z0,z1,z2,z3) -> if3(z0,z1,z2,z3)
            if2(true(),z0,z1,z2,z3) -> 0()
            if3(false(),z0,z1,z2) -> if4(z0,z1,z2)
            if3(true(),z0,z1,z2) -> 0()
            if4(false(),z0,z1) -> average(s(z0),p(p(z1)))
            if4(true(),z0,z1) -> s(0())
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            p(0()) -> 0()
            p(s(z0)) -> z0
        - Signature:
            {AVERAGE/2,IF/6,IF2/5,IF3/4,IF4/3,LE/2,P/1,average/2,if/6,if2/5,if3/4,if4/3,le/2,p/1} / {0/0,c/0,c1/0,c10/2
            ,c11/0,c12/1,c13/0,c14/1,c15/0,c16/3,c2/0,c3/0,c4/1,c5/2,c6/2,c7/2,c8/2,c9/1,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {AVERAGE,IF,IF2,IF3,IF4,LE,P,average,if,if2,if3,if4,le
            ,p} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,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:
            AVERAGE(z0,z1) -> c5(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z0,0()))
            AVERAGE(z0,z1) -> c6(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z1,0()))
            AVERAGE(z0,z1) -> c7(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z1,s(0())))
            AVERAGE(z0,z1) -> c8(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z1,s(s(0()))))
            IF(false(),z0,z1,z2,z3,z4) -> c10(AVERAGE(p(z3),s(z4)),P(z3))
            IF(true(),z0,z1,z2,z3,z4) -> c9(IF2(z0,z1,z2,z3,z4))
            IF2(false(),z0,z1,z2,z3) -> c12(IF3(z0,z1,z2,z3))
            IF2(true(),z0,z1,z2,z3) -> c11()
            IF3(false(),z0,z1,z2) -> c14(IF4(z0,z1,z2))
            IF3(true(),z0,z1,z2) -> c13()
            IF4(false(),z0,z1) -> c16(AVERAGE(s(z0),p(p(z1))),P(p(z1)),P(z1))
            IF4(true(),z0,z1) -> c15()
            LE(0(),z0) -> c2()
            LE(s(z0),0()) -> c3()
            LE(s(z0),s(z1)) -> c4(LE(z0,z1))
            P(0()) -> c1()
            P(s(z0)) -> c()
        - Weak TRS:
            average(z0,z1) -> if(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1)
            if(false(),z0,z1,z2,z3,z4) -> average(p(z3),s(z4))
            if(true(),z0,z1,z2,z3,z4) -> if2(z0,z1,z2,z3,z4)
            if2(false(),z0,z1,z2,z3) -> if3(z0,z1,z2,z3)
            if2(true(),z0,z1,z2,z3) -> 0()
            if3(false(),z0,z1,z2) -> if4(z0,z1,z2)
            if3(true(),z0,z1,z2) -> 0()
            if4(false(),z0,z1) -> average(s(z0),p(p(z1)))
            if4(true(),z0,z1) -> s(0())
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            p(0()) -> 0()
            p(s(z0)) -> z0
        - Signature:
            {AVERAGE/2,IF/6,IF2/5,IF3/4,IF4/3,LE/2,P/1,average/2,if/6,if2/5,if3/4,if4/3,le/2,p/1} / {0/0,c/0,c1/0,c10/2
            ,c11/0,c12/1,c13/0,c14/1,c15/0,c16/3,c2/0,c3/0,c4/1,c5/2,c6/2,c7/2,c8/2,c9/1,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {AVERAGE,IF,IF2,IF3,IF4,LE,P,average,if,if2,if3,if4,le
            ,p} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,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:
            AVERAGE(z0,z1) -> c5(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z0,0()))
            AVERAGE(z0,z1) -> c6(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z1,0()))
            AVERAGE(z0,z1) -> c7(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z1,s(0())))
            AVERAGE(z0,z1) -> c8(IF(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1),LE(z1,s(s(0()))))
            IF(false(),z0,z1,z2,z3,z4) -> c10(AVERAGE(p(z3),s(z4)),P(z3))
            IF(true(),z0,z1,z2,z3,z4) -> c9(IF2(z0,z1,z2,z3,z4))
            IF2(false(),z0,z1,z2,z3) -> c12(IF3(z0,z1,z2,z3))
            IF2(true(),z0,z1,z2,z3) -> c11()
            IF3(false(),z0,z1,z2) -> c14(IF4(z0,z1,z2))
            IF3(true(),z0,z1,z2) -> c13()
            IF4(false(),z0,z1) -> c16(AVERAGE(s(z0),p(p(z1))),P(p(z1)),P(z1))
            IF4(true(),z0,z1) -> c15()
            LE(0(),z0) -> c2()
            LE(s(z0),0()) -> c3()
            LE(s(z0),s(z1)) -> c4(LE(z0,z1))
            P(0()) -> c1()
            P(s(z0)) -> c()
        - Weak TRS:
            average(z0,z1) -> if(le(z0,0()),le(z1,0()),le(z1,s(0())),le(z1,s(s(0()))),z0,z1)
            if(false(),z0,z1,z2,z3,z4) -> average(p(z3),s(z4))
            if(true(),z0,z1,z2,z3,z4) -> if2(z0,z1,z2,z3,z4)
            if2(false(),z0,z1,z2,z3) -> if3(z0,z1,z2,z3)
            if2(true(),z0,z1,z2,z3) -> 0()
            if3(false(),z0,z1,z2) -> if4(z0,z1,z2)
            if3(true(),z0,z1,z2) -> 0()
            if4(false(),z0,z1) -> average(s(z0),p(p(z1)))
            if4(true(),z0,z1) -> s(0())
            le(0(),z0) -> true()
            le(s(z0),0()) -> false()
            le(s(z0),s(z1)) -> le(z0,z1)
            p(0()) -> 0()
            p(s(z0)) -> z0
        - Signature:
            {AVERAGE/2,IF/6,IF2/5,IF3/4,IF4/3,LE/2,P/1,average/2,if/6,if2/5,if3/4,if4/3,le/2,p/1} / {0/0,c/0,c1/0,c10/2
            ,c11/0,c12/1,c13/0,c14/1,c15/0,c16/3,c2/0,c3/0,c4/1,c5/2,c6/2,c7/2,c8/2,c9/1,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {AVERAGE,IF,IF2,IF3,IF4,LE,P,average,if,if2,if3,if4,le
            ,p} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16,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:
          LE(x,y){x -> s(x),y -> s(y)} =
            LE(s(x),s(y)) ->^+ c4(LE(x,y))
              = C[LE(x,y) = LE(x,y){}]

WORST_CASE(Omega(n^1),?)