WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            APP(add(z0,z1),z2) -> c6(APP(z1,z2))
            APP(nil(),z0) -> c5()
            HEAD(add(z0,z1)) -> c4()
            IF(false(),z0,z1,z2) -> c13(SHUFF(reverse(tail(z0)),z2),REVERSE(tail(z0)),TAIL(z0))
            IF(true(),z0,z1,z2) -> c12()
            NULL(add(z0,z1)) -> c1()
            NULL(nil()) -> c()
            REVERSE(add(z0,z1)) -> c8(APP(reverse(z1),add(z0,nil())),REVERSE(z1))
            REVERSE(nil()) -> c7()
            SHUFF(z0,z1) -> c10(IF(null(z0),z0,z1,app(z1,add(head(z0),nil()))),NULL(z0))
            SHUFF(z0,z1) -> c11(IF(null(z0),z0,z1,app(z1,add(head(z0),nil()))),APP(z1,add(head(z0),nil())),HEAD(z0))
            SHUFFLE(z0) -> c9(SHUFF(z0,nil()))
            TAIL(add(z0,z1)) -> c2()
            TAIL(nil()) -> c3()
        - Weak TRS:
            app(add(z0,z1),z2) -> add(z0,app(z1,z2))
            app(nil(),z0) -> z0
            head(add(z0,z1)) -> z0
            if(false(),z0,z1,z2) -> shuff(reverse(tail(z0)),z2)
            if(true(),z0,z1,z2) -> z1
            null(add(z0,z1)) -> false()
            null(nil()) -> true()
            reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil()))
            reverse(nil()) -> nil()
            shuff(z0,z1) -> if(null(z0),z0,z1,app(z1,add(head(z0),nil())))
            shuffle(z0) -> shuff(z0,nil())
            tail(add(z0,z1)) -> z1
            tail(nil()) -> nil()
        - Signature:
            {APP/2,HEAD/1,IF/4,NULL/1,REVERSE/1,SHUFF/2,SHUFFLE/1,TAIL/1,app/2,head/1,if/4,null/1,reverse/1,shuff/2
            ,shuffle/1,tail/1} / {add/2,c/0,c1/0,c10/2,c11/3,c12/0,c13/3,c2/0,c3/0,c4/0,c5/0,c6/1,c7/0,c8/2,c9/1,false/0
            ,nil/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {APP,HEAD,IF,NULL,REVERSE,SHUFF,SHUFFLE,TAIL,app,head,if
            ,null,reverse,shuff,shuffle,tail} and constructors {add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false
            ,nil,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            APP(add(z0,z1),z2) -> c6(APP(z1,z2))
            APP(nil(),z0) -> c5()
            HEAD(add(z0,z1)) -> c4()
            IF(false(),z0,z1,z2) -> c13(SHUFF(reverse(tail(z0)),z2),REVERSE(tail(z0)),TAIL(z0))
            IF(true(),z0,z1,z2) -> c12()
            NULL(add(z0,z1)) -> c1()
            NULL(nil()) -> c()
            REVERSE(add(z0,z1)) -> c8(APP(reverse(z1),add(z0,nil())),REVERSE(z1))
            REVERSE(nil()) -> c7()
            SHUFF(z0,z1) -> c10(IF(null(z0),z0,z1,app(z1,add(head(z0),nil()))),NULL(z0))
            SHUFF(z0,z1) -> c11(IF(null(z0),z0,z1,app(z1,add(head(z0),nil()))),APP(z1,add(head(z0),nil())),HEAD(z0))
            SHUFFLE(z0) -> c9(SHUFF(z0,nil()))
            TAIL(add(z0,z1)) -> c2()
            TAIL(nil()) -> c3()
        - Weak TRS:
            app(add(z0,z1),z2) -> add(z0,app(z1,z2))
            app(nil(),z0) -> z0
            head(add(z0,z1)) -> z0
            if(false(),z0,z1,z2) -> shuff(reverse(tail(z0)),z2)
            if(true(),z0,z1,z2) -> z1
            null(add(z0,z1)) -> false()
            null(nil()) -> true()
            reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil()))
            reverse(nil()) -> nil()
            shuff(z0,z1) -> if(null(z0),z0,z1,app(z1,add(head(z0),nil())))
            shuffle(z0) -> shuff(z0,nil())
            tail(add(z0,z1)) -> z1
            tail(nil()) -> nil()
        - Signature:
            {APP/2,HEAD/1,IF/4,NULL/1,REVERSE/1,SHUFF/2,SHUFFLE/1,TAIL/1,app/2,head/1,if/4,null/1,reverse/1,shuff/2
            ,shuffle/1,tail/1} / {add/2,c/0,c1/0,c10/2,c11/3,c12/0,c13/3,c2/0,c3/0,c4/0,c5/0,c6/1,c7/0,c8/2,c9/1,false/0
            ,nil/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {APP,HEAD,IF,NULL,REVERSE,SHUFF,SHUFFLE,TAIL,app,head,if
            ,null,reverse,shuff,shuffle,tail} and constructors {add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false
            ,nil,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            APP(add(z0,z1),z2) -> c6(APP(z1,z2))
            APP(nil(),z0) -> c5()
            HEAD(add(z0,z1)) -> c4()
            IF(false(),z0,z1,z2) -> c13(SHUFF(reverse(tail(z0)),z2),REVERSE(tail(z0)),TAIL(z0))
            IF(true(),z0,z1,z2) -> c12()
            NULL(add(z0,z1)) -> c1()
            NULL(nil()) -> c()
            REVERSE(add(z0,z1)) -> c8(APP(reverse(z1),add(z0,nil())),REVERSE(z1))
            REVERSE(nil()) -> c7()
            SHUFF(z0,z1) -> c10(IF(null(z0),z0,z1,app(z1,add(head(z0),nil()))),NULL(z0))
            SHUFF(z0,z1) -> c11(IF(null(z0),z0,z1,app(z1,add(head(z0),nil()))),APP(z1,add(head(z0),nil())),HEAD(z0))
            SHUFFLE(z0) -> c9(SHUFF(z0,nil()))
            TAIL(add(z0,z1)) -> c2()
            TAIL(nil()) -> c3()
        - Weak TRS:
            app(add(z0,z1),z2) -> add(z0,app(z1,z2))
            app(nil(),z0) -> z0
            head(add(z0,z1)) -> z0
            if(false(),z0,z1,z2) -> shuff(reverse(tail(z0)),z2)
            if(true(),z0,z1,z2) -> z1
            null(add(z0,z1)) -> false()
            null(nil()) -> true()
            reverse(add(z0,z1)) -> app(reverse(z1),add(z0,nil()))
            reverse(nil()) -> nil()
            shuff(z0,z1) -> if(null(z0),z0,z1,app(z1,add(head(z0),nil())))
            shuffle(z0) -> shuff(z0,nil())
            tail(add(z0,z1)) -> z1
            tail(nil()) -> nil()
        - Signature:
            {APP/2,HEAD/1,IF/4,NULL/1,REVERSE/1,SHUFF/2,SHUFFLE/1,TAIL/1,app/2,head/1,if/4,null/1,reverse/1,shuff/2
            ,shuffle/1,tail/1} / {add/2,c/0,c1/0,c10/2,c11/3,c12/0,c13/3,c2/0,c3/0,c4/0,c5/0,c6/1,c7/0,c8/2,c9/1,false/0
            ,nil/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {APP,HEAD,IF,NULL,REVERSE,SHUFF,SHUFFLE,TAIL,app,head,if
            ,null,reverse,shuff,shuffle,tail} and constructors {add,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9,false
            ,nil,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          APP(y,z){y -> add(x,y)} =
            APP(add(x,y),z) ->^+ c6(APP(y,z))
              = C[APP(y,z) = APP(y,z){}]

WORST_CASE(Omega(n^1),?)