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)(x24) -> K(0)(J(0)(x24))
   H(0)(I(0)(x25)) -> K(0)(J(0)(x25))
   J(0)(x26) -> J(0)(K(0)(J(0)(x26)))
   I(0)(x27) -> I(0)(J(0)(x27))
  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:
   strict:
    
   weak:
    
   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:
      [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:
       
      Decreasing Processor:
       The following diagrams are decreasing:
       peak:
        H(I(J(x))) <-0|0[==1]- H(I(x)) -2|[==1]-> K(J(x))
       joins (1):
        H(I(J(x))) -2|[==1]-> K(J(J(x))) -3|0,0[>>0]-> K(J(K(J(x))))
        K(J(x)) -1|0[>>0]-> K(J(K(J(x))))
       peak:
        J(K(J(x))) <-1|[==1]- J(x) -3|[==1]-> K(J(x))
       joins (1):
        J(K(J(x))) -3|[==1]-> K(J(K(J(x))))
        K(J(x)) -1|0[==1]-> K(J(K(J(x))))
       peak:
        K(J(x)) <-3|[==1]- J(x) -1|[==1]-> J(K(J(x)))
       joins (1):
        K(J(x)) -1|0[==1]-> K(J(K(J(x))))
        J(K(J(x))) -3|[==1]-> K(J(K(J(x))))
       Qed