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

Proof:
 Uncurry Processor:
  f7(f(),b()) -> a()
  f7(f(),b()) -> f7(f(),c())
  f7(f(),c()) -> f7(f(),b())
  f7(f(),c()) -> d()
  b() -> e()
  c() -> e'()
  f7(f(),e()) -> a()
  f7(f(),e'()) -> d()
  Church Rosser Transformation Processor:
   f7(f(),b()) -> a()
   f7(f(),b()) -> f7(f(),c())
   f7(f(),c()) -> f7(f(),b())
   f7(f(),c()) -> d()
   b() -> e()
   c() -> e'()
   f7(f(),e()) -> a()
   f7(f(),e'()) -> d()
   critical peaks: joinable
   Qed