WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            @'(Cons(z0,z1),z2) -> c(@'(z1,z2))
            @'(Nil(),z0) -> c1()
            BINOM(Cons(z0,z1),Cons(z2,z3)) -> c2(@'(binom(z1,z3),binom(z1,Cons(z2,z3))),BINOM(z1,z3))
            BINOM(Cons(z0,z1),Cons(z2,z3)) -> c3(@'(binom(z1,z3),binom(z1,Cons(z2,z3))),BINOM(z1,Cons(z2,z3)))
            BINOM(Cons(z0,z1),Nil()) -> c4()
            BINOM(Nil(),z0) -> c5()
            GOAL(z0,z1) -> c6(BINOM(z0,z1))
        - Weak TRS:
            @(Cons(z0,z1),z2) -> Cons(z0,@(z1,z2))
            @(Nil(),z0) -> z0
            binom(Cons(z0,z1),Cons(z2,z3)) -> @(binom(z1,z3),binom(z1,Cons(z2,z3)))
            binom(Cons(z0,z1),Nil()) -> Cons(Nil(),Nil())
            binom(Nil(),z0) -> Cons(Nil(),Nil())
            goal(z0,z1) -> binom(z0,z1)
        - Signature:
            {@/2,@'/2,BINOM/2,GOAL/2,binom/2,goal/2} / {Cons/2,Nil/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/0,c6/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@,@',BINOM,GOAL,binom,goal} and constructors {Cons,Nil,c
            ,c1,c2,c3,c4,c5,c6}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            @'(Cons(z0,z1),z2) -> c(@'(z1,z2))
            @'(Nil(),z0) -> c1()
            BINOM(Cons(z0,z1),Cons(z2,z3)) -> c2(@'(binom(z1,z3),binom(z1,Cons(z2,z3))),BINOM(z1,z3))
            BINOM(Cons(z0,z1),Cons(z2,z3)) -> c3(@'(binom(z1,z3),binom(z1,Cons(z2,z3))),BINOM(z1,Cons(z2,z3)))
            BINOM(Cons(z0,z1),Nil()) -> c4()
            BINOM(Nil(),z0) -> c5()
            GOAL(z0,z1) -> c6(BINOM(z0,z1))
        - Weak TRS:
            @(Cons(z0,z1),z2) -> Cons(z0,@(z1,z2))
            @(Nil(),z0) -> z0
            binom(Cons(z0,z1),Cons(z2,z3)) -> @(binom(z1,z3),binom(z1,Cons(z2,z3)))
            binom(Cons(z0,z1),Nil()) -> Cons(Nil(),Nil())
            binom(Nil(),z0) -> Cons(Nil(),Nil())
            goal(z0,z1) -> binom(z0,z1)
        - Signature:
            {@/2,@'/2,BINOM/2,GOAL/2,binom/2,goal/2} / {Cons/2,Nil/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/0,c6/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@,@',BINOM,GOAL,binom,goal} and constructors {Cons,Nil,c
            ,c1,c2,c3,c4,c5,c6}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            @'(Cons(z0,z1),z2) -> c(@'(z1,z2))
            @'(Nil(),z0) -> c1()
            BINOM(Cons(z0,z1),Cons(z2,z3)) -> c2(@'(binom(z1,z3),binom(z1,Cons(z2,z3))),BINOM(z1,z3))
            BINOM(Cons(z0,z1),Cons(z2,z3)) -> c3(@'(binom(z1,z3),binom(z1,Cons(z2,z3))),BINOM(z1,Cons(z2,z3)))
            BINOM(Cons(z0,z1),Nil()) -> c4()
            BINOM(Nil(),z0) -> c5()
            GOAL(z0,z1) -> c6(BINOM(z0,z1))
        - Weak TRS:
            @(Cons(z0,z1),z2) -> Cons(z0,@(z1,z2))
            @(Nil(),z0) -> z0
            binom(Cons(z0,z1),Cons(z2,z3)) -> @(binom(z1,z3),binom(z1,Cons(z2,z3)))
            binom(Cons(z0,z1),Nil()) -> Cons(Nil(),Nil())
            binom(Nil(),z0) -> Cons(Nil(),Nil())
            goal(z0,z1) -> binom(z0,z1)
        - Signature:
            {@/2,@'/2,BINOM/2,GOAL/2,binom/2,goal/2} / {Cons/2,Nil/0,c/1,c1/0,c2/2,c3/2,c4/0,c5/0,c6/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {@,@',BINOM,GOAL,binom,goal} and constructors {Cons,Nil,c
            ,c1,c2,c3,c4,c5,c6}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          @'(y,z){y -> Cons(x,y)} =
            @'(Cons(x,y),z) ->^+ c(@'(y,z))
              = C[@'(y,z) = @'(y,z){}]

WORST_CASE(Omega(n^1),?)