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

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   h(0)(x) -> g(0)(x)
   g(0)(x) -> h(0)(x)
   f(0)(x) -> f(1)(x)
   f(1)(y) -> f(0)(y)
   f(0)(h(0)(x)) -> f(1)(x)
   f(1)(h(0)(y)) -> f(0)(y)
   f(0)(g(0)(x)) -> f(0)(x)
   f(1)(h(0)(y)) -> f(1)(y)
   f(0)(h(0)(x)) -> f(0)(g(0)(x))
   f(1)(g(0)(y)) -> f(1)(g(0)(y))
   f(0)(g(0)(x)) -> f(0)(g(0)(x))
   f(1)(g(0)(y)) -> f(1)(h(0)(y))
  critical peaks: 16
  f(g(x182),h(x183)) <-0|[]- f(g(x182),g(x183)) -4|[]-> f(g(x183),g(x182))
  f(g(x184),g(x185)) <-1|[]- f(h(x184),g(x185)) -4|[]-> f(g(x185),h(x184))
  f(x186,x187) <-2|[]- f(g(x186),h(x187)) -4|[]-> f(h(x187),g(x186))
  f(x189,x188) <-3|[]- f(h(x188),h(x189)) -4|[]-> f(h(x189),h(x188))
  f(g(y),g(x)) <-4|[]- f(g(x),g(y)) -0|[]-> f(g(x),h(y))
  f(g(y),h(x)) <-4|[]- f(h(x),g(y)) -1|[]-> f(g(x),g(y))
  f(h(y),g(x)) <-4|[]- f(g(x),h(y)) -2|[]-> f(x,y)
  f(h(y),h(x)) <-4|[]- f(h(x),h(y)) -3|[]-> f(y,x)
  f(h(x),g(y)) <-5|0[]- f(g(x),g(y)) -0|[]-> f(g(x),h(y))
  f(g(x),h(y)) <-5|1[]- f(g(x),g(y)) -0|[]-> f(g(x),h(y))
  f(h(x),h(y)) <-5|1[]- f(h(x),g(y)) -1|[]-> f(g(x),g(y))
  f(h(x),h(y)) <-5|0[]- f(g(x),h(y)) -2|[]-> f(x,y)
  f(g(x),g(y)) <-6|0[]- f(h(x),g(y)) -1|[]-> f(g(x),g(y))
  f(g(x),g(y)) <-6|1[]- f(g(x),h(y)) -2|[]-> f(x,y)
  f(g(x),h(y)) <-6|0[]- f(h(x),h(y)) -3|[]-> f(y,x)
  f(h(x),g(y)) <-6|1[]- f(h(x),h(y)) -3|[]-> f(y,x)
  Matrix Interpretation Processor: dim=1, lab=right
   
   interpretation:
    [f(1)](x0) = x0,
    
    [f(0)](x0) = x0,
    
    [g(0)](x0) = 2x0 + 2,
    
    [h(0)](x0) = 2x0 + 2
   orientation:
    h(0)(x) = 2x + 2 >= 2x + 2 = g(0)(x)
    
    g(0)(x) = 2x + 2 >= 2x + 2 = h(0)(x)
    
    f(0)(x) = x >= x = f(1)(x)
    
    f(1)(y) = y >= y = f(0)(y)
    
    f(0)(h(0)(x)) = 2x + 2 >= x = f(1)(x)
    
    f(1)(h(0)(y)) = 2y + 2 >= y = f(0)(y)
    
    f(0)(g(0)(x)) = 2x + 2 >= x = f(0)(x)
    
    f(1)(h(0)(y)) = 2y + 2 >= y = f(1)(y)
    
    f(0)(h(0)(x)) = 2x + 2 >= 2x + 2 = f(0)(g(0)(x))
    
    f(1)(g(0)(y)) = 2y + 2 >= 2y + 2 = f(1)(g(0)(y))
    
    f(0)(g(0)(x)) = 2x + 2 >= 2x + 2 = f(0)(g(0)(x))
    
    f(1)(g(0)(y)) = 2y + 2 >= 2y + 2 = f(1)(h(0)(y))
   problem:
    
    strict:
     
    weak:
     h(0)(x) -> g(0)(x)
     g(0)(x) -> h(0)(x)
     f(0)(x) -> f(1)(x)
     f(1)(y) -> f(0)(y)
     f(0)(h(0)(x)) -> f(0)(g(0)(x))
     f(1)(g(0)(y)) -> f(1)(g(0)(y))
     f(0)(g(0)(x)) -> f(0)(g(0)(x))
     f(1)(g(0)(y)) -> f(1)(h(0)(y))
   Shift Processor lab=left (dd):
    
    strict:
     f(g(x182),g(x183)) -> f(g(x182),h(x183))
     f(g(x182),g(x183)) -> f(g(x183),g(x182))
     f(g(x182),h(x183)) -> f(h(x183),g(x182))
     f(g(x183),g(x182)) -> f(h(x183),g(x182))
     f(g(x182),h(x183)) -> f(g(x182),g(x183))
     f(g(x183),g(x182)) -> f(g(x182),g(x183))
     f(h(x184),g(x185)) -> f(g(x184),g(x185))
     f(h(x184),g(x185)) -> f(g(x185),h(x184))
     f(g(x184),g(x185)) -> f(g(x185),g(x184))
     f(g(x185),h(x184)) -> f(g(x185),g(x184))
     f(g(x184),g(x185)) -> f(h(x184),g(x185))
     f(g(x185),h(x184)) -> f(h(x184),g(x185))
     f(g(x186),h(x187)) -> f(x186,x187)
     f(g(x186),h(x187)) -> f(h(x187),g(x186))
     f(h(x187),g(x186)) -> f(g(x186),h(x187))
     f(g(x186),h(x187)) -> f(x186,x187)
     f(h(x187),g(x186)) -> f(h(x187),h(x186))
     f(h(x187),h(x186)) -> f(x186,x187)
     f(h(x188),h(x189)) -> f(x189,x188)
     f(h(x188),h(x189)) -> f(h(x189),h(x188))
     f(x189,x188) -> f(x188,x189)
     f(h(x189),h(x188)) -> f(x188,x189)
     f(g(x),g(y)) -> f(g(y),g(x))
     f(g(x),g(y)) -> f(g(x),h(y))
     f(g(y),g(x)) -> f(g(x),g(y))
     f(g(x),h(y)) -> f(g(x),g(y))
     f(g(y),g(x)) -> f(h(y),g(x))
     f(g(x),h(y)) -> f(h(y),g(x))
     f(h(x),g(y)) -> f(g(y),h(x))
     f(h(x),g(y)) -> f(g(x),g(y))
     f(g(y),h(x)) -> f(h(x),g(y))
     f(g(x),g(y)) -> f(h(x),g(y))
     f(g(y),h(x)) -> f(g(y),g(x))
     f(g(x),g(y)) -> f(g(y),g(x))
     f(g(x),h(y)) -> f(h(y),g(x))
     f(g(x),h(y)) -> f(x,y)
     f(h(y),g(x)) -> f(g(x),h(y))
     f(g(x),h(y)) -> f(x,y)
     f(h(y),g(x)) -> f(h(y),h(x))
     f(h(y),h(x)) -> f(x,y)
     f(h(x),h(y)) -> f(h(y),h(x))
     f(h(x),h(y)) -> f(y,x)
     f(h(y),h(x)) -> f(x,y)
     f(y,x) -> f(x,y)
     f(g(x),g(y)) -> f(h(x),g(y))
     f(g(x),g(y)) -> f(g(x),h(y))
     f(h(x),g(y)) -> f(g(x),g(y))
     f(g(x),h(y)) -> f(g(x),g(y))
     f(h(x),g(y)) -> f(h(x),h(y))
     f(g(x),h(y)) -> f(h(x),h(y))
     f(g(x),g(y)) -> f(g(x),h(y))
     f(g(x),g(y)) -> f(g(x),h(y))
     f(h(x),g(y)) -> f(h(x),h(y))
     f(h(x),g(y)) -> f(g(x),g(y))
     f(h(x),h(y)) -> f(h(x),g(y))
     f(g(x),g(y)) -> f(h(x),g(y))
     f(h(x),h(y)) -> f(g(x),h(y))
     f(g(x),g(y)) -> f(g(x),h(y))
     f(g(x),h(y)) -> f(h(x),h(y))
     f(g(x),h(y)) -> f(x,y)
     f(h(x),h(y)) -> f(y,x)
     f(x,y) -> f(y,x)
     f(h(x),g(y)) -> f(g(x),g(y))
     f(h(x),g(y)) -> f(g(x),g(y))
     f(g(x),h(y)) -> f(g(x),g(y))
     f(g(x),h(y)) -> f(x,y)
     f(g(x),g(y)) -> f(g(x),h(y))
     f(g(x),h(y)) -> f(x,y)
     f(h(x),h(y)) -> f(g(x),h(y))
     f(h(x),h(y)) -> f(y,x)
     f(g(x),h(y)) -> f(x,y)
     f(y,x) -> f(x,y)
     f(h(x),h(y)) -> f(h(x),g(y))
     f(h(x),h(y)) -> f(y,x)
     f(h(x),g(y)) -> f(g(y),h(x))
     f(g(y),h(x)) -> f(y,x)
     f(h(x),g(y)) -> f(h(x),h(y))
     f(h(x),h(y)) -> f(y,x)
    weak:
     f(g(x),g(y)) -> f(g(x),h(y))
     f(h(x),g(y)) -> f(g(x),g(y))
     f(g(x),h(y)) -> f(x,y)
     f(h(x),h(y)) -> f(y,x)
     f(x,y) -> f(y,x)
     g(x) -> h(x)
     h(x) -> g(x)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [h](x0) = 2x0 + 1,
      
      [f](x0, x1) = 4x0 + 4x1,
      
      [g](x0) = 2x0 + 1
     orientation:
      f(g(x182),g(x183)) = 8x182 + 8x183 + 8 >= 8x182 + 8x183 + 8 = f(g(x182),h(x183))
      
      f(g(x182),g(x183)) = 8x182 + 8x183 + 8 >= 8x182 + 8x183 + 8 = f(g(x183),g(x182))
      
      f(g(x182),h(x183)) = 8x182 + 8x183 + 8 >= 8x182 + 8x183 + 8 = f(h(x183),g(x182))
      
      f(g(x183),g(x182)) = 8x182 + 8x183 + 8 >= 8x182 + 8x183 + 8 = f(h(x183),g(x182))
      
      f(g(x182),h(x183)) = 8x182 + 8x183 + 8 >= 8x182 + 8x183 + 8 = f(g(x182),g(x183))
      
      f(g(x183),g(x182)) = 8x182 + 8x183 + 8 >= 8x182 + 8x183 + 8 = f(g(x182),g(x183))
      
      f(h(x184),g(x185)) = 8x184 + 8x185 + 8 >= 8x184 + 8x185 + 8 = f(g(x184),g(x185))
      
      f(h(x184),g(x185)) = 8x184 + 8x185 + 8 >= 8x184 + 8x185 + 8 = f(g(x185),h(x184))
      
      f(g(x184),g(x185)) = 8x184 + 8x185 + 8 >= 8x184 + 8x185 + 8 = f(g(x185),g(x184))
      
      f(g(x185),h(x184)) = 8x184 + 8x185 + 8 >= 8x184 + 8x185 + 8 = f(g(x185),g(x184))
      
      f(g(x184),g(x185)) = 8x184 + 8x185 + 8 >= 8x184 + 8x185 + 8 = f(h(x184),g(x185))
      
      f(g(x185),h(x184)) = 8x184 + 8x185 + 8 >= 8x184 + 8x185 + 8 = f(h(x184),g(x185))
      
      f(g(x186),h(x187)) = 8x186 + 8x187 + 8 >= 4x186 + 4x187 = f(x186,x187)
      
      f(g(x186),h(x187)) = 8x186 + 8x187 + 8 >= 8x186 + 8x187 + 8 = f(h(x187),g(x186))
      
      f(h(x187),g(x186)) = 8x186 + 8x187 + 8 >= 8x186 + 8x187 + 8 = f(g(x186),h(x187))
      
      f(g(x186),h(x187)) = 8x186 + 8x187 + 8 >= 4x186 + 4x187 = f(x186,x187)
      
      f(h(x187),g(x186)) = 8x186 + 8x187 + 8 >= 8x186 + 8x187 + 8 = f(h(x187),h(x186))
      
      f(h(x187),h(x186)) = 8x186 + 8x187 + 8 >= 4x186 + 4x187 = f(x186,x187)
      
      f(h(x188),h(x189)) = 8x188 + 8x189 + 8 >= 4x188 + 4x189 = f(x189,x188)
      
      f(h(x188),h(x189)) = 8x188 + 8x189 + 8 >= 8x188 + 8x189 + 8 = f(h(x189),h(x188))
      
      f(x189,x188) = 4x188 + 4x189 >= 4x188 + 4x189 = f(x188,x189)
      
      f(h(x189),h(x188)) = 8x188 + 8x189 + 8 >= 4x188 + 4x189 = f(x188,x189)
      
      f(g(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(y),g(x))
      
      f(g(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),h(y))
      
      f(g(y),g(x)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),g(y))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),g(y))
      
      f(g(y),g(x)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(y),g(x))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(y),g(x))
      
      f(h(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(y),h(x))
      
      f(h(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),g(y))
      
      f(g(y),h(x)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(x),g(y))
      
      f(g(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(x),g(y))
      
      f(g(y),h(x)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(y),g(x))
      
      f(g(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(y),g(x))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(y),g(x))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 4x + 4y = f(x,y)
      
      f(h(y),g(x)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),h(y))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 4x + 4y = f(x,y)
      
      f(h(y),g(x)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(y),h(x))
      
      f(h(y),h(x)) = 8x + 8y + 8 >= 4x + 4y = f(x,y)
      
      f(h(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(y),h(x))
      
      f(h(x),h(y)) = 8x + 8y + 8 >= 4x + 4y = f(y,x)
      
      f(h(y),h(x)) = 8x + 8y + 8 >= 4x + 4y = f(x,y)
      
      f(y,x) = 4x + 4y >= 4x + 4y = f(x,y)
      
      f(g(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(x),g(y))
      
      f(g(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),h(y))
      
      f(h(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),g(y))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),g(y))
      
      f(h(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(x),h(y))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(x),h(y))
      
      f(g(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),h(y))
      
      f(g(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),h(y))
      
      f(h(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(x),h(y))
      
      f(h(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),g(y))
      
      f(h(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(x),g(y))
      
      f(g(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(x),g(y))
      
      f(h(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),h(y))
      
      f(g(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),h(y))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(x),h(y))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 4x + 4y = f(x,y)
      
      f(h(x),h(y)) = 8x + 8y + 8 >= 4x + 4y = f(y,x)
      
      f(x,y) = 4x + 4y >= 4x + 4y = f(y,x)
      
      f(h(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),g(y))
      
      f(h(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),g(y))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),g(y))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 4x + 4y = f(x,y)
      
      f(g(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),h(y))
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 4x + 4y = f(x,y)
      
      f(h(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(x),h(y))
      
      f(h(x),h(y)) = 8x + 8y + 8 >= 4x + 4y = f(y,x)
      
      f(g(x),h(y)) = 8x + 8y + 8 >= 4x + 4y = f(x,y)
      
      f(y,x) = 4x + 4y >= 4x + 4y = f(x,y)
      
      f(h(x),h(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(x),g(y))
      
      f(h(x),h(y)) = 8x + 8y + 8 >= 4x + 4y = f(y,x)
      
      f(h(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(g(y),h(x))
      
      f(g(y),h(x)) = 8x + 8y + 8 >= 4x + 4y = f(y,x)
      
      f(h(x),g(y)) = 8x + 8y + 8 >= 8x + 8y + 8 = f(h(x),h(y))
      
      f(h(x),h(y)) = 8x + 8y + 8 >= 4x + 4y = f(y,x)
      
      g(x) = 2x + 1 >= 2x + 1 = h(x)
      
      h(x) = 2x + 1 >= 2x + 1 = g(x)
     problem:
      
      strict:
       f(g(x182),g(x183)) -> f(g(x182),h(x183))
       f(g(x182),g(x183)) -> f(g(x183),g(x182))
       f(g(x182),h(x183)) -> f(h(x183),g(x182))
       f(g(x183),g(x182)) -> f(h(x183),g(x182))
       f(g(x182),h(x183)) -> f(g(x182),g(x183))
       f(g(x183),g(x182)) -> f(g(x182),g(x183))
       f(h(x184),g(x185)) -> f(g(x184),g(x185))
       f(h(x184),g(x185)) -> f(g(x185),h(x184))
       f(g(x184),g(x185)) -> f(g(x185),g(x184))
       f(g(x185),h(x184)) -> f(g(x185),g(x184))
       f(g(x184),g(x185)) -> f(h(x184),g(x185))
       f(g(x185),h(x184)) -> f(h(x184),g(x185))
       f(g(x186),h(x187)) -> f(h(x187),g(x186))
       f(h(x187),g(x186)) -> f(g(x186),h(x187))
       f(h(x187),g(x186)) -> f(h(x187),h(x186))
       f(h(x188),h(x189)) -> f(h(x189),h(x188))
       f(x189,x188) -> f(x188,x189)
       f(g(x),g(y)) -> f(g(y),g(x))
       f(g(x),g(y)) -> f(g(x),h(y))
       f(g(y),g(x)) -> f(g(x),g(y))
       f(g(x),h(y)) -> f(g(x),g(y))
       f(g(y),g(x)) -> f(h(y),g(x))
       f(g(x),h(y)) -> f(h(y),g(x))
       f(h(x),g(y)) -> f(g(y),h(x))
       f(h(x),g(y)) -> f(g(x),g(y))
       f(g(y),h(x)) -> f(h(x),g(y))
       f(g(x),g(y)) -> f(h(x),g(y))
       f(g(y),h(x)) -> f(g(y),g(x))
       f(g(x),g(y)) -> f(g(y),g(x))
       f(g(x),h(y)) -> f(h(y),g(x))
       f(h(y),g(x)) -> f(g(x),h(y))
       f(h(y),g(x)) -> f(h(y),h(x))
       f(h(x),h(y)) -> f(h(y),h(x))
       f(y,x) -> f(x,y)
       f(g(x),g(y)) -> f(h(x),g(y))
       f(g(x),g(y)) -> f(g(x),h(y))
       f(h(x),g(y)) -> f(g(x),g(y))
       f(g(x),h(y)) -> f(g(x),g(y))
       f(h(x),g(y)) -> f(h(x),h(y))
       f(g(x),h(y)) -> f(h(x),h(y))
       f(g(x),g(y)) -> f(g(x),h(y))
       f(g(x),g(y)) -> f(g(x),h(y))
       f(h(x),g(y)) -> f(h(x),h(y))
       f(h(x),g(y)) -> f(g(x),g(y))
       f(h(x),h(y)) -> f(h(x),g(y))
       f(g(x),g(y)) -> f(h(x),g(y))
       f(h(x),h(y)) -> f(g(x),h(y))
       f(g(x),g(y)) -> f(g(x),h(y))
       f(g(x),h(y)) -> f(h(x),h(y))
       f(x,y) -> f(y,x)
       f(h(x),g(y)) -> f(g(x),g(y))
       f(h(x),g(y)) -> f(g(x),g(y))
       f(g(x),h(y)) -> f(g(x),g(y))
       f(g(x),g(y)) -> f(g(x),h(y))
       f(h(x),h(y)) -> f(g(x),h(y))
       f(y,x) -> f(x,y)
       f(h(x),h(y)) -> f(h(x),g(y))
       f(h(x),g(y)) -> f(g(y),h(x))
       f(h(x),g(y)) -> f(h(x),h(y))
      weak:
       f(g(x),g(y)) -> f(g(x),h(y))
       f(h(x),g(y)) -> f(g(x),g(y))
       f(x,y) -> f(y,x)
       g(x) -> h(x)
       h(x) -> g(x)
     Shift Processor (ldh) lab=left (force):
      
      strict:
       
      weak:
       
      Rule Labeling Processor:
       
       strict:
        
       weak:
        
       rule labeling (right):
        f(g(x),g(y)) -> f(g(x),h(y)): 0
        f(h(x),g(y)) -> f(g(x),g(y)): 2
        f(g(x),h(y)) -> f(x,y): 0
        f(h(x),h(y)) -> f(y,x): 0
        f(x,y) -> f(y,x): 1
        g(x) -> h(x): 0
        h(x) -> g(x): 2
       Decreasing Processor:
        The following diagrams are decreasing:
        peak:
         f(g(x182),h(x183)) <-0|[1,0,0]- f(g(x182),g(x183)) -4|[1,0,1]-> f(g(x183),g(x182))
        joins:
         f(g(x182),h(x183)) -4|[1,0,1]-> f(h(x183),g(x182))
         f(g(x183),g(x182)) -5|0[1,0,0]-> f(h(x183),g(x182))
        peak:
         f(g(x184),g(x185)) <-1|[1,0,2]- f(h(x184),g(x185)) -4|[1,0,1]-> f(g(x185),h(x184))
        joins:
         f(g(x184),g(x185)) -4|[1,0,1]-> f(g(x185),g(x184))
         f(g(x185),h(x184)) -6|1[1,0,2]-> f(g(x185),g(x184))
        peak:
         f(x186,x187) <-2|[1,0,0]- f(g(x186),h(x187)) -4|[1,0,1]-> f(h(x187),g(x186))
        joins:
         
         f(h(x187),g(x186)) -5|1[1,0,0]-> f(h(x187),h(x186)) -3|[1,0,0]-> f(x186,x187)
        peak:
         f(x189,x188) <-3|[1,0,0]- f(h(x188),h(x189)) -4|[1,0,1]-> f(h(x189),h(x188))
        joins:
         f(x189,x188) -4|[0,0,1]-> f(x188,x189)
         f(h(x189),h(x188)) -3|[1,0,0]-> f(x188,x189)
        peak:
         f(g(y),g(x)) <-4|[1,0,1]- f(g(x),g(y)) -0|[1,0,0]-> f(g(x),h(y))
        joins:
         f(g(y),g(x)) -5|0[1,0,0]-> f(h(y),g(x))
         f(g(x),h(y)) -4|[1,0,1]-> f(h(y),g(x))
        peak:
         f(g(y),h(x)) <-4|[1,0,1]- f(h(x),g(y)) -1|[1,0,2]-> f(g(x),g(y))
        joins:
         f(g(y),h(x)) -4|[1,0,1]-> f(h(x),g(y))
         f(g(x),g(y)) -5|0[1,0,0]-> f(h(x),g(y))
        peak:
         f(h(y),g(x)) <-4|[1,0,1]- f(g(x),h(y)) -2|[1,0,0]-> f(x,y)
        joins:
         f(h(y),g(x)) -5|1[1,0,0]-> f(h(y),h(x)) -3|[1,0,0]-> f(x,y)
         
        peak:
         f(h(y),h(x)) <-4|[1,0,1]- f(h(x),h(y)) -3|[1,0,0]-> f(y,x)
        joins:
         f(h(y),h(x)) -3|[1,0,0]-> f(x,y)
         f(y,x) -4|[0,0,1]-> f(x,y)
        peak:
         f(h(x),g(y)) <-5|0[1,0,0]- f(g(x),g(y)) -0|[1,0,0]-> f(g(x),h(y))
        joins:
         f(h(x),g(y)) -5|1[1,0,0]-> f(h(x),h(y))
         f(g(x),h(y)) -5|0[1,0,0]-> f(h(x),h(y))
        peak:
         f(g(x),h(y)) <-5|1[1,0,0]- f(g(x),g(y)) -0|[1,0,0]-> f(g(x),h(y))
        joins:
         
         
        peak:
         f(h(x),h(y)) <-5|1[1,0,0]- f(h(x),g(y)) -1|[1,0,2]-> f(g(x),g(y))
        joins:
         f(h(x),h(y)) -6|1[1,0,2]-> f(h(x),g(y))
         f(g(x),g(y)) -5|0[1,0,0]-> f(h(x),g(y))
        peak:
         f(h(x),h(y)) <-5|0[1,0,0]- f(g(x),h(y)) -2|[1,0,0]-> f(x,y)
        joins:
         f(h(x),h(y)) -3|[1,0,0]-> f(y,x)
         f(x,y) -4|[0,0,1]-> f(y,x)
        peak:
         f(g(x),g(y)) <-6|0[1,0,2]- f(h(x),g(y)) -1|[1,0,2]-> f(g(x),g(y))
        joins:
         
         
        peak:
         f(g(x),g(y)) <-6|1[1,0,2]- f(g(x),h(y)) -2|[1,0,0]-> f(x,y)
        joins:
         f(g(x),g(y)) -0|[1,0,0]-> f(g(x),h(y)) -2|[1,0,0]-> f(x,y)
         
        peak:
         f(g(x),h(y)) <-6|0[1,0,2]- f(h(x),h(y)) -3|[1,0,0]-> f(y,x)
        joins:
         f(g(x),h(y)) -2|[1,0,0]-> f(x,y)
         f(y,x) -4|[0,0,1]-> f(x,y)
        peak:
         f(h(x),g(y)) <-6|1[1,0,2]- f(h(x),h(y)) -3|[1,0,0]-> f(y,x)
        joins:
         f(h(x),g(y)) -4|[1,0,1]-> f(g(y),h(x)) -2|[1,0,0]-> f(y,x)
         
        Qed