* Step 1: Sum WORST_CASE(?,O(n^1))
    + 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:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: MI WORST_CASE(?,O(n^1))
    + 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:
        MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 1, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
        
        The following argument positions are considered usable:
          uargs(plus) = {2}
        
        Following symbols are considered usable:
          {plus,times}
        TcT has computed the following interpretation:
           p(plus) = [1] x_2 + [0]          
              p(s) = [1] x_1 + [4]          
          p(times) = [1] x_1 + [1] x_2 + [0]
        
        Following rules are strictly oriented:
        times(X,s(Y)) = [1] X + [1] Y + [4]
                      > [1] X + [1] Y + [0]
                      = plus(X,times(Y,X)) 
        
        
        Following rules are (at-least) weakly oriented:
        plus(plus(X,Y),Z) =  [1] Z + [0]      
                          >= [1] Z + [0]      
                          =  plus(X,plus(Y,Z))
        
* Step 3: MI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
        - Weak TRS:
            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:
        MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity (Just 1))), miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity (Just 1))):
        
        The following argument positions are considered usable:
          uargs(plus) = {2}
        
        Following symbols are considered usable:
          {plus,times}
        TcT has computed the following interpretation:
           p(plus) = [0 6] x_1 + [1 0] x_2 + [2]  
                     [0 1]       [0 1]       [2]  
              p(s) = [1 2] x_1 + [2]              
                     [0 0]       [1]              
          p(times) = [14 9] x_1 + [14 2] x_2 + [0]
                     [ 4 1]       [ 4 0]       [9]
        
        Following rules are strictly oriented:
        plus(plus(X,Y),Z) = [0 6] X + [0 6] Y + [1 0] Z + [14]
                            [0 1]     [0 1]     [0 1]     [4] 
                          > [0 6] X + [0 6] Y + [1 0] Z + [4] 
                            [0 1]     [0 1]     [0 1]     [4] 
                          = plus(X,plus(Y,Z))                 
        
        
        Following rules are (at-least) weakly oriented:
        times(X,s(Y)) =  [14 9] X + [14 28] Y + [30]
                         [ 4 1]     [ 4  8]     [17]
                      >= [14 8] X + [14 9] Y + [2]  
                         [ 4 1]     [ 4 1]     [11] 
                      =  plus(X,times(Y,X))         
        
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - 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} / {s/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).

WORST_CASE(?,O(n^1))