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:
  strict:
   
  weak:
   
  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)))
  Shift Processor lab=left (dd) (force):
   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:
     [J](x0) = x0,
     
     [H](x0) = 4x0 + 6,
     
     [I](x0) = x0,
     
     [K](x0) = x0
    orientation:
     H(I(x)) = 4x + 6 >= 4x + 6 = H(I(J(x)))
     
     H(I(x)) = 4x + 6 >= x = K(J(x))
     
     H(I(J(x))) = 4x + 6 >= 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 + 6 >= 4x + 6 = H(I(K(J(x))))
     
     H(I(K(J(x)))) = 4x + 6 >= 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:
      
     Rule Labeling Processor:
      strict:
       
      weak:
       
      rule labeling (right):
       I(x) -> I(J(x)): 0
       J(x) -> J(K(J(x))): 0
       H(I(x)) -> K(J(x)): 0
       J(x) -> K(J(x)): 0
      Rule Labeling Processor:
       strict:
        
       weak:
        
       rule labeling (left):
        I(x) -> I(J(x)): 1
        J(x) -> J(K(J(x))): 1
        H(I(x)) -> K(J(x)): 0
        J(x) -> K(J(x)): 0
       Decreasing Processor:
        The following diagrams are decreasing:
        peak:
         H(I(J(x))) <-0|0[=?1,==1,==0]- H(I(x)) -2|[>=0,==1,==0]-> K(J(x))
        joins (1):
         H(I(J(x))) -2|[>=0,==1,==0]-> K(J(J(x))) -3|0,0[>=0,>>0,==0]-> K(J(K(J(x))))
         K(J(x)) -1|0[=?1,>>0,==0]-> K(J(K(J(x))))
        peak:
         J(K(J(x))) <-1|[=?1,==1,==0]- J(x) -3|[>=0,==1,==0]-> K(J(x))
        joins (1):
         J(K(J(x))) -3|[>=0,==1,==0]-> K(J(K(J(x))))
         K(J(x)) -1|0[=?1,==1,==0]-> K(J(K(J(x))))
        peak:
         K(J(x)) <-3|[=>0,==1,==0]- J(x) -1|[?=1,==1,==0]-> J(K(J(x)))
        joins (1):
         K(J(x)) -1|0[?=1,==1,==0]-> K(J(K(J(x))))
         J(K(J(x))) -3|[=>0,==1,==0]-> K(J(K(J(x))))
        Qed