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

Proof:
 Church Rosser Transformation Processor:
  
  critical peaks: joinable
  Qed