MAYBE
* Step 1: DependencyPairs 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:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          assrewrite#(exp) -> c_1(rewrite#(exp))
          first#(Op(x,y)) -> c_2()
          first#(Val(n)) -> c_3()
          isOp#(Op(x,y)) -> c_4()
          isOp#(Val(n)) -> c_5()
          rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x))
          rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y))
          rewrite#(Val(n)) -> c_8()
          second#(Op(x,y)) -> c_9()
        Weak DPs
          rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y))
          rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                        ,rewrite#(y))
          rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1))
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            assrewrite#(exp) -> c_1(rewrite#(exp))
            first#(Op(x,y)) -> c_2()
            first#(Val(n)) -> c_3()
            isOp#(Op(x,y)) -> c_4()
            isOp#(Val(n)) -> c_5()
            rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x))
            rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y))
            rewrite#(Val(n)) -> c_8()
            second#(Op(x,y)) -> c_9()
        - Weak DPs:
            rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y))
            rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                          ,rewrite#(y))
            rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1))
        - Weak 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)
            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))))
            second(Op(x,y)) -> y
        - Signature:
            {assrewrite/1,first/1,isOp/1,rewrite/1,rewrite[Let]/3,rewrite[Let][Let]/4,rewrite[Let][Let][Let]/4,second/1
            ,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,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/2,c_7/1,c_8/0,c_9/0,c_10/2,c_11/2
            ,c_12/2}
        - 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:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          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)
          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))))
          assrewrite#(exp) -> c_1(rewrite#(exp))
          first#(Op(x,y)) -> c_2()
          first#(Val(n)) -> c_3()
          isOp#(Op(x,y)) -> c_4()
          isOp#(Val(n)) -> c_5()
          rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x))
          rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y))
          rewrite#(Val(n)) -> c_8()
          rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y))
          rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                        ,rewrite#(y))
          rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1))
          second#(Op(x,y)) -> c_9()
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            assrewrite#(exp) -> c_1(rewrite#(exp))
            first#(Op(x,y)) -> c_2()
            first#(Val(n)) -> c_3()
            isOp#(Op(x,y)) -> c_4()
            isOp#(Val(n)) -> c_5()
            rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x))
            rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y))
            rewrite#(Val(n)) -> c_8()
            second#(Op(x,y)) -> c_9()
        - Weak DPs:
            rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y))
            rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                          ,rewrite#(y))
            rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1))
        - Weak TRS:
            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)
            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
            ,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,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/2,c_7/1,c_8/0,c_9/0,c_10/2,c_11/2
            ,c_12/2}
        - 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:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,3,4,5,9}
        by application of
          Pre({2,3,4,5,9}) = {}.
        Here rules are labelled as follows:
          1: assrewrite#(exp) -> c_1(rewrite#(exp))
          2: first#(Op(x,y)) -> c_2()
          3: first#(Val(n)) -> c_3()
          4: isOp#(Op(x,y)) -> c_4()
          5: isOp#(Val(n)) -> c_5()
          6: rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x))
          7: rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y))
          8: rewrite#(Val(n)) -> c_8()
          9: second#(Op(x,y)) -> c_9()
          10: rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y))
          11: rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                            ,rewrite#(y))
          12: rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            assrewrite#(exp) -> c_1(rewrite#(exp))
            rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x))
            rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y))
            rewrite#(Val(n)) -> c_8()
        - Weak DPs:
            first#(Op(x,y)) -> c_2()
            first#(Val(n)) -> c_3()
            isOp#(Op(x,y)) -> c_4()
            isOp#(Val(n)) -> c_5()
            rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y))
            rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                          ,rewrite#(y))
            rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1))
            second#(Op(x,y)) -> c_9()
        - Weak TRS:
            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)
            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
            ,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,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/2,c_7/1,c_8/0,c_9/0,c_10/2,c_11/2
            ,c_12/2}
        - 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:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:assrewrite#(exp) -> c_1(rewrite#(exp))
             -->_1 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
             -->_1 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
             -->_1 rewrite#(Val(n)) -> c_8():4
          
          2:S:rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x))
             -->_1 rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y)):9
             -->_2 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
             -->_2 rewrite#(Val(n)) -> c_8():4
             -->_2 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
          
          3:S:rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y))
             -->_1 rewrite#(Val(n)) -> c_8():4
             -->_1 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
             -->_1 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
          
          4:S:rewrite#(Val(n)) -> c_8()
             
          
          5:W:first#(Op(x,y)) -> c_2()
             
          
          6:W:first#(Val(n)) -> c_3()
             
          
          7:W:isOp#(Op(x,y)) -> c_4()
             
          
          8:W:isOp#(Val(n)) -> c_5()
             
          
          9:W:rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y))
             -->_1 rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                                 ,rewrite#(y)):10
             -->_2 rewrite#(Val(n)) -> c_8():4
             -->_2 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
             -->_2 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
          
          10:W:rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                             ,rewrite#(y))
             -->_1 rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1)):11
             -->_2 rewrite#(Val(n)) -> c_8():4
             -->_2 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
             -->_2 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
          
          11:W:rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1))
             -->_2 rewrite#(Val(n)) -> c_8():4
             -->_2 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
             -->_1 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
             -->_2 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
             -->_1 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
          
          12:W:second#(Op(x,y)) -> c_9()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          12: second#(Op(x,y)) -> c_9()
          8: isOp#(Val(n)) -> c_5()
          7: isOp#(Op(x,y)) -> c_4()
          6: first#(Val(n)) -> c_3()
          5: first#(Op(x,y)) -> c_2()
