YES

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

Proof:
 Bounds Processor:
  bound: 2
  enrichment: roof
  automaton:
   final states: {5,6}
   transitions:
    b1() -> 9,5
    f1(5,8) -> 5*
    f1(6,9) -> 5*
    g1(5) -> 8*
    g1(6) -> 9*
    b2() -> 12,8
    f2(9,12) -> 5*
    f0(5,5) -> 5*
    f0(6,6) -> 5*
    f0(5,6) -> 5*
    f0(6,5) -> 5*
    g2(9) -> 12*
    a0() -> 6*
    g0(5) -> 5*
    g0(6) -> 5*
    b0() -> 5*
  problem:
   
  Qed