WORST_CASE(Omega(n^1),O(n^1))
* 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)
            g(x,y) -> x
            g(x,y) -> y
        - Signature:
            {f/3,g/2} / {0/0,1/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g} 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)
            g(x,y) -> x
            g(x,y) -> y
        - Signature:
            {f/3,g/2} / {0/0,1/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g} 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: NaturalMI 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)
            g(x,y) -> x
            g(x,y) -> y
        - Signature:
            {f/3,g/2} / {0/0,1/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g} and constructors {0,1,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(s) = {1}
        
        Following symbols are considered usable:
          {f,g}
        TcT has computed the following interpretation:
          p(0) = [0]                  
          p(1) = [0]                  
          p(f) = [9]                  
          p(g) = [4] x1 + [2] x2 + [8]
          p(s) = [1] x1 + [0]         
        
        Following rules are strictly oriented:
        g(x,y) = [4] x + [2] y + [8]
               > [1] x + [0]        
               = x                  
        
        g(x,y) = [4] x + [2] y + [8]
               > [1] y + [0]        
               = y                  
        
        
        Following rules are (at-least) weakly oriented:
         f(x,y,s(z)) =  [9]            
                     >= [9]            
                     =  s(f(0(),1(),z))
        
        f(0(),1(),x) =  [9]            
                     >= [9]            
                     =  f(s(x),x,x)    
        
** Step 1.b:2: NaturalPI 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)
        - Weak TRS:
            g(x,y) -> x
            g(x,y) -> y
        - Signature:
            {f/3,g/2} / {0/0,1/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g} and constructors {0,1,s}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {f,g}
        TcT has computed the following interpretation:
          p(0) = 1          
          p(1) = 1          
          p(f) = 7 + 10*x3  
          p(g) = 8*x1 + 4*x2
          p(s) = 1 + x1     
        
        Following rules are strictly oriented:
        f(x,y,s(z)) = 17 + 10*z      
                    > 8 + 10*z       
                    = s(f(0(),1(),z))
        
        
        Following rules are (at-least) weakly oriented:
        f(0(),1(),x) =  7 + 10*x   
                     >= 7 + 10*x   
                     =  f(s(x),x,x)
        
              g(x,y) =  8*x + 4*y  
                     >= x          
                     =  x          
        
              g(x,y) =  8*x + 4*y  
                     >= y          
                     =  y          
        
** Step 1.b:3: NaturalMI 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))
            g(x,y) -> x
            g(x,y) -> y
        - Signature:
            {f/3,g/2} / {0/0,1/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g} and constructors {0,1,s}
    + Applied Processor:
        NaturalMI {miDimension = 3, miDegree = 3, 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(s) = {1}
        
        Following symbols are considered usable:
          {f,g}
        TcT has computed the following interpretation:
          p(0) = [0]                          
                 [2]                          
                 [1]                          
          p(1) = [0]                          
                 [1]                          
                 [0]                          
          p(f) = [0 2 2]      [6 0 0]      [0]
                 [0 3 0] x1 + [4 2 0] x3 + [3]
                 [0 0 2]      [0 0 4]      [0]
          p(g) = [4 1 0]      [4 0 2]      [0]
                 [2 1 2] x1 + [1 4 4] x2 + [0]
                 [0 0 1]      [0 1 1]      [1]
          p(s) = [1 0 2]      [2]             
                 [0 0 0] x1 + [2]             
                 [0 0 0]      [0]             
        
        Following rules are strictly oriented:
        f(0(),1(),x) = [6 0 0]     [6]
                       [4 2 0] x + [9]
                       [0 0 4]     [2]
                     > [6 0 0]     [4]
                       [4 2 0] x + [9]
                       [0 0 4]     [0]
                     = f(s(x),x,x)    
        
        
        Following rules are (at-least) weakly oriented:
        f(x,y,s(z)) =  [0 2 2]     [6 0 12]     [12]
                       [0 3 0] x + [4 0  8] z + [15]
                       [0 0 2]     [0 0  0]     [0] 
                    >= [6 0 8]     [12]             
                       [0 0 0] z + [2]              
                       [0 0 0]     [0]              
                    =  s(f(0(),1(),z))              
        
             g(x,y) =  [4 1 0]     [4 0 2]     [0]  
                       [2 1 2] x + [1 4 4] y + [0]  
                       [0 0 1]     [0 1 1]     [1]  
                    >= [1 0 0]     [0]              
                       [0 1 0] x + [0]              
                       [0 0 1]     [0]              
                    =  x                            
        
             g(x,y) =  [4 1 0]     [4 0 2]     [0]  
                       [2 1 2] x + [1 4 4] y + [0]  
                       [0 0 1]     [0 1 1]     [1]  
                    >= [1 0 0]     [0]              
                       [0 1 0] y + [0]              
                       [0 0 1]     [0]              
                    =  y                            
        
** Step 1.b:4: 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)
            g(x,y) -> x
            g(x,y) -> y
        - Signature:
            {f/3,g/2} / {0/0,1/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g} 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))