*** 1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        f(x,0()) -> x
        f(0(),y) -> y
        f(1(),g(x,y)) -> x
        f(2(),g(x,y)) -> y
        f(f(x,y),z) -> f(x,f(y,z))
        f(g(x,y),z) -> g(f(x,z),f(y,z))
        f(i(x),y) -> i(x)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {f/2} / {0/0,1/0,2/0,g/2,i/1}
      Obligation:
        Full
        basic terms: {f}/{0,1,2,g,i}
    Applied Processor:
      NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a polynomial interpretation of kind constructor-based(mixed(2)):
      The following argument positions are considered usable:
        uargs(f) = {2},
        uargs(g) = {1,2}
      
      Following symbols are considered usable:
        {}
      TcT has computed the following interpretation:
        p(0) = 0                        
        p(1) = 0                        
        p(2) = 0                        
        p(f) = 1 + 2*x1 + 2*x1*x2 + 2*x2
        p(g) = 1 + x1 + x2              
        p(i) = 1                        
      
      Following rules are strictly oriented:
           f(x,0()) = 1 + 2*x      
                    > x            
                    = x            
      
           f(0(),y) = 1 + 2*y      
                    > y            
                    = y            
      
      f(1(),g(x,y)) = 3 + 2*x + 2*y
                    > x            
                    = x            
      
      f(2(),g(x,y)) = 3 + 2*x + 2*y
                    > y            
                    = y            
      
          f(i(x),y) = 3 + 4*y      
                    > 1            
                    = i(x)         
      
      
      Following rules are (at-least) weakly oriented:
      f(f(x,y),z) =  3 + 4*x + 4*x*y + 4*x*y*z + 4*x*z + 4*y + 4*y*z + 4*z
                  >= 3 + 4*x + 4*x*y + 4*x*y*z + 4*x*z + 4*y + 4*y*z + 4*z
                  =  f(x,f(y,z))                                          
      
      f(g(x,y),z) =  3 + 2*x + 2*x*z + 2*y + 2*y*z + 4*z                  
                  >= 3 + 2*x + 2*x*z + 2*y + 2*y*z + 4*z                  
                  =  g(f(x,z),f(y,z))                                     
      
*** 1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        f(f(x,y),z) -> f(x,f(y,z))
        f(g(x,y),z) -> g(f(x,z),f(y,z))
      Weak DP Rules:
        
      Weak TRS Rules:
        f(x,0()) -> x
        f(0(),y) -> y
        f(1(),g(x,y)) -> x
        f(2(),g(x,y)) -> y
        f(i(x),y) -> i(x)
      Signature:
        {f/2} / {0/0,1/0,2/0,g/2,i/1}
      Obligation:
        Full
        basic terms: {f}/{0,1,2,g,i}
    Applied Processor:
      NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a polynomial interpretation of kind constructor-based(mixed(2)):
      The following argument positions are considered usable:
        uargs(f) = {2},
        uargs(g) = {1,2}
      
      Following symbols are considered usable:
        {}
      TcT has computed the following interpretation:
        p(0) = 0                       
        p(1) = 1                       
        p(2) = 0                       
        p(f) = x1 + 2*x1*x2 + x1^2 + x2
        p(g) = 1 + x1 + x2             
        p(i) = x1                      
      
      Following rules are strictly oriented:
      f(g(x,y),z) = 2 + 3*x + 2*x*y + 2*x*z + x^2 + 3*y + 2*y*z + y^2 + 3*z
                  > 1 + x + 2*x*z + x^2 + y + 2*y*z + y^2 + 2*z            
                  = g(f(x,z),f(y,z))                                       
      
      
      Following rules are (at-least) weakly oriented:
           f(x,0()) =  x + x^2                                                                                                                    
                    >= x                                                                                                                          
                    =  x                                                                                                                          
      
           f(0(),y) =  y                                                                                                                          
                    >= y                                                                                                                          
                    =  y                                                                                                                          
      
      f(1(),g(x,y)) =  5 + 3*x + 3*y                                                                                                              
                    >= x                                                                                                                          
                    =  x                                                                                                                          
      
      f(2(),g(x,y)) =  1 + x + y                                                                                                                  
                    >= y                                                                                                                          
                    =  y                                                                                                                          
      
        f(f(x,y),z) =  x + 4*x*y + 4*x*y*z + 4*x*y^2 + 2*x*z + 2*x^2 + 6*x^2*y + 4*x^2*y^2 + 2*x^2*z + 2*x^3 + 4*x^3*y + x^4 + y + 2*y*z + y^2 + z
                    >= x + 2*x*y + 4*x*y*z + 2*x*y^2 + 2*x*z + x^2 + y + 2*y*z + y^2 + z                                                          
                    =  f(x,f(y,z))                                                                                                                
      
          f(i(x),y) =  x + 2*x*y + x^2 + y                                                                                                        
                    >= x                                                                                                                          
                    =  i(x)                                                                                                                       
      
*** 1.1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        f(f(x,y),z) -> f(x,f(y,z))
      Weak DP Rules:
        
      Weak TRS Rules:
        f(x,0()) -> x
        f(0(),y) -> y
        f(1(),g(x,y)) -> x
        f(2(),g(x,y)) -> y
        f(g(x,y),z) -> g(f(x,z),f(y,z))
        f(i(x),y) -> i(x)
      Signature:
        {f/2} / {0/0,1/0,2/0,g/2,i/1}
      Obligation:
        Full
        basic terms: {f}/{0,1,2,g,i}
    Applied Processor:
      NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a polynomial interpretation of kind constructor-based(mixed(2)):
      The following argument positions are considered usable:
        uargs(f) = {2},
        uargs(g) = {1,2}
      
      Following symbols are considered usable:
        {}
      TcT has computed the following interpretation:
        p(0) = 0                    
        p(1) = 0                    
        p(2) = 1                    
        p(f) = 2 + 3*x1 + x1*x2 + x2
        p(g) = 1 + x1 + x2          
        p(i) = 0                    
      
      Following rules are strictly oriented:
      f(f(x,y),z) = 8 + 9*x + 3*x*y + x*y*z + 3*x*z + 3*y + y*z + 3*z
                  > 4 + 5*x + 3*x*y + x*y*z + x*z + 3*y + y*z + z    
                  = f(x,f(y,z))                                      
      
      
      Following rules are (at-least) weakly oriented:
           f(x,0()) =  2 + 3*x                        
                    >= x                              
                    =  x                              
      
           f(0(),y) =  2 + y                          
                    >= y                              
                    =  y                              
      
      f(1(),g(x,y)) =  3 + x + y                      
                    >= x                              
                    =  x                              
      
      f(2(),g(x,y)) =  7 + 2*x + 2*y                  
                    >= y                              
                    =  y                              
      
        f(g(x,y),z) =  5 + 3*x + x*z + 3*y + y*z + 2*z
                    >= 5 + 3*x + x*z + 3*y + y*z + 2*z
                    =  g(f(x,z),f(y,z))               
      
          f(i(x),y) =  2 + y                          
                    >= 0                              
                    =  i(x)                           
      
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        f(x,0()) -> x
        f(0(),y) -> y
        f(1(),g(x,y)) -> x
        f(2(),g(x,y)) -> y
        f(f(x,y),z) -> f(x,f(y,z))
        f(g(x,y),z) -> g(f(x,z),f(y,z))
        f(i(x),y) -> i(x)
      Signature:
        {f/2} / {0/0,1/0,2/0,g/2,i/1}
      Obligation:
        Full
        basic terms: {f}/{0,1,2,g,i}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).