Problem:
 W(W(x)) -> W(x)
 B(I(x)) -> W(x)
 W(B(x)) -> B(x)
 F(H(x),y) -> F(H(x),G(y))
 F(x,I(y)) -> F(G(x),I(y))
 G(x) -> x

Proof:
 sorted: (order)
 0:F(H(x),y) -> F(H(x),G(y))
   F(x,I(y)) -> F(G(x),I(y))
   G(x) -> x
 1:W(W(x)) -> W(x)
   B(I(x)) -> W(x)
   W(B(x)) -> B(x)
 -----
 sorts
   [0>3, 1>2, 2>4, 3>4, 3>6, 4>5, 6>7]
 sort attachment (non-strict)
   W : 1 -> 1
   B : 2 -> 1
   I : 5 -> 4
   F : 3 x 3 -> 0
   H : 7 -> 6
   G : 3 -> 3
 -----
 0:F(H(x),y) -> F(H(x),G(y))
   F(x,I(y)) -> F(G(x),I(y))
   G(x) -> x
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    G(I(x31)) -> I(x31)
    G(H(x32)) -> H(x32)
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [I](x0) = 2x0,
      
      [H](x0) = 2x0,
      
      [G](x0) = 2x0 + 6
     orientation:
      G(I(x31)) = 4x31 + 6 >= 2x31 = I(x31)
      
      G(H(x32)) = 4x32 + 6 >= 2x32 = H(x32)
     problem:
      
     Qed
 
 
 1:W(W(x)) -> W(x)
   B(I(x)) -> W(x)
   W(B(x)) -> B(x)
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    W(W(x56)) -> W(x56)
    B(I(x57)) -> W(x57)
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [I](x0) = x0 + 6,
      
      [W](x0) = x0,
      
      [B](x0) = x0 + 1
     orientation:
      W(W(x56)) = x56 >= x56 = W(x56)
      
      B(I(x57)) = x57 + 7 >= x57 = W(x57)
     problem:
      W(W(x56)) -> W(x56)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [W](x0) = 2x0 + 5
      orientation:
       W(W(x56)) = 4x56 + 15 >= 2x56 + 5 = W(x56)
      problem:
       
      Qed