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

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