YES

Problem:
 f(a(),y) -> f(y,g(y))
 g(a()) -> b()
 g(b()) -> b()

Proof:
 DP Processor:
  DPs:
   f#(a(),y) -> g#(y)
   f#(a(),y) -> f#(y,g(y))
  TRS:
   f(a(),y) -> f(y,g(y))
   g(a()) -> b()
   g(b()) -> b()
  Usable Rule Processor:
   DPs:
    f#(a(),y) -> g#(y)
    f#(a(),y) -> f#(y,g(y))
   TRS:
    g(a()) -> b()
    g(b()) -> b()
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     g(a()) -> b()
     g(b()) -> b()
    interpretation:
     [g#](x0) = x0,
     
     [f#](x0, x1) = -4x0 + 1x1 + -16,
     
     [b] = 0,
     
     [g](x0) = -4x0 + 5,
     
     [a] = 11
    orientation:
     f#(a(),y) = 1y + 7 >= y = g#(y)
     
     f#(a(),y) = 1y + 7 >= -3y + 6 = f#(y,g(y))
     
     g(a()) = 7 >= 0 = b()
     
     g(b()) = 5 >= 0 = b()
    problem:
     DPs:
      
     TRS:
      g(a()) -> b()
      g(b()) -> b()
    Qed