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

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