* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x,y,s(z)) -> s(f(0(),1(),z))
            f(0(),1(),x) -> f(s(x),x,x)
        - Signature:
            {f/3} / {0/0,1/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f} and constructors {0,1,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            f(x,y,s(z)) -> s(f(0(),1(),z))
            f(0(),1(),x) -> f(s(x),x,x)
        - Signature:
            {f/3} / {0/0,1/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f} and constructors {0,1,s}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          f(x,y,z){z -> s(z)} =
            f(x,y,s(z)) ->^+ s(f(0(),1(),z))
              = C[f(0(),1(),z) = f(x,y,z){x -> 0(),y -> 1()}]

** Step 1.b:1: MI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x,y,s(z)) -> s(f(0(),1(),z))
            f(0(),1(),x) -> f(s(x),x,x)
        - Signature:
            {f/3} / {0/0,1/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f} and constructors {0,1,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(s) = {1}
        
        Following symbols are considered usable:
          {f}
        TcT has computed the following interpretation:
          p(0) = [4]          
          p(1) = [0]          
          p(f) = [2] x_3 + [7]
          p(s) = [1] x_1 + [2]
        
        Following rules are strictly oriented:
        f(x,y,s(z)) = [2] z + [11]   
                    > [2] z + [9]    
                    = s(f(0(),1(),z))
        
        
        Following rules are (at-least) weakly oriented:
        f(0(),1(),x) =  [2] x + [7]
                     >= [2] x + [7]
                     =  f(s(x),x,x)
        
** Step 1.b:2: MI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(0(),1(),x) -> f(s(x),x,x)
        - Weak TRS:
            f(x,y,s(z)) -> s(f(0(),1(),z))
        - Signature:
            {f/3} / {0/0,1/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f} and constructors {0,1,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(s) = {1}
        
        Following symbols are considered usable:
          {f}
        TcT has computed the following interpretation:
          p(0) = [0]                        
                 [1]                        
          p(1) = [1]                        
                 [1]                        
          p(f) = [0 8] x_1 + [3 0] x_3 + [1]
                 [0 0]       [0 1]       [0]
          p(s) = [1 8] x_1 + [4]            
                 [0 0]       [0]            
        
        Following rules are strictly oriented:
        f(0(),1(),x) = [3 0] x + [9]
                       [0 1]     [0]
                     > [3 0] x + [1]
                       [0 1]     [0]
                     = f(s(x),x,x)  
        
        
        Following rules are (at-least) weakly oriented:
        f(x,y,s(z)) =  [0 8] x + [3 24] z + [13]
                       [0 0]     [0  0]     [0] 
                    >= [3 8] z + [13]           
                       [0 0]     [0]            
                    =  s(f(0(),1(),z))          
        
** Step 1.b:3: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            f(x,y,s(z)) -> s(f(0(),1(),z))
            f(0(),1(),x) -> f(s(x),x,x)
        - Signature:
            {f/3} / {0/0,1/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f} and constructors {0,1,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(Omega(n^1),O(n^1))