Problem:
 I(x) -> I(J(x))
 J(x) -> J(K(J(x)))
 H(I(x)) -> K(J(x))
 J(x) -> K(J(x))

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