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

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   
  critical peaks: 11
  f(a()) <-0|0[]- f(f(f(f(x35)))) -0|[]-> a()
  f(f(a())) <-0|0,0[]- f(f(f(f(f(x36))))) -0|[]-> a()
  f(a()) <-1|0[]- f(f(f(a()))) -0|[]-> a()
  f(f(a())) <-1|0,0[]- f(f(f(f(a())))) -0|[]-> a()
  f(f(a())) <-2|0,0[]- f(f(f(a()))) -0|[]-> a()
  f(a()) <-2|0[]- f(f(a())) -1|[]-> a()
  g(a()) <-2|0[]- g(f(a())) -4|[]-> a()
  f(f(a())) <-3|0[]- f(f(f(g(g(x37))))) -0|[]-> a()
  f(f(f(a()))) <-3|0,0[]- f(f(f(f(g(g(x38)))))) -0|[]-> a()
  f(f(g(a()))) <-4|0,0,0[]- f(f(g(g(f(a()))))) -3|[]-> f(a())
  f(f(g(a()))) <-5|0,0,0[]- f(f(g(g(a())))) -3|[]-> f(a())
  Shift Processor lab=left (dd):
   
   strict:
    f(f(f(f(x35)))) -> f(a())
    f(f(f(f(x35)))) -> a()
    f(a()) -> a()
    f(f(f(f(f(x36))))) -> f(f(a()))
    f(f(f(f(f(x36))))) -> a()
    f(f(a())) -> a()
    f(f(f(a()))) -> f(a())
    f(f(f(a()))) -> a()
    f(a()) -> a()
    f(f(f(f(a())))) -> f(f(a()))
    f(f(f(f(a())))) -> a()
    f(f(a())) -> a()
    f(f(f(a()))) -> f(f(a()))
    f(f(f(a()))) -> a()
    f(f(a())) -> a()
    f(f(a())) -> f(a())
    f(f(a())) -> a()
    f(a()) -> a()
    g(f(a())) -> g(a())
    g(f(a())) -> a()
    g(a()) -> a()
    f(f(f(g(g(x37))))) -> f(f(a()))
    f(f(f(g(g(x37))))) -> a()
    f(f(a())) -> a()
    f(f(f(f(g(g(x38)))))) -> f(f(f(a())))
    f(f(f(f(g(g(x38)))))) -> a()
    f(f(f(a()))) -> a()
    f(f(g(g(f(a()))))) -> f(f(g(a())))
    f(f(g(g(f(a()))))) -> f(a())
    f(f(g(a()))) -> f(f(a()))
    f(f(a())) -> a()
    f(a()) -> a()
    f(f(g(a()))) -> f(f(a()))
    f(f(a())) -> f(a())
    f(f(g(g(a())))) -> f(f(g(a())))
    f(f(g(g(a())))) -> f(a())
    f(f(g(a()))) -> f(f(a()))
    f(f(a())) -> a()
    f(a()) -> a()
    f(f(g(a()))) -> f(f(a()))
    f(f(a())) -> f(a())
   weak:
    f(f(f(x))) -> a()
    f(f(a())) -> a()
    f(a()) -> a()
    f(f(g(g(x)))) -> f(a())
    g(f(a())) -> a()
    g(a()) -> a()
   LPO Processor:
    precedence:
     g > a ~ f
    problem:
     
     strict:
      
     weak:
      
    Shift Processor (ldh) lab=left (force):
     
     strict:
      
     weak:
      
     Decreasing Processor:
      The following diagrams are decreasing:
      peak:
       f(a()) <-0|0[1]- f(f(f(f(x35)))) -0|[1]-> a()
      joins:
       f(a()) -2|[0]-> a()
       
      peak:
       f(f(a())) <-0|0,0[1]- f(f(f(f(f(x36))))) -0|[1]-> a()
      joins:
       f(f(a())) -1|[0]-> a()
       
      peak:
       f(a()) <-1|0[1]- f(f(f(a()))) -0|[1]-> a()
      joins:
       f(a()) -2|[0]-> a()
       
      peak:
       f(f(a())) <-1|0,0[1]- f(f(f(f(a())))) -0|[1]-> a()
      joins:
       f(f(a())) -1|[0]-> a()
       
      peak:
       f(f(a())) <-2|0,0[1]- f(f(f(a()))) -0|[1]-> a()
      joins:
       f(f(a())) -1|[0]-> a()
       
      peak:
       f(a()) <-2|0[1]- f(f(a())) -1|[1]-> a()
      joins:
       f(a()) -2|[0]-> a()
       
      peak:
       g(a()) <-2|0[1]- g(f(a())) -4|[1]-> a()
      joins:
       g(a()) -5|[0]-> a()
       
      peak:
       f(f(a())) <-3|0[1]- f(f(f(g(g(x37))))) -0|[1]-> a()
      joins:
       f(f(a())) -1|[0]-> a()
       
      peak:
       f(f(f(a()))) <-3|0,0[1]- f(f(f(f(g(g(x38)))))) -0|[1]-> a()
      joins:
       f(f(f(a()))) -0|[0]-> a()
       
      peak:
       f(f(g(a()))) <-4|0,0,0[1]- f(f(g(g(f(a()))))) -3|[1]-> f(a())
      joins:
       f(f(g(a()))) -5|0,0[0]-> f(f(a())) -2|0[0]-> f(a())
       
      peak:
       f(f(g(a()))) <-5|0,0,0[1]- f(f(g(g(a())))) -3|[1]-> f(a())
      joins:
       f(f(g(a()))) -5|0,0[0]-> f(f(a())) -2|0[0]-> f(a())
       
      Qed