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

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   f() -> g()
   g() -> f()
   h(x,a'(),y) -> h(x,y,y)
   a() -> a'()
  weak:
   
  critical peaks: 0
  Closedness Processor (*feeble*):
   
   Qed