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

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