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

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   f(0)(x) -> g(0)(x)
   f(0)(x) -> g(1)(f(0)(x))
   f(0)(f(0)(f(0)(f(0)(x)))) -> f(0)(f(0)(f(0)(g(0)(x))))
   f(0)(f(0)(f(0)(f(0)(x)))) -> f(0)(f(0)(f(0)(g(1)(f(0)(x)))))
  weak:
   
  critical peaks: 8
  f(f(f(f(g(x11,f(x11)))))) <-0|0[]- f(f(f(f(f(x11))))) -0|[]-> f(f(f(g(f(x11),f(f(x11))))))
  f(f(f(f(f(g(x12,f(x12))))))) <-0|0,0[]- f(f(f(f(f(f(x12)))))) -0|[]-> 
                                          f(f(f(g(f(f(x12)),f(f(f(x12)))))))
  f(f(f(f(f(f(g(x13,f(x13)))))))) <-0|0,0,0[]- f(f(f(f(f(f(f(x13))))))) -0|
                                               []-> f(f(f(g(f(f(f(x13))),f(f(f(f(x13))))))))
  f(f(f(g(x14,f(x14))))) <-0|[]- f(f(f(f(x14)))) -1|[]-> g(f(f(f(x14))),f(f(f(f(x14)))))
  g(f(f(f(x))),f(f(f(f(x))))) <-1|[]- f(f(f(f(x)))) -0|[]-> f(f(f(g(x,f(x)))))
  f(g(f(f(x)),f(f(f(x))))) <-1|0[]- f(f(f(f(x)))) -0|[]-> f(f(f(g(x,f(x)))))
  f(f(g(f(x),f(f(x))))) <-1|0,0[]- f(f(f(f(x)))) -0|[]-> f(f(f(g(x,f(x)))))
  f(f(f(g(x,f(x))))) <-1|0,0,0[]- f(f(f(f(x)))) -0|[]-> f(f(f(g(x,f(x)))))
  Matrix Interpretation Processor: dim=2, lab=right
   
   interpretation:
                 [1 0]  
    [g(1)](x0) = [0 0]x0,
    
                 [1 0]     [0]
    [g(0)](x0) = [0 0]x0 + [1],
    
                 [1 1]     [0]
    [f(0)](x0) = [0 0]x0 + [1]
   orientation:
              [1 1]    [0]    [1 0]    [0]          
    f(0)(x) = [0 0]x + [1] >= [0 0]x + [1] = g(0)(x)
    
              [1 1]    [0]    [1 1]                 
    f(0)(x) = [0 0]x + [1] >= [0 0]x = g(1)(f(0)(x))
    
                                [1 1]    [3]    [1 0]    [3]                            
    f(0)(f(0)(f(0)(f(0)(x)))) = [0 0]x + [1] >= [0 0]x + [1] = f(0)(f(0)(f(0)(g(0)(x))))
    
                                [1 1]    [3]    [1 1]    [2]                                  
    f(0)(f(0)(f(0)(f(0)(x)))) = [0 0]x + [1] >= [0 0]x + [1] = f(0)(f(0)(f(0)(g(1)(f(0)(x)))))
   problem:
    
    strict:
     f(0)(x) -> g(0)(x)
     f(0)(x) -> g(1)(f(0)(x))
     f(0)(f(0)(f(0)(f(0)(x)))) -> f(0)(f(0)(f(0)(g(0)(x))))
    weak:
     
   Matrix Interpretation Processor: dim=2, lab=right
    
    interpretation:
                    
     [g(1)](x0) = x0,
     
                  [1 0]  
     [g(0)](x0) = [0 0]x0,
     
                  [1 1]     [0]
     [f(0)](x0) = [0 0]x0 + [1]
    orientation:
               [1 1]    [0]    [1 0]           
     f(0)(x) = [0 0]x + [1] >= [0 0]x = g(0)(x)
     
               [1 1]    [0]    [1 1]    [0]                
     f(0)(x) = [0 0]x + [1] >= [0 0]x + [1] = g(1)(f(0)(x))
     
                                 [1 1]    [3]    [1 0]    [2]                            
     f(0)(f(0)(f(0)(f(0)(x)))) = [0 0]x + [1] >= [0 0]x + [1] = f(0)(f(0)(f(0)(g(0)(x))))
    problem:
     
     strict:
      f(0)(x) -> g(0)(x)
      f(0)(x) -> g(1)(f(0)(x))
     weak:
      
    Matrix Interpretation Processor: dim=1, lab=right
     
     interpretation:
      [g(1)](x0) = x0,
      
      [g(0)](x0) = x0,
      
      [f(0)](x0) = x0 + 2
     orientation:
      f(0)(x) = x + 2 >= x = g(0)(x)
      
      f(0)(x) = x + 2 >= x + 2 = g(1)(f(0)(x))
     problem:
      
      strict:
       f(0)(x) -> g(1)(f(0)(x))
      weak:
       
     Shift Processor (**) lab=left:
      
      strict:
       
      weak:
       
      Shift Processor lab=left (dd):
       
       strict:
        f(f(f(f(f(x11))))) -> f(f(f(f(g(x11,f(x11))))))
        f(f(f(f(f(x11))))) -> f(f(f(g(f(x11),f(f(x11))))))
        f(f(f(f(g(x11,f(x11)))))) -> f(f(f(g(g(x11,f(x11)),f(g(x11,f(x11)))))))
        f(f(f(g(f(x11),f(f(x11)))))) -> f(f(f(g(f(x11),f(g(x11,f(x11)))))))
        f(f(f(g(f(x11),f(g(x11,f(x11))))))) -> f(f(f(g(g(x11,f(x11)),f(g(x11,f(x11)))))))
        f(f(f(f(g(x11,f(x11)))))) -> f(f(f(g(g(x11,f(x11)),f(g(x11,f(x11)))))))
        f(f(f(g(f(x11),f(f(x11)))))) -> f(f(f(g(g(x11,f(x11)),f(f(x11))))))
        f(f(f(g(g(x11,f(x11)),f(f(x11)))))) -> f(f(f(g(g(x11,f(x11)),f(g(x11,f(x11)))))))
        f(f(f(f(f(f(x12)))))) -> f(f(f(f(f(g(x12,f(x12)))))))
        f(f(f(f(f(f(x12)))))) -> f(f(f(g(f(f(x12)),f(f(f(x12)))))))
        f(f(f(f(f(g(x12,f(x12))))))) -> f(f(f(g(f(g(x12,f(x12))),f(f(g(x12,f(x12))))))))
        f(f(f(g(f(f(x12)),f(f(f(x12))))))) -> f(f(f(g(f(f(x12)),f(f(g(x12,f(x12))))))))
        f(f(f(g(f(f(x12)),f(f(g(x12,f(x12)))))))) ->
        f(f(f(g(f(g(x12,f(x12))),f(f(g(x12,f(x12))))))))
        f(f(f(f(f(g(x12,f(x12))))))) -> f(f(f(g(f(g(x12,f(x12))),f(f(g(x12,f(x12))))))))
        f(f(f(g(f(f(x12)),f(f(f(x12))))))) -> f(f(f(g(f(g(x12,f(x12))),f(f(f(x12)))))))
        f(f(f(g(f(g(x12,f(x12))),f(f(f(x12))))))) ->
        f(f(f(g(f(g(x12,f(x12))),f(f(g(x12,f(x12))))))))
        f(f(f(f(f(f(f(x13))))))) -> f(f(f(f(f(f(g(x13,f(x13))))))))
        f(f(f(f(f(f(f(x13))))))) -> f(f(f(g(f(f(f(x13))),f(f(f(f(x13))))))))
        f(f(f(f(f(f(g(x13,f(x13)))))))) -> f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(g(x13,f(x13)))))))))
        f(f(f(g(f(f(f(x13))),f(f(f(f(x13)))))))) -> f(f(f(g(f(f(f(x13))),f(f(f(g(x13,f(x13)))))))))
        f(f(f(g(f(f(f(x13))),f(f(f(g(x13,f(x13))))))))) ->
        f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(g(x13,f(x13)))))))))
        f(f(f(f(f(f(g(x13,f(x13)))))))) -> f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(g(x13,f(x13)))))))))
        f(f(f(g(f(f(f(x13))),f(f(f(f(x13)))))))) -> f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(f(x13))))))))
        f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(f(x13)))))))) ->
        f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(g(x13,f(x13)))))))))
        f(f(f(f(x14)))) -> f(f(f(g(x14,f(x14)))))
        f(f(f(f(x14)))) -> g(f(f(f(x14))),f(f(f(f(x14)))))
        f(f(f(g(x14,f(x14))))) -> g(f(f(g(x14,f(x14)))),f(f(f(g(x14,f(x14))))))
        g(f(f(f(x14))),f(f(f(f(x14))))) -> g(f(f(f(x14))),f(f(f(g(x14,f(x14))))))
        g(f(f(f(x14))),f(f(f(g(x14,f(x14)))))) -> g(f(f(g(x14,f(x14)))),f(f(f(g(x14,f(x14))))))
        f(f(f(g(x14,f(x14))))) -> g(f(f(g(x14,f(x14)))),f(f(f(g(x14,f(x14))))))
        g(f(f(f(x14))),f(f(f(f(x14))))) -> g(f(f(g(x14,f(x14)))),f(f(f(f(x14)))))
        g(f(f(g(x14,f(x14)))),f(f(f(f(x14))))) -> g(f(f(g(x14,f(x14)))),f(f(f(g(x14,f(x14))))))
        f(f(f(f(x)))) -> g(f(f(f(x))),f(f(f(f(x)))))
        f(f(f(f(x)))) -> f(f(f(g(x,f(x)))))
        g(f(f(f(x))),f(f(f(f(x))))) -> g(f(f(f(x))),f(f(f(g(x,f(x))))))
        g(f(f(f(x))),f(f(f(g(x,f(x)))))) -> g(f(f(g(x,f(x)))),f(f(f(g(x,f(x))))))
        f(f(f(g(x,f(x))))) -> g(f(f(g(x,f(x)))),f(f(f(g(x,f(x))))))
        g(f(f(f(x))),f(f(f(f(x))))) -> g(f(f(g(x,f(x)))),f(f(f(f(x)))))
        g(f(f(g(x,f(x)))),f(f(f(f(x))))) -> g(f(f(g(x,f(x)))),f(f(f(g(x,f(x))))))
        f(f(f(g(x,f(x))))) -> g(f(f(g(x,f(x)))),f(f(f(g(x,f(x))))))
        f(f(f(f(x)))) -> f(g(f(f(x)),f(f(f(x)))))
        f(f(f(f(x)))) -> f(f(f(g(x,f(x)))))
        f(g(f(f(x)),f(f(f(x))))) -> f(g(f(f(x)),f(f(g(x,f(x))))))
        f(g(f(f(x)),f(f(g(x,f(x)))))) -> f(g(f(g(x,f(x))),f(f(g(x,f(x))))))
        f(f(f(g(x,f(x))))) -> f(g(f(g(x,f(x))),f(f(g(x,f(x))))))
        f(g(f(f(x)),f(f(f(x))))) -> f(g(f(g(x,f(x))),f(f(f(x)))))
        f(g(f(g(x,f(x))),f(f(f(x))))) -> f(g(f(g(x,f(x))),f(f(g(x,f(x))))))
        f(f(f(g(x,f(x))))) -> f(g(f(g(x,f(x))),f(f(g(x,f(x))))))
        f(f(f(f(x)))) -> f(f(g(f(x),f(f(x)))))
        f(f(f(f(x)))) -> f(f(f(g(x,f(x)))))
        f(f(g(f(x),f(f(x))))) -> f(f(g(f(x),f(g(x,f(x))))))
        f(f(g(f(x),f(g(x,f(x)))))) -> f(f(g(g(x,f(x)),f(g(x,f(x))))))
        f(f(f(g(x,f(x))))) -> f(f(g(g(x,f(x)),f(g(x,f(x))))))
        f(f(g(f(x),f(f(x))))) -> f(f(g(g(x,f(x)),f(f(x)))))
        f(f(g(g(x,f(x)),f(f(x))))) -> f(f(g(g(x,f(x)),f(g(x,f(x))))))
        f(f(f(g(x,f(x))))) -> f(f(g(g(x,f(x)),f(g(x,f(x))))))
        f(f(f(f(x)))) -> f(f(f(g(x,f(x)))))
        f(f(f(f(x)))) -> f(f(f(g(x,f(x)))))
       weak:
        f(f(f(f(x)))) -> f(f(f(g(x,f(x)))))
        f(x) -> g(x,f(x))
       Shift Processor (ldh) lab=left (force):
        
        strict:
         
        weak:
         
        Rule Labeling Processor:
         
         strict:
          
         weak:
          
         rule labeling (left):
          f(f(f(f(x)))) -> f(f(f(g(x,f(x))))): 1
          f(x) -> g(x,f(x)): 0
         Decreasing Processor:
          The following diagrams are decreasing:
          peak:
           f(f(f(f(g(x11,f(x11)))))) <-0|0[1,1,0,0,2]- f(f(f(f(f(x11))))) -0|
                                                       [1,1,0,0,0]-> 
                                                       f(f(f(g(f(x11),f(f(x11))))))
          joins:
           f(f(f(f(g(x11,f(x11)))))) -0|[1,1,0,0,0]-> f(f(f(g(g(x11,f(x11)),f(g(x11,f(x11)))))))
           f(f(f(g(f(x11),f(f(x11)))))) -1|0,0,0,1,0[0,1,2,3,8]-> f(f
                                                                    (
                                                                    f(g(f(x11),f(g(x11,f(x11))))))) -1|
                                                                  0,0,
                                                                  0,0[
                                                                  0,1,3,2,6]-> 
                                                                  f(f
                                                                    (
                                                                    f
                                                                    (
                                                                    g
                                                                    (
                                                                    g(x11,f(x11)),f(g(x11,f(x11)))))))
          peak:
           f(f(f(f(f(g(x12,f(x12))))))) <-0|0,0[1,1,1,1,4]- f(f(f(f(f(f(x12)))))) -0|
                                                            [1,1,0,0,0]-> 
                                                            f(f(f(g(f(f(x12)),f(f(f(x12)))))))
          joins:
           f(f(f(f(f(g(x12,f(x12))))))) -0|[1,1,0,0,0]-> f(f(f(g(f(g(x12,f(x12))),
                                                                 f(f(g(x12,f(x12))))))))
           f(f(f(g(f(f(x12)),f(f(f(x12))))))) -1|0,0,0,1,0,0[0,1,3,4,10]-> 
            f(f(f(g(f(f(x12)),f(f(g(x12,f(x12)))))))) -1|0,0,0,0,0[0,1,3,2,8]-> 
            f(f(f(g(f(g(x12,f(x12))),f(f(g(x12,f(x12))))))))
          peak:
           f(f(f(f(f(f(g(x13,f(x13)))))))) <-0|0,0,0[1,1,2,2,6]- f(f(f(f(f(f(f(x13))))))) -0|
                                                                 [1,1,0,0,0]-> 
                                                                 f(f(
                                                                    f
                                                                    (
                                                                    g(f(f(f(x13))),f(f(f(f(x13))))))))
          joins:
           f(f(f(f(f(f(g(x13,f(x13)))))))) -0|[1,1,0,0,0]-> f(f(f(g(f(f(g(x13,f(x13)))),
                                                                    f
                                                                    (f(f(g(x13,f(x13)))))))))
           f(f(f(g(f(f(f(x13))),f(f(f(f(x13)))))))) -0|0,0,0,1[1,1,2,2,6]-> 
            f(f(f(g(f(f(f(x13))),f(f(f(g(x13,f(x13))))))))) -1|0,0,0,0,0,0[
            0,1,4,3,10]-> f(f(f(g(f(f(g(x13,f(x13)))),f(f(f(g(x13,f(x13)))))))))
          peak:
           f(f(f(g(x14,f(x14))))) <-0|[1,1,0,0,0]- f(f(f(f(x14)))) -1|
                                                   [0,1,0,0,0]-> g(f(f(f(x14))),f(f(f(f(x14)))))
          joins:
           f(f(f(g(x14,f(x14))))) -1|[0,1,0,0,0]-> g(f(f(g(x14,f(x14)))),f(f(f(g(x14,f(x14))))))
           g(f(f(f(x14))),f(f(f(f(x14))))) -0|1[1,1,0,0,0]-> g(f(f(f(x14))),f(f(f(g(x14,f(x14)))))) -1|
                                                             0,0,0[0,1,1,1,4]-> 
                                                             g(f(f(g(x14,f(x14)))),
                                                               f(f(f(g(x14,f(x14))))))
          peak:
           g(f(f(f(x))),f(f(f(f(x))))) <-1|[0,1,0,0,0]- f(f(f(f(x)))) -0|
                                                        [1,1,0,0,0]-> 
                                                        f(f(f(g(x,f(x)))))
          joins:
           g(f(f(f(x))),f(f(f(f(x))))) -0|1[1,1,0,0,0]-> g(f(f(f(x))),f(f(f(g(x,f(x)))))) -1|
                                                         0,0,0[0,1,1,1,4]-> 
                                                         g(f(f(g(x,f(x)))),f(f(f(g(x,f(x))))))
           f(f(f(g(x,f(x))))) -1|[0,1,0,0,0]-> g(f(f(g(x,f(x)))),f(f(f(g(x,f(x))))))
          peak:
           f(g(f(f(x)),f(f(f(x))))) <-1|0[0,1,0,0,2]- f(f(f(f(x)))) -0|
                                                      [1,1,0,0,0]-> f(f(f(g(x,f(x)))))
          joins:
           f(g(f(f(x)),f(f(f(x))))) -1|0,1,0,0[0,1,1,2,6]-> f(g(f(f(x)),f(f(g(x,f(x)))))) -1|
                                                            0,0,0[0,1,1,0,4]-> 
                                                            f(g(f(g(x,f(x))),f(f(g(x,f(x))))))
           f(f(f(g(x,f(x))))) -1|0[0,1,0,0,2]-> f(g(f(g(x,f(x))),f(f(g(x,f(x))))))
          peak:
           f(f(g(f(x),f(f(x))))) <-1|0,0[0,1,1,1,4]- f(f(f(f(x)))) -0|
                                                     [1,1,0,0,0]-> f(f(f(g(x,f(x)))))
          joins:
           f(f(g(f(x),f(f(x))))) -1|0,0,1,0[0,1,1,2,6]-> f(f(g(f(x),f(g(x,f(x)))))) -1|
                                                         0,0,0[0,1,2,1,4]-> 
                                                         f(f(g(g(x,f(x)),f(g(x,f(x))))))
           f(f(f(g(x,f(x))))) -1|0,0[0,1,1,1,4]-> f(f(g(g(x,f(x)),f(g(x,f(x))))))
          peak:
           f(f(f(g(x,f(x))))) <-1|0,0,0[0,1,2,2,6]- f(f(f(f(x)))) -0|
                                                    [1,1,0,0,0]-> f(f(f(g(x,f(x)))))
          joins:
           
           
          Qed