YES

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

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