YES

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

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   b() -> f(a'(),a'())
   f(a'(),a'()) -> b()
   f(x,a'()) -> f(x,x)
   f(a'(),x) -> f(x,x)
  weak:
   
  critical peaks: 6
   b() <-1|[]- f(a'(),a'()) -2|[]-> f(a'(),a'())
   b() <-1|[]- f(a'(),a'()) -3|[]-> f(a'(),a'())
   f(a'(),a'()) <-2|[]- f(a'(),a'()) -1|[]-> b()
   f(a'(),a'()) <-2|[]- f(a'(),a'()) -3|[]-> f(a'(),a'())
   f(a'(),a'()) <-3|[]- f(a'(),a'()) -1|[]-> b()
   f(a'(),a'()) <-3|[]- f(a'(),a'()) -2|[]-> f(a'(),a'())
  Closedness Processor (*feeble*):
   
   Qed