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

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   
  critical peaks: 3
  f(f(a())) <-0|[]- f(a()) -2|[]-> f(b())
  f(b()) <-1|0[]- f(a()) -0|[]-> f(f(a()))
  f(b()) <-2|[]- f(a()) -0|[]-> f(f(a()))
  Shift Processor lab=left (dd):
   
   strict:
    f(a()) -> f(f(a()))
    f(a()) -> f(b())
    f(f(a())) -> f(b())
    f(a()) -> f(b())
    f(a()) -> f(f(a()))
    f(f(a())) -> f(b())
    f(a()) -> f(b())
    f(a()) -> f(f(a()))
    f(f(a())) -> f(b())
   weak:
    f(a()) -> f(f(a()))
    a() -> b()
    f(x) -> f(b())
   Polynomial Interpretation Processor:
    dimension: 1
    interpretation:
     [b] = 0,
     
     [f](x0) = x0,
     
     [a] = 1
    orientation:
     f(a()) = 1 >= 1 = f(f(a()))
     
     f(a()) = 1 >= 0 = f(b())
     
     f(f(a())) = 1 >= 0 = f(b())
     
     f(a()) = 1 >= 0 = f(b())
     
     f(a()) = 1 >= 1 = f(f(a()))
     
     f(f(a())) = 1 >= 0 = f(b())
     
     f(a()) = 1 >= 0 = f(b())
     
     f(a()) = 1 >= 1 = f(f(a()))
     
     f(f(a())) = 1 >= 0 = f(b())
     
     a() = 1 >= 0 = b()
     
     f(x) = x >= 0 = f(b())
    problem:
     
     strict:
      f(a()) -> f(f(a()))
      f(a()) -> f(f(a()))
      f(a()) -> f(f(a()))
     weak:
      f(a()) -> f(f(a()))
      f(x) -> f(b())
    Shift Processor (ldh) lab=left (force):
     
     strict:
      
     weak:
      
     Decreasing Processor:
      The following diagrams are decreasing:
      peak:
       f(f(a())) <-0|[1]- f(a()) -2|[1]-> f(b())
      joins:
       f(f(a())) -2|[1]-> f(b())
       
      peak:
       f(b()) <-1|0[1]- f(a()) -0|[1]-> f(f(a()))
      joins:
       
       f(f(a())) -2|[1]-> f(b())
      peak:
       f(b()) <-2|[1]- f(a()) -0|[1]-> f(f(a()))
      joins:
       
       f(f(a())) -2|[1]-> f(b())
      Qed