YES

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

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   f(f(f(b()))) -> b()
   b() -> f(f(b()))
   a() -> f(a())
   a() -> b()
  weak:
   
  critical peaks: 3
   f(f(f(f(f(b()))))) <-1|0,0,0[]- f(f(f(b()))) -0|[]-> b()
   f(a()) <-2|[]- a() -3|[]-> b()
   b() <-3|[]- a() -2|[]-> f(a())
  Closedness Processor (*strongly -- <=7 steps*):
   
   Qed