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

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   
  weak:
   
  critical peaks: 4
  f(b(),a()) <-1|0[]- f(a(),a()) -0|[]-> g(f(a(),a()))
  f(a(),b()) <-1|1[]- f(a(),a()) -0|[]-> g(f(a(),a()))
  g(f(b(),b())) <-2|[]- f(b(),b()) -3|[]-> g(f(b(),b()))
  g(f(b(),b())) <-3|[]- f(b(),b()) -2|[]-> g(f(b(),b()))
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed