YES(?,O(n^1))

Problem:
 a() -> g(c())
 g(a()) -> b()
 f(g(X),b()) -> f(a(),X)

Proof:
 Matrix Interpretation Processor:
  dimension: 1
  interpretation:
   [f](x0, x1) = x0 + x1 + 3,
   
   [b] = 8,
   
   [g](x0) = x0 + 4,
   
   [c] = 4,
   
   [a] = 9
  orientation:
   a() = 9 >= 8 = g(c())
   
   g(a()) = 13 >= 8 = b()
   
   f(g(X),b()) = X + 15 >= X + 12 = f(a(),X)
  problem:
   
  Qed