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

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