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

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   
  critical peaks: 2
  f(f(f(a()))) <-0|[]- f(f(a())) -1|[]-> f(a())
  f(a()) <-1|[]- f(f(a())) -0|[]-> f(f(f(a())))
  Shift Processor lab=left (dd):
   
   strict:
    f(f(a())) -> f(f(f(a())))
    f(f(a())) -> f(a())
    f(f(f(a()))) -> f(f(a()))
    f(f(a())) -> f(a())
    f(f(a())) -> f(a())
    f(f(a())) -> f(f(f(a())))
    f(f(f(a()))) -> f(f(a()))
    f(f(a())) -> f(a())
   weak:
    f(f(a())) -> f(f(f(a())))
    f(f(a())) -> f(a())
   Shift Processor (ldh) lab=left (force):
    
    strict:
     
    weak:
     
    Rule Labeling Processor:
     
     strict:
      
     weak:
      
     rule labeling (right):
      f(f(a())) -> f(f(f(a()))): 2
      f(f(a())) -> f(a()): 0
     Decreasing Processor:
      The following diagrams are decreasing:
      peak:
       f(f(f(a()))) <-0|[1,2]- f(f(a())) -1|[1,0]-> f(a())
      joins:
       f(f(f(a()))) -1|0[1,0]-> f(f(a())) -1|[1,0]-> f(a())
       
      peak:
       f(a()) <-1|[1,0]- f(f(a())) -0|[1,2]-> f(f(f(a())))
      joins:
       
       f(f(f(a()))) -1|0[1,0]-> f(f(a())) -1|[1,0]-> f(a())
      Qed