Problem:
 W(B(x)) -> W(x)
 B(I(x)) -> J(x)
 W(I(x)) -> W(J(x))

Proof:
 Church Rosser Transformation Processor (kb):
  W(B(x)) -> W(x)
  B(I(x)) -> J(x)
  W(I(x)) -> W(J(x))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=3
   
   interpretation:
              [1 0 0]     [0]
    [J](x0) = [0 0 0]x0 + [1]
              [0 0 0]     [0],
    
              [1 0 0]     [1]
    [I](x0) = [0 0 0]x0 + [0]
              [0 0 0]     [0],
    
              [1 1 0]     [0]
    [W](x0) = [0 0 0]x0 + [0]
              [0 0 0]     [1],
    
              [1 1 0]     [0]
    [B](x0) = [0 0 0]x0 + [1]
              [0 0 0]     [0]
   orientation:
              [1 1 0]    [1]    [1 1 0]    [0]       
    W(B(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = W(x)
              [0 0 0]    [1]    [0 0 0]    [1]       
    
              [1 0 0]    [1]    [1 0 0]    [0]       
    B(I(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = J(x)
              [0 0 0]    [0]    [0 0 0]    [0]       
    
              [1 0 0]    [1]    [1 0 0]    [1]          
    W(I(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = W(J(x))
              [0 0 0]    [1]    [0 0 0]    [1]          
   problem:
    W(I(x)) -> W(J(x))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [J](x0) = x0 + 2,
     
     [I](x0) = x0 + 5,
     
     [W](x0) = x0 + 6
    orientation:
     W(I(x)) = x + 11 >= x + 8 = W(J(x))
    problem:
     
    Qed