Problem:
 f(a(),a()) -> b()
 a() -> a'()
 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:
  strict:
   
  weak:
   
  critical peaks: 8
   f(a'(),a()) <-1|0[]- f(a(),a()) -0|[]-> b()
   f(a(),a'()) <-1|1[]- f(a(),a()) -0|[]-> b()
   f(a'(),a'()) <-2|[]- f(a'(),a'()) -3|[]-> f(a'(),a'())
   f(a'(),a'()) <-2|[]- f(a'(),a'()) -4|[]-> b()
   f(a'(),a'()) <-3|[]- f(a'(),a'()) -2|[]-> f(a'(),a'())
   f(a'(),a'()) <-3|[]- f(a'(),a'()) -4|[]-> b()
   b() <-4|[]- f(a'(),a'()) -2|[]-> f(a'(),a'())
   b() <-4|[]- f(a'(),a'()) -3|[]-> f(a'(),a'())
  Redundant Rules Transformation:
   a() -> a'()
   f(a'(),x) -> f(x,x)
   f(x,a'()) -> f(x,x)
   b() -> f(a'(),a'())
   Church Rosser Transformation Processor (no redundant rules):
    strict:
     b() -> f(a'(),a'())
     f(x,a'()) -> f(x,x)
     f(a'(),x) -> f(x,x)
     a() -> a'()
    weak:
     
    critical peaks: 2
     f(a'(),a'()) <-1|[]- f(a'(),a'()) -2|[]-> f(a'(),a'())
     f(a'(),a'()) <-2|[]- f(a'(),a'()) -1|[]-> f(a'(),a'())
    Closedness Processor (*feeble*):
     
     Qed