Problem:
 f(a()) -> b()
 f(a()) -> f(c())
 a() -> d()
 f(d()) -> b()
 f(c()) -> b()
 d() -> c()

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