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:
 Matrix Interpretation Processor:
  dimension: 3
  interpretation:
                     [1 0 1]     [1 0 0]     [1 0 3]     [1]
   [k](x0, x1, x2) = [0 0 1]x0 + [0 1 0]x1 + [0 0 1]x2 + [1]
                     [0 0 1]     [0 0 0]     [0 0 1]     [3],
   
             [1 0 2]     [0]
   [g](x0) = [0 0 2]x0 + [1]
             [0 0 0]     [0],
   
             [1 5 3]     [6]
   [h](x0) = [0 0 2]x0 + [4]
             [0 0 0]     [0],
   
             [1 0 7]     [0]
   [f](x0) = [0 0 1]x0 + [0]
             [0 0 0]     [1],
   
         [1]
   [a] = [0]
         [2]
  orientation:
            [15]    [13]            
   f(a()) = [2 ] >= [1 ] = g(h(a()))
            [1 ]    [0 ]            
   
             [1  0  12]    [11]    [1  0  12]    [9]             
   h(g(x)) = [0  0  0 ]x + [4 ] >= [0  0  0 ]x + [1] = g(h(f(x)))
             [0  0  0 ]    [0 ]    [0  0  0 ]    [0]             
   
                   [2 5 4]    [14]    [1 5 3]    [6]       
   k(x,h(x),a()) = [0 0 3]x + [7 ] >= [0 0 2]x + [4] = h(x)
                   [0 0 1]    [5 ]    [0 0 0]    [0]       
   
                 [2  0  10]    [1 0 0]    [2]    [1 0 7]    [0]       
   k(f(x),y,x) = [0  0  1 ]x + [0 1 0]y + [2] >= [0 0 1]x + [0] = f(x)
                 [0  0  1 ]    [0 0 0]    [4]    [0 0 0]    [1]       
  problem:
   
  Qed