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

Proof:
 Church Rosser Transformation Processor (kb):
  H(H(x)) -> K(x)
  H(K(x)) -> K(H(x))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [K](x0) = 2x0 + 6,
    
    [H](x0) = 2x0 + 2
   orientation:
    H(H(x)) = 4x + 6 >= 2x + 6 = K(x)
    
    H(K(x)) = 4x + 14 >= 4x + 10 = K(H(x))
   problem:
    H(H(x)) -> K(x)
   Matrix Interpretation Processor: dim=3
    
    interpretation:
               [1 0 1]  
     [K](x0) = [0 0 0]x0
               [0 0 0]  ,
     
               [1 0 1]     [0]
     [H](x0) = [0 0 0]x0 + [0]
               [0 0 0]     [1]
    orientation:
               [1 0 1]    [1]    [1 0 1]        
     H(H(x)) = [0 0 0]x + [0] >= [0 0 0]x = K(x)
               [0 0 0]    [1]    [0 0 0]        
    problem:
     
    Qed