YES

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

Proof:
 Church Rosser Transformation Processor:
  
  critical peaks: joinable
  Qed