MAYBE
* Step 1: Failure MAYBE
  + 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:
      NaturalPI {shape = Mixed 3, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing}
  + Details:
      Incompatible
MAYBE