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()
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [g#](x0) = x0,
    
    [f#](x0, x1) = -6x0 + 1x1 + -16,
    
    [b] = 0,
    
    [g](x0) = 1,
    
    [f](x0, x1) = -8x0 + 2x1 + 4,
    
    [a] = 13
   orientation:
    f#(a(),y) = 1y + 7 >= y = g#(y)
    
    f#(a(),y) = 1y + 7 >= -6y + 2 = f#(y,g(y))
    
    f(a(),y) = 2y + 5 >= -8y + 4 = f(y,g(y))
    
    g(a()) = 1 >= 0 = b()
    
    g(b()) = 1 >= 0 = b()
   problem:
    DPs:
     
    TRS:
     f(a(),y) -> f(y,g(y))
     g(a()) -> b()
     g(b()) -> b()
   Qed