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

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