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

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  W(I(x20)) -> W(J(x20))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [W](x0) = 4x0 + 2,
    
    [J](x0) = x0 + 1,
    
    [I](x0) = x0 + 2
   orientation:
    W(I(x20)) = 4x20 + 10 >= 4x20 + 6 = W(J(x20))
   problem:
    
   Qed