* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            assrewrite(exp) -> rewrite(exp)
            first(Op(x,y)) -> x
            first(Val(n)) -> Val(n)
            isOp(Op(x,y)) -> True()
            isOp(Val(n)) -> False()
            rewrite(Op(Op(x,y),y')) -> rewrite[Let](Op(Op(x,y),y'),Op(x,y),rewrite(x))
            rewrite(Op(Val(n),y)) -> Op(rewrite(y),Val(n))
            rewrite(Val(n)) -> Val(n)
            second(Op(x,y)) -> y
        - Weak TRS:
            rewrite[Let](exp,Op(x,y),a1) -> rewrite[Let][Let](exp,Op(x,y),a1,rewrite(y))
            rewrite[Let][Let](Op(x,y),opab,a1,b1) -> rewrite[Let][Let][Let](Op(x,y),a1,b1,rewrite(y))
            rewrite[Let][Let][Let](exp,a1,b1,c1) -> rewrite(Op(a1,Op(b1,rewrite(c1))))
        - Signature:
            {assrewrite/1,first/1,isOp/1,rewrite/1,rewrite[Let]/3,rewrite[Let][Let]/4,rewrite[Let][Let][Let]/4
            ,second/1} / {False/0,Op/2,True/0,Val/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {assrewrite,first,isOp,rewrite,rewrite[Let]
            ,rewrite[Let][Let],rewrite[Let][Let][Let],second} and constructors {False,Op,True,Val}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            assrewrite(exp) -> rewrite(exp)
            first(Op(x,y)) -> x
            first(Val(n)) -> Val(n)
            isOp(Op(x,y)) -> True()
            isOp(Val(n)) -> False()
            rewrite(Op(Op(x,y),y')) -> rewrite[Let](Op(Op(x,y),y'),Op(x,y),rewrite(x))
            rewrite(Op(Val(n),y)) -> Op(rewrite(y),Val(n))
            rewrite(Val(n)) -> Val(n)
            second(Op(x,y)) -> y
        - Weak TRS:
            rewrite[Let](exp,Op(x,y),a1) -> rewrite[Let][Let](exp,Op(x,y),a1,rewrite(y))
            rewrite[Let][Let](Op(x,y),opab,a1,b1) -> rewrite[Let][Let][Let](Op(x,y),a1,b1,rewrite(y))
            rewrite[Let][Let][Let](exp,a1,b1,c1) -> rewrite(Op(a1,Op(b1,rewrite(c1))))
        - Signature:
            {assrewrite/1,first/1,isOp/1,rewrite/1,rewrite[Let]/3,rewrite[Let][Let]/4,rewrite[Let][Let][Let]/4
            ,second/1} / {False/0,Op/2,True/0,Val/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {assrewrite,first,isOp,rewrite,rewrite[Let]
            ,rewrite[Let][Let],rewrite[Let][Let][Let],second} and constructors {False,Op,True,Val}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          rewrite(x){x -> Op(Op(x,y),z)} =
            rewrite(Op(Op(x,y),z)) ->^+ rewrite[Let](Op(Op(x,y),z),Op(x,y),rewrite(x))
              = C[rewrite(x) = rewrite(x){}]

WORST_CASE(Omega(n^1),?)