WORST_CASE(?,O(n^1))
* Step 1: Sum WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
            f(j(x,y),y) -> g(f(x,k(y)))
            g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
            h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
            i(f(x,h(y))) -> y
            i(h2(s(x),y,h1(x,z))) -> z
            k(h(x)) -> h1(0(),x)
            k(h1(x,y)) -> h1(s(x),y)
        - Signature:
            {f/2,g/1,h2/3,i/1,k/1} / {0/0,h/1,h1/2,j/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g,h2,i,k} and constructors {0,h,h1,j,s}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
            f(j(x,y),y) -> g(f(x,k(y)))
            g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
            h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
            i(f(x,h(y))) -> y
            i(h2(s(x),y,h1(x,z))) -> z
            k(h(x)) -> h1(0(),x)
            k(h1(x,y)) -> h1(s(x),y)
        - Signature:
            {f/2,g/1,h2/3,i/1,k/1} / {0/0,h/1,h1/2,j/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g,h2,i,k} and constructors {0,h,h1,j,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(f) = {2},
          uargs(g) = {1}
        
        Following symbols are considered usable:
          {f,g,h2,i,k}
        TcT has computed the following interpretation:
           p(0) = 0          
           p(f) = 4*x2       
           p(g) = x1         
           p(h) = x1         
          p(h1) = x2         
          p(h2) = 2*x1 + 2*x3
           p(i) = 4 + 2*x1   
           p(j) = 0          
           p(k) = x1         
           p(s) = 0          
        
        Following rules are strictly oriented:
                 i(f(x,h(y))) = 4 + 8*y
                              > y      
                              = y      
        
        i(h2(s(x),y,h1(x,z))) = 4 + 4*z
                              > z      
                              = z      
        
        
        Following rules are (at-least) weakly oriented:
                      f(x,h1(y,z)) =  4*z                  
                                   >= 2*z                  
                                   =  h2(0(),x,h1(y,z))    
        
                       f(j(x,y),y) =  4*y                  
                                   >= 4*y                  
                                   =  g(f(x,k(y)))         
        
                g(h2(x,y,h1(z,u))) =  2*u + 2*x            
                                   >= 2*u                  
                                   =  h2(s(x),y,h1(z,u))   
        
        h2(x,j(y,h1(z,u)),h1(z,u)) =  2*u + 2*x            
                                   >= 2*u                  
                                   =  h2(s(x),y,h1(s(z),u))
        
                           k(h(x)) =  x                    
                                   >= x                    
                                   =  h1(0(),x)            
        
                        k(h1(x,y)) =  y                    
                                   >= y                    
                                   =  h1(s(x),y)           
        
* Step 3: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
            f(j(x,y),y) -> g(f(x,k(y)))
            g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
            h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
            k(h(x)) -> h1(0(),x)
            k(h1(x,y)) -> h1(s(x),y)
        - Weak TRS:
            i(f(x,h(y))) -> y
            i(h2(s(x),y,h1(x,z))) -> z
        - Signature:
            {f/2,g/1,h2/3,i/1,k/1} / {0/0,h/1,h1/2,j/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g,h2,i,k} and constructors {0,h,h1,j,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(f) = {2},
          uargs(g) = {1}
        
        Following symbols are considered usable:
          {f,g,h2,i,k}
        TcT has computed the following interpretation:
           p(0) = 0      
           p(f) = x1 + x2
           p(g) = x1     
           p(h) = 3 + x1 
          p(h1) = x1 + x2
          p(h2) = x2 + x3
           p(i) = 4*x1   
           p(j) = 6 + x1 
           p(k) = 3 + x1 
           p(s) = 3 + x1 
        
        Following rules are strictly oriented:
                       f(j(x,y),y) = 6 + x + y            
                                   > 3 + x + y            
                                   = g(f(x,k(y)))         
        
        h2(x,j(y,h1(z,u)),h1(z,u)) = 6 + u + y + z        
                                   > 3 + u + y + z        
                                   = h2(s(x),y,h1(s(z),u))
        
                           k(h(x)) = 6 + x                
                                   > x                    
                                   = h1(0(),x)            
        
        
        Following rules are (at-least) weakly oriented:
                 f(x,h1(y,z)) =  x + y + z         
                              >= x + y + z         
                              =  h2(0(),x,h1(y,z)) 
        
           g(h2(x,y,h1(z,u))) =  u + y + z         
                              >= u + y + z         
                              =  h2(s(x),y,h1(z,u))
        
                 i(f(x,h(y))) =  12 + 4*x + 4*y    
                              >= y                 
                              =  y                 
        
        i(h2(s(x),y,h1(x,z))) =  4*x + 4*y + 4*z   
                              >= z                 
                              =  z                 
        
                   k(h1(x,y)) =  3 + x + y         
                              >= 3 + x + y         
                              =  h1(s(x),y)        
        
* Step 4: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
            g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
            k(h1(x,y)) -> h1(s(x),y)
        - Weak TRS:
            f(j(x,y),y) -> g(f(x,k(y)))
            h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
            i(f(x,h(y))) -> y
            i(h2(s(x),y,h1(x,z))) -> z
            k(h(x)) -> h1(0(),x)
        - Signature:
            {f/2,g/1,h2/3,i/1,k/1} / {0/0,h/1,h1/2,j/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g,h2,i,k} and constructors {0,h,h1,j,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(f) = {2},
          uargs(g) = {1}
        
        Following symbols are considered usable:
          {f,g,h2,i,k}
        TcT has computed the following interpretation:
           p(0) = 4          
           p(f) = 4*x1 + 4*x2
           p(g) = x1         
           p(h) = 1 + x1     
          p(h1) = x1 + x2    
          p(h2) = 4*x2 + 4*x3
           p(i) = x1         
           p(j) = 3 + x1 + x2
           p(k) = 3 + 2*x1   
           p(s) = 1          
        
        Following rules are strictly oriented:
        k(h1(x,y)) = 3 + 2*x + 2*y
                   > 1 + y        
                   = h1(s(x),y)   
        
        
        Following rules are (at-least) weakly oriented:
                      f(x,h1(y,z)) =  4*x + 4*y + 4*z      
                                   >= 4*x + 4*y + 4*z      
                                   =  h2(0(),x,h1(y,z))    
        
                       f(j(x,y),y) =  12 + 4*x + 8*y       
                                   >= 12 + 4*x + 8*y       
                                   =  g(f(x,k(y)))         
        
                g(h2(x,y,h1(z,u))) =  4*u + 4*y + 4*z      
                                   >= 4*u + 4*y + 4*z      
                                   =  h2(s(x),y,h1(z,u))   
        
        h2(x,j(y,h1(z,u)),h1(z,u)) =  12 + 8*u + 4*y + 8*z 
                                   >= 4 + 4*u + 4*y        
                                   =  h2(s(x),y,h1(s(z),u))
        
                      i(f(x,h(y))) =  4 + 4*x + 4*y        
                                   >= y                    
                                   =  y                    
        
             i(h2(s(x),y,h1(x,z))) =  4*x + 4*y + 4*z      
                                   >= z                    
                                   =  z                    
        
                           k(h(x)) =  5 + 2*x              
                                   >= 4 + x                
                                   =  h1(0(),x)            
        
* Step 5: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
            g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
        - Weak TRS:
            f(j(x,y),y) -> g(f(x,k(y)))
            h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
            i(f(x,h(y))) -> y
            i(h2(s(x),y,h1(x,z))) -> z
            k(h(x)) -> h1(0(),x)
            k(h1(x,y)) -> h1(s(x),y)
        - Signature:
            {f/2,g/1,h2/3,i/1,k/1} / {0/0,h/1,h1/2,j/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g,h2,i,k} and constructors {0,h,h1,j,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(f) = {2},
          uargs(g) = {1}
        
        Following symbols are considered usable:
          {f,g,h2,i,k}
        TcT has computed the following interpretation:
           p(0) = 0       
           p(f) = 5 + 5*x2
           p(g) = x1      
           p(h) = x1      
          p(h1) = x1 + x2 
          p(h2) = 4*x3    
           p(i) = x1      
           p(j) = x1 + x2 
           p(k) = x1      
           p(s) = x1      
        
        Following rules are strictly oriented:
        f(x,h1(y,z)) = 5 + 5*y + 5*z    
                     > 4*y + 4*z        
                     = h2(0(),x,h1(y,z))
        
        
        Following rules are (at-least) weakly oriented:
                       f(j(x,y),y) =  5 + 5*y              
                                   >= 5 + 5*y              
                                   =  g(f(x,k(y)))         
        
                g(h2(x,y,h1(z,u))) =  4*u + 4*z            
                                   >= 4*u + 4*z            
                                   =  h2(s(x),y,h1(z,u))   
        
        h2(x,j(y,h1(z,u)),h1(z,u)) =  4*u + 4*z            
                                   >= 4*u + 4*z            
                                   =  h2(s(x),y,h1(s(z),u))
        
                      i(f(x,h(y))) =  5 + 5*y              
                                   >= y                    
                                   =  y                    
        
             i(h2(s(x),y,h1(x,z))) =  4*x + 4*z            
                                   >= z                    
                                   =  z                    
        
                           k(h(x)) =  x                    
                                   >= x                    
                                   =  h1(0(),x)            
        
                        k(h1(x,y)) =  x + y                
                                   >= x + y                
                                   =  h1(s(x),y)           
        
* Step 6: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
        - Weak TRS:
            f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
            f(j(x,y),y) -> g(f(x,k(y)))
            h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
            i(f(x,h(y))) -> y
            i(h2(s(x),y,h1(x,z))) -> z
            k(h(x)) -> h1(0(),x)
            k(h1(x,y)) -> h1(s(x),y)
        - Signature:
            {f/2,g/1,h2/3,i/1,k/1} / {0/0,h/1,h1/2,j/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g,h2,i,k} and constructors {0,h,h1,j,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(f) = {2},
          uargs(g) = {1}
        
        Following symbols are considered usable:
          {f,g,h2,i,k}
        TcT has computed the following interpretation:
           p(0) = 4              
           p(f) = 2 + 4*x1 + 2*x2
           p(g) = 1 + x1         
           p(h) = 4 + x1         
          p(h1) = x1 + x2        
          p(h2) = 2*x2 + x3      
           p(i) = 2 + x1         
           p(j) = 2 + x1 + x2    
           p(k) = 2 + 2*x1       
           p(s) = 2              
        
        Following rules are strictly oriented:
        g(h2(x,y,h1(z,u))) = 1 + u + 2*y + z   
                           > u + 2*y + z       
                           = h2(s(x),y,h1(z,u))
        
        
        Following rules are (at-least) weakly oriented:
                      f(x,h1(y,z)) =  2 + 4*x + 2*y + 2*z  
                                   >= 2*x + y + z          
                                   =  h2(0(),x,h1(y,z))    
        
                       f(j(x,y),y) =  10 + 4*x + 6*y       
                                   >= 7 + 4*x + 4*y        
                                   =  g(f(x,k(y)))         
        
        h2(x,j(y,h1(z,u)),h1(z,u)) =  4 + 3*u + 2*y + 3*z  
                                   >= 2 + u + 2*y          
                                   =  h2(s(x),y,h1(s(z),u))
        
                      i(f(x,h(y))) =  12 + 4*x + 2*y       
                                   >= y                    
                                   =  y                    
        
             i(h2(s(x),y,h1(x,z))) =  2 + x + 2*y + z      
                                   >= z                    
                                   =  z                    
        
                           k(h(x)) =  10 + 2*x             
                                   >= 4 + x                
                                   =  h1(0(),x)            
        
                        k(h1(x,y)) =  2 + 2*x + 2*y        
                                   >= 2 + y                
                                   =  h1(s(x),y)           
        
* Step 7: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
            f(j(x,y),y) -> g(f(x,k(y)))
            g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
            h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
            i(f(x,h(y))) -> y
            i(h2(s(x),y,h1(x,z))) -> z
            k(h(x)) -> h1(0(),x)
            k(h1(x,y)) -> h1(s(x),y)
        - Signature:
            {f/2,g/1,h2/3,i/1,k/1} / {0/0,h/1,h1/2,j/2,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g,h2,i,k} and constructors {0,h,h1,j,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))