YES(?,O(n^3))

Problem:
 f(a()) -> g(h(a()))
 h(g(x)) -> g(h(f(x)))
 k(x,h(x),a()) -> h(x)
 k(f(x),y,x) -> f(x)

Proof:
 Complexity Transformation Processor:
  strict:
   f(a()) -> g(h(a()))
   h(g(x)) -> g(h(f(x)))
   k(x,h(x),a()) -> h(x)
   k(f(x),y,x) -> f(x)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [k](x0, x1, x2) = x0 + x1 + x2 + 1,
     
     [g](x0) = x0,
     
     [h](x0) = x0,
     
     [f](x0) = x0 + 1,
     
     [a] = 0
    orientation:
     f(a()) = 1 >= 0 = g(h(a()))
     
     h(g(x)) = x >= x + 1 = g(h(f(x)))
     
     k(x,h(x),a()) = 2x + 1 >= x = h(x)
     
     k(f(x),y,x) = 2x + y + 2 >= x + 1 = f(x)
    problem:
     strict:
      h(g(x)) -> g(h(f(x)))
     weak:
      f(a()) -> g(h(a()))
      k(x,h(x),a()) -> h(x)
      k(f(x),y,x) -> f(x)
    Matrix Interpretation Processor:
     dimension: 3
     max_matrix:
      [1 1 0]
      [0 1 1]
      [0 0 1]
      interpretation:
                         [1 1 0]     [1 0 0]     [1 1 0]     [0]
       [k](x0, x1, x2) = [0 1 1]x0 + [0 0 0]x1 + [0 1 1]x2 + [0]
                         [0 0 1]     [0 0 0]     [0 0 1]     [1],
       
                 [1 0 0]     [0]
       [g](x0) = [0 0 1]x0 + [1]
                 [0 0 0]     [0],
       
                 [1 1 0]     [0]
       [h](x0) = [0 0 0]x0 + [1]
                 [0 0 0]     [0],
       
                 [1 0 0]  
       [f](x0) = [0 0 1]x0
                 [0 0 0]  ,
       
             [0]
       [a] = [0]
             [1]
      orientation:
                 [1 0 1]    [1]    [1 0 1]    [0]             
       h(g(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = g(h(f(x)))
                 [0 0 0]    [0]    [0 0 0]    [0]             
       
                [0]    [0]            
       f(a()) = [1] >= [1] = g(h(a()))
                [0]    [0]            
       
                       [2 2 0]    [0]    [1 1 0]    [0]       
       k(x,h(x),a()) = [0 1 1]x + [1] >= [0 0 0]x + [1] = h(x)
                       [0 0 1]    [2]    [0 0 0]    [0]       
       
                     [2 1 1]    [1 0 0]    [0]    [1 0 0]        
       k(f(x),y,x) = [0 1 2]x + [0 0 0]y + [0] >= [0 0 1]x = f(x)
                     [0 0 1]    [0 0 0]    [1]    [0 0 0]        
      problem:
       strict:
        
       weak:
        h(g(x)) -> g(h(f(x)))
        f(a()) -> g(h(a()))
        k(x,h(x),a()) -> h(x)
        k(f(x),y,x) -> f(x)
      Qed