WORST_CASE(Omega(n^1),?)
* Step 1: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            SUB(0(),0()) -> c()
            SUB(0(),s(z0)) -> c2()
            SUB(s(z0),0()) -> c1()
            SUB(s(z0),s(z1)) -> c3(SUB(z0,z1))
            ZERO(cons(z0,z1)) -> c5(ZERO2(sub(z0,z0),cons(z0,z1)),SUB(z0,z0))
            ZERO(nil()) -> c4(ZERO2(0(),nil()))
            ZERO2(0(),cons(z0,z1)) -> c7(SUB(z0,z0))
            ZERO2(0(),cons(z0,z1)) -> c8(ZERO(z1))
            ZERO2(0(),nil()) -> c6()
            ZERO2(s(z0),cons(z1,z2)) -> c10(ZERO(cons(z1,z2)))
            ZERO2(s(z0),nil()) -> c9(ZERO(nil()))
        - Weak TRS:
            sub(0(),0()) -> 0()
            sub(0(),s(z0)) -> 0()
            sub(s(z0),0()) -> s(z0)
            sub(s(z0),s(z1)) -> sub(z0,z1)
            zero(cons(z0,z1)) -> zero2(sub(z0,z0),cons(z0,z1))
            zero(nil()) -> zero2(0(),nil())
            zero2(0(),cons(z0,z1)) -> cons(sub(z0,z0),zero(z1))
            zero2(0(),nil()) -> nil()
            zero2(s(z0),cons(z1,z2)) -> zero(cons(z1,z2))
            zero2(s(z0),nil()) -> zero(nil())
        - Signature:
            {SUB/2,ZERO/1,ZERO2/2,sub/2,zero/1,zero2/2} / {0/0,c/0,c1/0,c10/1,c2/0,c3/1,c4/1,c5/2,c6/0,c7/1,c8/1,c9/1
            ,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SUB,ZERO,ZERO2,sub,zero,zero2} and constructors {0,c,c1
            ,c10,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: Sum.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            SUB(0(),0()) -> c()
            SUB(0(),s(z0)) -> c2()
            SUB(s(z0),0()) -> c1()
            SUB(s(z0),s(z1)) -> c3(SUB(z0,z1))
            ZERO(cons(z0,z1)) -> c5(ZERO2(sub(z0,z0),cons(z0,z1)),SUB(z0,z0))
            ZERO(nil()) -> c4(ZERO2(0(),nil()))
            ZERO2(0(),cons(z0,z1)) -> c7(SUB(z0,z0))
            ZERO2(0(),cons(z0,z1)) -> c8(ZERO(z1))
            ZERO2(0(),nil()) -> c6()
            ZERO2(s(z0),cons(z1,z2)) -> c10(ZERO(cons(z1,z2)))
            ZERO2(s(z0),nil()) -> c9(ZERO(nil()))
        - Weak TRS:
            sub(0(),0()) -> 0()
            sub(0(),s(z0)) -> 0()
            sub(s(z0),0()) -> s(z0)
            sub(s(z0),s(z1)) -> sub(z0,z1)
            zero(cons(z0,z1)) -> zero2(sub(z0,z0),cons(z0,z1))
            zero(nil()) -> zero2(0(),nil())
            zero2(0(),cons(z0,z1)) -> cons(sub(z0,z0),zero(z1))
            zero2(0(),nil()) -> nil()
            zero2(s(z0),cons(z1,z2)) -> zero(cons(z1,z2))
            zero2(s(z0),nil()) -> zero(nil())
        - Signature:
            {SUB/2,ZERO/1,ZERO2/2,sub/2,zero/1,zero2/2} / {0/0,c/0,c1/0,c10/1,c2/0,c3/1,c4/1,c5/2,c6/0,c7/1,c8/1,c9/1
            ,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SUB,ZERO,ZERO2,sub,zero,zero2} and constructors {0,c,c1
            ,c10,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 3: DecreasingLoops.  WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            SUB(0(),0()) -> c()
            SUB(0(),s(z0)) -> c2()
            SUB(s(z0),0()) -> c1()
            SUB(s(z0),s(z1)) -> c3(SUB(z0,z1))
            ZERO(cons(z0,z1)) -> c5(ZERO2(sub(z0,z0),cons(z0,z1)),SUB(z0,z0))
            ZERO(nil()) -> c4(ZERO2(0(),nil()))
            ZERO2(0(),cons(z0,z1)) -> c7(SUB(z0,z0))
            ZERO2(0(),cons(z0,z1)) -> c8(ZERO(z1))
            ZERO2(0(),nil()) -> c6()
            ZERO2(s(z0),cons(z1,z2)) -> c10(ZERO(cons(z1,z2)))
            ZERO2(s(z0),nil()) -> c9(ZERO(nil()))
        - Weak TRS:
            sub(0(),0()) -> 0()
            sub(0(),s(z0)) -> 0()
            sub(s(z0),0()) -> s(z0)
            sub(s(z0),s(z1)) -> sub(z0,z1)
            zero(cons(z0,z1)) -> zero2(sub(z0,z0),cons(z0,z1))
            zero(nil()) -> zero2(0(),nil())
            zero2(0(),cons(z0,z1)) -> cons(sub(z0,z0),zero(z1))
            zero2(0(),nil()) -> nil()
            zero2(s(z0),cons(z1,z2)) -> zero(cons(z1,z2))
            zero2(s(z0),nil()) -> zero(nil())
        - Signature:
            {SUB/2,ZERO/1,ZERO2/2,sub/2,zero/1,zero2/2} / {0/0,c/0,c1/0,c10/1,c2/0,c3/1,c4/1,c5/2,c6/0,c7/1,c8/1,c9/1
            ,cons/2,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SUB,ZERO,ZERO2,sub,zero,zero2} and constructors {0,c,c1
            ,c10,c2,c3,c4,c5,c6,c7,c8,c9,cons,nil,s}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          SUB(x,y){x -> s(x),y -> s(y)} =
            SUB(s(x),s(y)) ->^+ c3(SUB(x,y))
              = C[SUB(x,y) = SUB(x,y){}]

WORST_CASE(Omega(n^1),?)