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:
    [J](x0) = x0 + 1,
    
    [I](x0) = x0 + 4,
    
    [W](x0) = x0 + 7
   orientation:
    W(I(x20)) = x20 + 11 >= x20 + 8 = W(J(x20))
   problem:
    
   Qed