* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            a() -> c()
            a() -> d()
            div(x,y) -> div2(x,y,0())
            div2(x,y,i) -> if1(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i))
            if1(false(),b,x,y,i,j) -> if2(b,x,y,i,j)
            if1(true(),b,x,y,i,j) -> divZeroError()
            if2(false(),x,y,i,j) -> i
            if2(true(),x,y,i,j) -> div2(minus(x,y),y,j)
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            inc(0()) -> 0()
            inc(s(i)) -> s(inc(i))
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            minus(x,0()) -> x
            minus(0(),y) -> 0()
            minus(s(x),s(y)) -> minus(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
        - Signature:
            {a/0,div/2,div2/3,if1/6,if2/5,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3} / {0/0,c/0,d/0,divZeroError/0
            ,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a,div,div2,if1,if2,ifPlus,inc,le,minus,plus
            ,plusIter} and constructors {0,c,d,divZeroError,false,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            a() -> c()
            a() -> d()
            div(x,y) -> div2(x,y,0())
            div2(x,y,i) -> if1(le(y,0()),le(y,x),x,y,plus(i,0()),inc(i))
            if1(false(),b,x,y,i,j) -> if2(b,x,y,i,j)
            if1(true(),b,x,y,i,j) -> divZeroError()
            if2(false(),x,y,i,j) -> i
            if2(true(),x,y,i,j) -> div2(minus(x,y),y,j)
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            inc(0()) -> 0()
            inc(s(i)) -> s(inc(i))
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            minus(x,0()) -> x
            minus(0(),y) -> 0()
            minus(s(x),s(y)) -> minus(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
        - Signature:
            {a/0,div/2,div2/3,if1/6,if2/5,ifPlus/4,inc/1,le/2,minus/2,plus/2,plusIter/3} / {0/0,c/0,d/0,divZeroError/0
            ,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a,div,div2,if1,if2,ifPlus,inc,le,minus,plus
            ,plusIter} and constructors {0,c,d,divZeroError,false,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          inc(x){x -> s(x)} =
            inc(s(x)) ->^+ s(inc(x))
              = C[inc(x) = inc(x){}]

WORST_CASE(Omega(n^1),?)