* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            eq(x,x) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(x)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            f() -> g()
            f() -> h()
            ifPlus(false(),x,y,z) -> plus(x,z)
            ifPlus(true(),x,y,z) -> y
            ifTimes(false(),x,y,z,u) -> timesIter(x,y,u)
            ifTimes(true(),x,y,z,u) -> z
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            minus(x,x) -> 0()
            minus(x,0()) -> x
            minus(0(),x) -> 0()
            minus(s(x),s(y)) -> minus(x,y)
            plus(x,y) -> ifPlus(eq(x,0()),minus(x,s(0())),x,inc(x))
            times(x,y) -> timesIter(x,y,0())
            timesIter(x,y,z) -> ifTimes(eq(x,0()),minus(x,s(0())),y,z,plus(y,z))
        - Signature:
            {eq/2,f/0,ifPlus/4,ifTimes/5,inc/1,minus/2,plus/2,times/2,timesIter/3} / {0/0,false/0,g/0,h/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,f,ifPlus,ifTimes,inc,minus,plus,times
            ,timesIter} and constructors {0,false,g,h,s,true}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            eq(x,x) -> true()
            eq(0(),0()) -> true()
            eq(0(),s(x)) -> false()
            eq(s(x),0()) -> false()
            eq(s(x),s(y)) -> eq(x,y)
            f() -> g()
            f() -> h()
            ifPlus(false(),x,y,z) -> plus(x,z)
            ifPlus(true(),x,y,z) -> y
            ifTimes(false(),x,y,z,u) -> timesIter(x,y,u)
            ifTimes(true(),x,y,z,u) -> z
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            minus(x,x) -> 0()
            minus(x,0()) -> x
            minus(0(),x) -> 0()
            minus(s(x),s(y)) -> minus(x,y)
            plus(x,y) -> ifPlus(eq(x,0()),minus(x,s(0())),x,inc(x))
            times(x,y) -> timesIter(x,y,0())
            timesIter(x,y,z) -> ifTimes(eq(x,0()),minus(x,s(0())),y,z,plus(y,z))
        - Signature:
            {eq/2,f/0,ifPlus/4,ifTimes/5,inc/1,minus/2,plus/2,times/2,timesIter/3} / {0/0,false/0,g/0,h/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,f,ifPlus,ifTimes,inc,minus,plus,times
            ,timesIter} and constructors {0,false,g,h,s,true}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          eq(x,y){x -> s(x),y -> s(y)} =
            eq(s(x),s(y)) ->^+ eq(x,y)
              = C[eq(x,y) = eq(x,y){}]

WORST_CASE(Omega(n^1),?)