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=1
   
   interpretation:
    [J](x0) = 2x0 + 5,
    
    [I](x0) = 3x0 + 5,
    
    [W](x0) = 5x0 + 4,
    
    [B](x0) = 5x0
   orientation:
    W(B(x)) = 25x + 4 >= 5x + 4 = W(x)
    
    B(I(x)) = 15x + 25 >= 2x + 5 = J(x)
    
    W(I(x)) = 15x + 29 >= 10x + 29 = W(J(x))
   problem:
    W(B(x)) -> W(x)
    W(I(x)) -> W(J(x))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [J](x0) = x0,
     
     [I](x0) = x0 + 5,
     
     [W](x0) = x0,
     
     [B](x0) = x0
    orientation:
     W(B(x)) = x >= x = W(x)
     
     W(I(x)) = x + 5 >= x = W(J(x))
    problem:
     W(B(x)) -> W(x)
    Matrix Interpretation Processor: dim=3
     
     interpretation:
                [1 0 0]  
      [W](x0) = [0 0 0]x0
                [0 0 0]  ,
      
                [1 0 0]     [1]
      [B](x0) = [0 0 0]x0 + [0]
                [0 0 0]     [0]
     orientation:
                [1 0 0]    [1]    [1 0 0]        
      W(B(x)) = [0 0 0]x + [0] >= [0 0 0]x = W(x)
                [0 0 0]    [0]    [0 0 0]        
     problem:
      
     Qed