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:
            GOAL(z0) -> c9(PERMUTE(z0))
            MAPCONSAPP(z0,Cons(z1,z2),z3) -> c7(MAPCONSAPP(z0,z2,z3))
            MAPCONSAPP(z0,Nil(),z1) -> c8()
            PERMUTE(Cons(z0,z1)) -> c5(SELECT(z0,Nil(),z1))
            PERMUTE(Nil()) -> c6()
            REVAPP(Cons(z0,z1),z2) -> c3(REVAPP(z1,Cons(z0,z2)))
            REVAPP(Nil(),z0) -> c4()
            SELECT(z0,z1,Cons(z2,z3)) -> c(MAPCONSAPP(z0,permute(revapp(z1,Cons(z2,z3))),select(z2,Cons(z0,z1),z3))
                                          ,PERMUTE(revapp(z1,Cons(z2,z3)))
                                          ,REVAPP(z1,Cons(z2,z3)))
            SELECT(z0,z1,Cons(z2,z3)) -> c1(MAPCONSAPP(z0,permute(revapp(z1,Cons(z2,z3))),select(z2,Cons(z0,z1),z3))
                                           ,SELECT(z2,Cons(z0,z1),z3))
            SELECT(z0,z1,Nil()) -> c2(MAPCONSAPP(z0,permute(revapp(z1,Nil())),Nil())
                                     ,PERMUTE(revapp(z1,Nil()))
                                     ,REVAPP(z1,Nil()))
        - Weak TRS:
            goal(z0) -> permute(z0)
            mapconsapp(z0,Cons(z1,z2),z3) -> Cons(Cons(z0,z1),mapconsapp(z0,z2,z3))
            mapconsapp(z0,Nil(),z1) -> z1
            permute(Cons(z0,z1)) -> select(z0,Nil(),z1)
            permute(Nil()) -> Cons(Nil(),Nil())
            revapp(Cons(z0,z1),z2) -> revapp(z1,Cons(z0,z2))
            revapp(Nil(),z0) -> z0
            select(z0,z1,Cons(z2,z3)) -> mapconsapp(z0,permute(revapp(z1,Cons(z2,z3))),select(z2,Cons(z0,z1),z3))
            select(z0,z1,Nil()) -> mapconsapp(z0,permute(revapp(z1,Nil())),Nil())
        - Signature:
            {GOAL/1,MAPCONSAPP/3,PERMUTE/1,REVAPP/2,SELECT/3,goal/1,mapconsapp/3,permute/1,revapp/2,select/3} / {Cons/2
            ,Nil/0,c/3,c1/2,c2/3,c3/1,c4/0,c5/1,c6/0,c7/1,c8/0,c9/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {GOAL,MAPCONSAPP,PERMUTE,REVAPP,SELECT,goal,mapconsapp
            ,permute,revapp,select} and constructors {Cons,Nil,c,c1,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:
            GOAL(z0) -> c9(PERMUTE(z0))
            MAPCONSAPP(z0,Cons(z1,z2),z3) -> c7(MAPCONSAPP(z0,z2,z3))
            MAPCONSAPP(z0,Nil(),z1) -> c8()
            PERMUTE(Cons(z0,z1)) -> c5(SELECT(z0,Nil(),z1))
            PERMUTE(Nil()) -> c6()
            REVAPP(Cons(z0,z1),z2) -> c3(REVAPP(z1,Cons(z0,z2)))
            REVAPP(Nil(),z0) -> c4()
            SELECT(z0,z1,Cons(z2,z3)) -> c(MAPCONSAPP(z0,permute(revapp(z1,Cons(z2,z3))),select(z2,Cons(z0,z1),z3))
                                          ,PERMUTE(revapp(z1,Cons(z2,z3)))
                                          ,REVAPP(z1,Cons(z2,z3)))
            SELECT(z0,z1,Cons(z2,z3)) -> c1(MAPCONSAPP(z0,permute(revapp(z1,Cons(z2,z3))),select(z2,Cons(z0,z1),z3))
                                           ,SELECT(z2,Cons(z0,z1),z3))
            SELECT(z0,z1,Nil()) -> c2(MAPCONSAPP(z0,permute(revapp(z1,Nil())),Nil())
                                     ,PERMUTE(revapp(z1,Nil()))
                                     ,REVAPP(z1,Nil()))
        - Weak TRS:
            goal(z0) -> permute(z0)
            mapconsapp(z0,Cons(z1,z2),z3) -> Cons(Cons(z0,z1),mapconsapp(z0,z2,z3))
            mapconsapp(z0,Nil(),z1) -> z1
            permute(Cons(z0,z1)) -> select(z0,Nil(),z1)
            permute(Nil()) -> Cons(Nil(),Nil())
            revapp(Cons(z0,z1),z2) -> revapp(z1,Cons(z0,z2))
            revapp(Nil(),z0) -> z0
            select(z0,z1,Cons(z2,z3)) -> mapconsapp(z0,permute(revapp(z1,Cons(z2,z3))),select(z2,Cons(z0,z1),z3))
            select(z0,z1,Nil()) -> mapconsapp(z0,permute(revapp(z1,Nil())),Nil())
        - Signature:
            {GOAL/1,MAPCONSAPP/3,PERMUTE/1,REVAPP/2,SELECT/3,goal/1,mapconsapp/3,permute/1,revapp/2,select/3} / {Cons/2
            ,Nil/0,c/3,c1/2,c2/3,c3/1,c4/0,c5/1,c6/0,c7/1,c8/0,c9/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {GOAL,MAPCONSAPP,PERMUTE,REVAPP,SELECT,goal,mapconsapp
            ,permute,revapp,select} and constructors {Cons,Nil,c,c1,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:
            GOAL(z0) -> c9(PERMUTE(z0))
            MAPCONSAPP(z0,Cons(z1,z2),z3) -> c7(MAPCONSAPP(z0,z2,z3))
            MAPCONSAPP(z0,Nil(),z1) -> c8()
            PERMUTE(Cons(z0,z1)) -> c5(SELECT(z0,Nil(),z1))
            PERMUTE(Nil()) -> c6()
            REVAPP(Cons(z0,z1),z2) -> c3(REVAPP(z1,Cons(z0,z2)))
            REVAPP(Nil(),z0) -> c4()
            SELECT(z0,z1,Cons(z2,z3)) -> c(MAPCONSAPP(z0,permute(revapp(z1,Cons(z2,z3))),select(z2,Cons(z0,z1),z3))
                                          ,PERMUTE(revapp(z1,Cons(z2,z3)))
                                          ,REVAPP(z1,Cons(z2,z3)))
            SELECT(z0,z1,Cons(z2,z3)) -> c1(MAPCONSAPP(z0,permute(revapp(z1,Cons(z2,z3))),select(z2,Cons(z0,z1),z3))
                                           ,SELECT(z2,Cons(z0,z1),z3))
            SELECT(z0,z1,Nil()) -> c2(MAPCONSAPP(z0,permute(revapp(z1,Nil())),Nil())
                                     ,PERMUTE(revapp(z1,Nil()))
                                     ,REVAPP(z1,Nil()))
        - Weak TRS:
            goal(z0) -> permute(z0)
            mapconsapp(z0,Cons(z1,z2),z3) -> Cons(Cons(z0,z1),mapconsapp(z0,z2,z3))
            mapconsapp(z0,Nil(),z1) -> z1
            permute(Cons(z0,z1)) -> select(z0,Nil(),z1)
            permute(Nil()) -> Cons(Nil(),Nil())
            revapp(Cons(z0,z1),z2) -> revapp(z1,Cons(z0,z2))
            revapp(Nil(),z0) -> z0
            select(z0,z1,Cons(z2,z3)) -> mapconsapp(z0,permute(revapp(z1,Cons(z2,z3))),select(z2,Cons(z0,z1),z3))
            select(z0,z1,Nil()) -> mapconsapp(z0,permute(revapp(z1,Nil())),Nil())
        - Signature:
            {GOAL/1,MAPCONSAPP/3,PERMUTE/1,REVAPP/2,SELECT/3,goal/1,mapconsapp/3,permute/1,revapp/2,select/3} / {Cons/2
            ,Nil/0,c/3,c1/2,c2/3,c3/1,c4/0,c5/1,c6/0,c7/1,c8/0,c9/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {GOAL,MAPCONSAPP,PERMUTE,REVAPP,SELECT,goal,mapconsapp
            ,permute,revapp,select} and constructors {Cons,Nil,c,c1,c2,c3,c4,c5,c6,c7,c8,c9}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          MAPCONSAPP(x,z,u){z -> Cons(y,z)} =
            MAPCONSAPP(x,Cons(y,z),u) ->^+ c7(MAPCONSAPP(x,z,u))
              = C[MAPCONSAPP(x,z,u) = MAPCONSAPP(x,z,u){}]

WORST_CASE(Omega(n^1),?)