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

Proof:
 Church Rosser Transformation Processor:
  a() -> f(a(),b())
  f(a(),b()) -> f(b(),a())
  critical peaks: joinable
  Qed