* Step 5: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            assrewrite#(exp) -> c_1(rewrite#(exp))
            rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x))
            rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y))
            rewrite#(Val(n)) -> c_8()
        - Weak DPs:
            rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y))
            rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                          ,rewrite#(y))
            rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1))
        - Weak TRS:
            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)
            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
            ,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,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/2,c_7/1,c_8/0,c_9/0,c_10/2,c_11/2
            ,c_12/2}
        - 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:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:assrewrite#(exp) -> c_1(rewrite#(exp))
           -->_1 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
           -->_1 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
           -->_1 rewrite#(Val(n)) -> c_8():4
        
        2:S:rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x))
           -->_1 rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y)):9
           -->_2 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
           -->_2 rewrite#(Val(n)) -> c_8():4
           -->_2 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
        
        3:S:rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y))
           -->_1 rewrite#(Val(n)) -> c_8():4
           -->_1 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
           -->_1 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
        
        4:S:rewrite#(Val(n)) -> c_8()
           
        
        9:W:rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y))
           -->_1 rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                               ,rewrite#(y)):10
           -->_2 rewrite#(Val(n)) -> c_8():4
           -->_2 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
           -->_2 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
        
        10:W:rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                           ,rewrite#(y))
           -->_1 rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1)):11
           -->_2 rewrite#(Val(n)) -> c_8():4
           -->_2 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
           -->_2 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
        
        11:W:rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1))
           -->_2 rewrite#(Val(n)) -> c_8():4
           -->_2 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
           -->_1 rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y)):3
           -->_2 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
           -->_1 rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x)):2
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(1,assrewrite#(exp) -> c_1(rewrite#(exp)))]
* Step 6: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          rewrite#(Op(Op(x,y),y')) -> c_6(rewrite[Let]#(Op(Op(x,y),y'),Op(x,y),rewrite(x)),rewrite#(x))
          rewrite#(Op(Val(n),y)) -> c_7(rewrite#(y))
          rewrite#(Val(n)) -> c_8()
      - Weak DPs:
          rewrite[Let]#(exp,Op(x,y),a1) -> c_10(rewrite[Let][Let]#(exp,Op(x,y),a1,rewrite(y)),rewrite#(y))
          rewrite[Let][Let]#(Op(x,y),opab,a1,b1) -> c_11(rewrite[Let][Let][Let]#(Op(x,y),a1,b1,rewrite(y))
                                                        ,rewrite#(y))
          rewrite[Let][Let][Let]#(exp,a1,b1,c1) -> c_12(rewrite#(Op(a1,Op(b1,rewrite(c1)))),rewrite#(c1))
      - Weak TRS:
          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)
          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
          ,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,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/2,c_7/1,c_8/0,c_9/0,c_10/2,c_11/2
          ,c_12/2}
      - 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:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE