WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            MAIN(0()) -> c11()
            MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0),unfoldr#2(S(z0)))))
                              ,MAP#2(Cons(S(z0),unfoldr#2(S(z0))))
                              ,UNFOLDR#2(S(z0)))
            MAP#2(Cons(z0,z1)) -> c3(MULT#2(z0,z0))
            MAP#2(Cons(z0,z1)) -> c4(MAP#2(z1))
            MAP#2(Nil()) -> c2()
            MULT#2(0(),z0) -> c7()
            MULT#2(S(z0),z1) -> c8(PLUS#2(z1,mult#2(z0,z1)),MULT#2(z0,z1))
            PLUS#2(0(),z0) -> c9()
            PLUS#2(S(z0),z1) -> c10(PLUS#2(z0,z1))
            SUM#1(Cons(z0,z1)) -> c1(PLUS#2(z0,sum#1(z1)),SUM#1(z1))
            SUM#1(Nil()) -> c()
            UNFOLDR#2(0()) -> c5()
            UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
        - Weak TRS:
            main(0()) -> 0()
            main(S(z0)) -> sum#1(map#2(Cons(S(z0),unfoldr#2(S(z0)))))
            map#2(Cons(z0,z1)) -> Cons(mult#2(z0,z0),map#2(z1))
            map#2(Nil()) -> Nil()
            mult#2(0(),z0) -> 0()
            mult#2(S(z0),z1) -> plus#2(z1,mult#2(z0,z1))
            plus#2(0(),z0) -> z0
            plus#2(S(z0),z1) -> S(plus#2(z0,z1))
            sum#1(Cons(z0,z1)) -> plus#2(z0,sum#1(z1))
            sum#1(Nil()) -> 0()
            unfoldr#2(0()) -> Nil()
            unfoldr#2(S(z0)) -> Cons(z0,unfoldr#2(z0))
        - Signature:
            {MAIN/1,MAP#2/1,MULT#2/2,PLUS#2/2,SUM#1/1,UNFOLDR#2/1,main/1,map#2/1,mult#2/2,plus#2/2,sum#1/1
            ,unfoldr#2/1} / {0/0,Cons/2,Nil/0,S/1,c/0,c1/2,c10/1,c11/0,c12/3,c2/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/2,c9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {MAIN,MAP#2,MULT#2,PLUS#2,SUM#1,UNFOLDR#2,main,map#2
            ,mult#2,plus#2,sum#1,unfoldr#2} and constructors {0,Cons,Nil,S,c,c1,c10,c11,c12,c2,c3,c4,c5,c6,c7,c8,c9}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            MAIN(0()) -> c11()
            MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0),unfoldr#2(S(z0)))))
                              ,MAP#2(Cons(S(z0),unfoldr#2(S(z0))))
                              ,UNFOLDR#2(S(z0)))
            MAP#2(Cons(z0,z1)) -> c3(MULT#2(z0,z0))
            MAP#2(Cons(z0,z1)) -> c4(MAP#2(z1))
            MAP#2(Nil()) -> c2()
            MULT#2(0(),z0) -> c7()
            MULT#2(S(z0),z1) -> c8(PLUS#2(z1,mult#2(z0,z1)),MULT#2(z0,z1))
            PLUS#2(0(),z0) -> c9()
            PLUS#2(S(z0),z1) -> c10(PLUS#2(z0,z1))
            SUM#1(Cons(z0,z1)) -> c1(PLUS#2(z0,sum#1(z1)),SUM#1(z1))
            SUM#1(Nil()) -> c()
            UNFOLDR#2(0()) -> c5()
            UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
        - Weak TRS:
            main(0()) -> 0()
            main(S(z0)) -> sum#1(map#2(Cons(S(z0),unfoldr#2(S(z0)))))
            map#2(Cons(z0,z1)) -> Cons(mult#2(z0,z0),map#2(z1))
            map#2(Nil()) -> Nil()
            mult#2(0(),z0) -> 0()
            mult#2(S(z0),z1) -> plus#2(z1,mult#2(z0,z1))
            plus#2(0(),z0) -> z0
            plus#2(S(z0),z1) -> S(plus#2(z0,z1))
            sum#1(Cons(z0,z1)) -> plus#2(z0,sum#1(z1))
            sum#1(Nil()) -> 0()
            unfoldr#2(0()) -> Nil()
            unfoldr#2(S(z0)) -> Cons(z0,unfoldr#2(z0))
        - Signature:
            {MAIN/1,MAP#2/1,MULT#2/2,PLUS#2/2,SUM#1/1,UNFOLDR#2/1,main/1,map#2/1,mult#2/2,plus#2/2,sum#1/1
            ,unfoldr#2/1} / {0/0,Cons/2,Nil/0,S/1,c/0,c1/2,c10/1,c11/0,c12/3,c2/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/2,c9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {MAIN,MAP#2,MULT#2,PLUS#2,SUM#1,UNFOLDR#2,main,map#2
            ,mult#2,plus#2,sum#1,unfoldr#2} and constructors {0,Cons,Nil,S,c,c1,c10,c11,c12,c2,c3,c4,c5,c6,c7,c8,c9}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            MAIN(0()) -> c11()
            MAIN(S(z0)) -> c12(SUM#1(map#2(Cons(S(z0),unfoldr#2(S(z0)))))
                              ,MAP#2(Cons(S(z0),unfoldr#2(S(z0))))
                              ,UNFOLDR#2(S(z0)))
            MAP#2(Cons(z0,z1)) -> c3(MULT#2(z0,z0))
            MAP#2(Cons(z0,z1)) -> c4(MAP#2(z1))
            MAP#2(Nil()) -> c2()
            MULT#2(0(),z0) -> c7()
            MULT#2(S(z0),z1) -> c8(PLUS#2(z1,mult#2(z0,z1)),MULT#2(z0,z1))
            PLUS#2(0(),z0) -> c9()
            PLUS#2(S(z0),z1) -> c10(PLUS#2(z0,z1))
            SUM#1(Cons(z0,z1)) -> c1(PLUS#2(z0,sum#1(z1)),SUM#1(z1))
            SUM#1(Nil()) -> c()
            UNFOLDR#2(0()) -> c5()
            UNFOLDR#2(S(z0)) -> c6(UNFOLDR#2(z0))
        - Weak TRS:
            main(0()) -> 0()
            main(S(z0)) -> sum#1(map#2(Cons(S(z0),unfoldr#2(S(z0)))))
            map#2(Cons(z0,z1)) -> Cons(mult#2(z0,z0),map#2(z1))
            map#2(Nil()) -> Nil()
            mult#2(0(),z0) -> 0()
            mult#2(S(z0),z1) -> plus#2(z1,mult#2(z0,z1))
            plus#2(0(),z0) -> z0
            plus#2(S(z0),z1) -> S(plus#2(z0,z1))
            sum#1(Cons(z0,z1)) -> plus#2(z0,sum#1(z1))
            sum#1(Nil()) -> 0()
            unfoldr#2(0()) -> Nil()
            unfoldr#2(S(z0)) -> Cons(z0,unfoldr#2(z0))
        - Signature:
            {MAIN/1,MAP#2/1,MULT#2/2,PLUS#2/2,SUM#1/1,UNFOLDR#2/1,main/1,map#2/1,mult#2/2,plus#2/2,sum#1/1
            ,unfoldr#2/1} / {0/0,Cons/2,Nil/0,S/1,c/0,c1/2,c10/1,c11/0,c12/3,c2/0,c3/1,c4/1,c5/0,c6/1,c7/0,c8/2,c9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {MAIN,MAP#2,MULT#2,PLUS#2,SUM#1,UNFOLDR#2,main,map#2
            ,mult#2,plus#2,sum#1,unfoldr#2} and constructors {0,Cons,Nil,S,c,c1,c10,c11,c12,c2,c3,c4,c5,c6,c7,c8,c9}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          MAP#2(y){y -> Cons(x,y)} =
            MAP#2(Cons(x,y)) ->^+ c4(MAP#2(y))
              = C[MAP#2(y) = MAP#2(y){}]

WORST_CASE(Omega(n^1),?)