YES(O(1),O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { 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) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(g) = {1, 2}, Uargs(h) = {2}

TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).

      [f](x1) = [0]                  
                                     
          [a] = [7]                  
                                     
          [b] = [7]                  
                                     
          [c] = [7]                  
                                     
          [d] = [7]                  
                                     
  [g](x1, x2) = [1] x1 + [1] x2 + [4]
                                     
  [h](x1, x2) = [1] x2 + [0]         
                                     
          [e] = [7]                  

The following symbols are considered usable

  {f, g}

The order satisfies the following ordering constraints:

      [f(a())] = [0]                        
               ? [7]                        
               = [b()]                      
                                            
      [f(c())] = [0]                        
               ? [7]                        
               = [d()]                      
                                            
  [f(g(x, y))] = [0]                        
               ? [4]                        
               = [g(f(x), f(y))]            
                                            
  [f(h(x, y))] = [0]                        
               ? [4]                        
               = [g(h(y, f(x)), h(x, f(y)))]
                                            
     [g(x, x)] = [2] x + [4]                
               > [1] x + [0]                
               = [h(e(), x)]                
                                            

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { 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 Trs: { g(x, x) -> h(e(), x) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(g) = {1, 2}, Uargs(h) = {2}

TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).

      [f](x1) = [4]                  
                                     
          [a] = [7]                  
                                     
          [b] = [3]                  
                                     
          [c] = [7]                  
                                     
          [d] = [3]                  
                                     
  [g](x1, x2) = [1] x1 + [1] x2 + [4]
                                     
  [h](x1, x2) = [1] x2 + [0]         
                                     
          [e] = [7]                  

The following symbols are considered usable

  {f, g}

The order satisfies the following ordering constraints:

      [f(a())] = [4]                        
               > [3]                        
               = [b()]                      
                                            
      [f(c())] = [4]                        
               > [3]                        
               = [d()]                      
                                            
  [f(g(x, y))] = [4]                        
               ? [12]                       
               = [g(f(x), f(y))]            
                                            
  [f(h(x, y))] = [4]                        
               ? [12]                       
               = [g(h(y, f(x)), h(x, f(y)))]
                                            
     [g(x, x)] = [2] x + [4]                
               > [1] x + [0]                
               = [h(e(), x)]                
                                            

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { f(g(x, y)) -> g(f(x), f(y))
  , f(h(x, y)) -> g(h(y, f(x)), h(x, f(y))) }
Weak Trs:
  { f(a()) -> b()
  , f(c()) -> d()
  , g(x, x) -> h(e(), x) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'polynomial interpretation' to orient
following rules strictly.

Trs:
  { f(g(x, y)) -> g(f(x), f(y))
  , f(h(x, y)) -> g(h(y, f(x)), h(x, f(y))) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  The following argument positions are considered usable:
  
    Uargs(g) = {1, 2}, Uargs(h) = {2}
  
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  
      [f](x1) = 2*x1 + 2*x1^2
                             
        [a]() = 0            
                             
        [b]() = 0            
                             
        [c]() = 0            
                             
        [d]() = 0            
                             
  [g](x1, x2) = 1 + x1 + x2  
                             
  [h](x1, x2) = 1 + x1 + x2  
                             
        [e]() = 0            
                             
  
  The following symbols are considered usable
  
    {f, g}
  
  This order satisfies the following ordering constraints.
  
        [f(a())] =                                               
                 >=                                              
                 =  [b()]                                        
                                                                 
        [f(c())] =                                               
                 >=                                              
                 =  [d()]                                        
                                                                 
    [f(g(x, y))] =  4 + 6*x + 6*y + 2*x^2 + 2*x*y + 2*y*x + 2*y^2
                 >  1 + 2*x + 2*x^2 + 2*y + 2*y^2                
                 =  [g(f(x), f(y))]                              
                                                                 
    [f(h(x, y))] =  4 + 6*x + 6*y + 2*x^2 + 2*x*y + 2*y*x + 2*y^2
                 >  3 + 3*y + 3*x + 2*x^2 + 2*y^2                
                 =  [g(h(y, f(x)), h(x, f(y)))]                  
                                                                 
       [g(x, x)] =  1 + 2*x                                      
                 >= 1 + x                                        
                 =  [h(e(), x)]                                  
                                                                 

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { 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) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^2))