WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
            times(X,s(Y)) -> plus(X,times(Y,X))
        - Signature:
            {plus/2,times/2} / {s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {plus,times} and constructors {s}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z)),plus#(Y,Z))
          times#(X,s(Y)) -> c_2(plus#(X,times(Y,X)),times#(Y,X))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: DecomposeDG WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z)),plus#(Y,Z))
            times#(X,s(Y)) -> c_2(plus#(X,times(Y,X)),times#(Y,X))
        - Weak TRS:
            plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
            times(X,s(Y)) -> plus(X,times(Y,X))
        - Signature:
            {plus/2,times/2,plus#/2,times#/2} / {s/1,c_1/2,c_2/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {plus#,times#} and constructors {s}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          times#(X,s(Y)) -> c_2(plus#(X,times(Y,X)),times#(Y,X))
        and a lower component
          plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z)),plus#(Y,Z))
        Further, following extension rules are added to the lower component.
          times#(X,s(Y)) -> plus#(X,times(Y,X))
          times#(X,s(Y)) -> times#(Y,X)
** Step 2.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            times#(X,s(Y)) -> c_2(plus#(X,times(Y,X)),times#(Y,X))
        - Weak TRS:
            plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
            times(X,s(Y)) -> plus(X,times(Y,X))
        - Signature:
            {plus/2,times/2,plus#/2,times#/2} / {s/1,c_1/2,c_2/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {plus#,times#} and constructors {s}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:times#(X,s(Y)) -> c_2(plus#(X,times(Y,X)),times#(Y,X))
             -->_2 times#(X,s(Y)) -> c_2(plus#(X,times(Y,X)),times#(Y,X)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          times#(X,s(Y)) -> c_2(times#(Y,X))
** Step 2.a:2: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            times#(X,s(Y)) -> c_2(times#(Y,X))
        - Weak TRS:
            plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
            times(X,s(Y)) -> plus(X,times(Y,X))
        - Signature:
            {plus/2,times/2,plus#/2,times#/2} / {s/1,c_1/2,c_2/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {plus#,times#} and constructors {s}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          times#(X,s(Y)) -> c_2(times#(Y,X))
** Step 2.a:3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            times#(X,s(Y)) -> c_2(times#(Y,X))
        - Signature:
            {plus/2,times/2,plus#/2,times#/2} / {s/1,c_1/2,c_2/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {plus#,times#} and constructors {s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_2) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
              p(plus) = [0]                  
                 p(s) = [1] x1 + [1]         
             p(times) = [0]                  
             p(plus#) = [0]                  
            p(times#) = [1] x1 + [1] x2 + [2]
               p(c_1) = [1] x2 + [0]         
               p(c_2) = [1] x1 + [0]         
          
          Following rules are strictly oriented:
          times#(X,s(Y)) = [1] X + [1] Y + [3]
                         > [1] X + [1] Y + [2]
                         = c_2(times#(Y,X))   
          
          
          Following rules are (at-least) weakly oriented:
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 2.a:4: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            times#(X,s(Y)) -> c_2(times#(Y,X))
        - Signature:
            {plus/2,times/2,plus#/2,times#/2} / {s/1,c_1/2,c_2/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {plus#,times#} and constructors {s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

** Step 2.b:1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z)),plus#(Y,Z))
        - Weak DPs:
            times#(X,s(Y)) -> plus#(X,times(Y,X))
            times#(X,s(Y)) -> times#(Y,X)
        - Weak TRS:
            plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
            times(X,s(Y)) -> plus(X,times(Y,X))
        - Signature:
            {plus/2,times/2,plus#/2,times#/2} / {s/1,c_1/2,c_2/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {plus#,times#} and constructors {s}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_1) = {1,2}
        
        Following symbols are considered usable:
          {plus#,times#}
        TcT has computed the following interpretation:
            p(plus) = [1] x1 + [2] x2 + [8]
               p(s) = [1] x1 + [8]         
           p(times) = [1] x2 + [0]         
           p(plus#) = [1] x1 + [1]         
          p(times#) = [1] x1 + [1] x2 + [8]
             p(c_1) = [1] x1 + [2] x2 + [4]
             p(c_2) = [1] x1 + [1]         
        
        Following rules are strictly oriented:
        plus#(plus(X,Y),Z) = [1] X + [2] Y + [9]               
                           > [1] X + [2] Y + [7]               
                           = c_1(plus#(X,plus(Y,Z)),plus#(Y,Z))
        
        
        Following rules are (at-least) weakly oriented:
        times#(X,s(Y)) =  [1] X + [1] Y + [16]
                       >= [1] X + [1]         
                       =  plus#(X,times(Y,X)) 
        
        times#(X,s(Y)) =  [1] X + [1] Y + [16]
                       >= [1] X + [1] Y + [8] 
                       =  times#(Y,X)         
        
** Step 2.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            plus#(plus(X,Y),Z) -> c_1(plus#(X,plus(Y,Z)),plus#(Y,Z))
            times#(X,s(Y)) -> plus#(X,times(Y,X))
            times#(X,s(Y)) -> times#(Y,X)
        - Weak TRS:
            plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
            times(X,s(Y)) -> plus(X,times(Y,X))
        - Signature:
            {plus/2,times/2,plus#/2,times#/2} / {s/1,c_1/2,c_2/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {plus#,times#} and constructors {s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))