*** 1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        f(a()) -> b()
        f(c()) -> d()
        f(g(x,y)) -> g(f(x),f(y))
        f(h(x,y)) -> g(h(y,f(x)),h(x,f(y)))
        g(x,x) -> h(e(),x)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {f/1,g/2} / {a/0,b/0,c/0,d/0,e/0,h/2}
      Obligation:
        Full
        basic terms: {f,g}/{a,b,c,d,e,h}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following nonconstant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(g) = {1,2},
          uargs(h) = {2}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
          p(a) = [0]                  
          p(b) = [0]                  
          p(c) = [0]                  
          p(d) = [0]                  
          p(e) = [0]                  
          p(f) = [0]                  
          p(g) = [1] x1 + [1] x2 + [5]
          p(h) = [1] x2 + [0]         
        
        Following rules are strictly oriented:
        g(x,x) = [2] x + [5]
               > [1] x + [0]
               = h(e(),x)   
        
        
        Following rules are (at-least) weakly oriented:
           f(a()) =  [0]                   
                  >= [0]                   
                  =  b()                   
        
           f(c()) =  [0]                   
                  >= [0]                   
                  =  d()                   
        
        f(g(x,y)) =  [0]                   
                  >= [5]                   
                  =  g(f(x),f(y))          
        
        f(h(x,y)) =  [0]                   
                  >= [5]                   
                  =  g(h(y,f(x)),h(x,f(y)))
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        f(a()) -> b()
        f(c()) -> d()
        f(g(x,y)) -> g(f(x),f(y))
        f(h(x,y)) -> g(h(y,f(x)),h(x,f(y)))
      Weak DP Rules:
        
      Weak TRS Rules:
        g(x,x) -> h(e(),x)
      Signature:
        {f/1,g/2} / {a/0,b/0,c/0,d/0,e/0,h/2}
      Obligation:
        Full
        basic terms: {f,g}/{a,b,c,d,e,h}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following nonconstant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(g) = {1,2},
          uargs(h) = {2}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
          p(a) = [1]                  
          p(b) = [2]                  
          p(c) = [0]                  
          p(d) = [2]                  
          p(e) = [1]                  
          p(f) = [5]                  
          p(g) = [1] x1 + [1] x2 + [8]
          p(h) = [1] x2 + [0]         
        
        Following rules are strictly oriented:
        f(a()) = [5]
               > [2]
               = b()
        
        f(c()) = [5]
               > [2]
               = d()
        
        
        Following rules are (at-least) weakly oriented:
        f(g(x,y)) =  [5]                   
                  >= [18]                  
                  =  g(f(x),f(y))          
        
        f(h(x,y)) =  [5]                   
                  >= [18]                  
                  =  g(h(y,f(x)),h(x,f(y)))
        
           g(x,x) =  [2] x + [8]           
                  >= [1] x + [0]           
                  =  h(e(),x)              
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        f(g(x,y)) -> g(f(x),f(y))
        f(h(x,y)) -> g(h(y,f(x)),h(x,f(y)))
      Weak DP Rules:
        
      Weak TRS Rules:
        f(a()) -> b()
        f(c()) -> d()
        g(x,x) -> h(e(),x)
      Signature:
        {f/1,g/2} / {a/0,b/0,c/0,d/0,e/0,h/2}
      Obligation:
        Full
        basic terms: {f,g}/{a,b,c,d,e,h}
    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(g) = {1,2},
        uargs(h) = {2}
      
      Following symbols are considered usable:
        {}
      TcT has computed the following interpretation:
        p(a) = 1          
        p(b) = 0          
        p(c) = 0          
        p(d) = 0          
        p(e) = 0          
        p(f) = 2*x1 + x1^2
        p(g) = 1 + x1 + x2
        p(h) = 1 + x1 + x2
      
      Following rules are strictly oriented:
      f(g(x,y)) = 3 + 4*x + 2*x*y + x^2 + 4*y + y^2
                > 1 + 2*x + x^2 + 2*y + y^2        
                = g(f(x),f(y))                     
      
      
      Following rules are (at-least) weakly oriented:
         f(a()) =  3                                
                >= 0                                
                =  b()                              
      
         f(c()) =  0                                
                >= 0                                
                =  d()                              
      
      f(h(x,y)) =  3 + 4*x + 2*x*y + x^2 + 4*y + y^2
                >= 3 + 3*x + x^2 + 3*y + y^2        
                =  g(h(y,f(x)),h(x,f(y)))           
      
         g(x,x) =  1 + 2*x                          
                >= 1 + x                            
                =  h(e(),x)                         
      
*** 1.1.1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        f(h(x,y)) -> g(h(y,f(x)),h(x,f(y)))
      Weak DP Rules:
        
      Weak TRS Rules:
        f(a()) -> b()
        f(c()) -> d()
        f(g(x,y)) -> g(f(x),f(y))
        g(x,x) -> h(e(),x)
      Signature:
        {f/1,g/2} / {a/0,b/0,c/0,d/0,e/0,h/2}
      Obligation:
        Full
        basic terms: {f,g}/{a,b,c,d,e,h}
    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(g) = {1,2},
        uargs(h) = {2}
      
      Following symbols are considered usable:
        {}
      TcT has computed the following interpretation:
        p(a) = 1            
        p(b) = 0            
        p(c) = 0            
        p(d) = 0            
        p(e) = 0            
        p(f) = 3*x1 + 2*x1^2
        p(g) = 1 + x1 + x2  
        p(h) = 1 + x1 + x2  
      
      Following rules are strictly oriented:
      f(h(x,y)) = 5 + 7*x + 4*x*y + 2*x^2 + 7*y + 2*y^2
                > 3 + 4*x + 2*x^2 + 4*y + 2*y^2        
                = g(h(y,f(x)),h(x,f(y)))               
      
      
      Following rules are (at-least) weakly oriented:
         f(a()) =  5                                    
                >= 0                                    
                =  b()                                  
      
         f(c()) =  0                                    
                >= 0                                    
                =  d()                                  
      
      f(g(x,y)) =  5 + 7*x + 4*x*y + 2*x^2 + 7*y + 2*y^2
                >= 1 + 3*x + 2*x^2 + 3*y + 2*y^2        
                =  g(f(x),f(y))                         
      
         g(x,x) =  1 + 2*x                              
                >= 1 + x                                
                =  h(e(),x)                             
      
*** 1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        f(a()) -> b()
        f(c()) -> d()
        f(g(x,y)) -> g(f(x),f(y))
        f(h(x,y)) -> g(h(y,f(x)),h(x,f(y)))
        g(x,x) -> h(e(),x)
      Signature:
        {f/1,g/2} / {a/0,b/0,c/0,d/0,e/0,h/2}
      Obligation:
        Full
        basic terms: {f,g}/{a,b,c,d,e,h}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).