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

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   
  weak:
   
  critical peaks: 0
  Qed