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:
      [G](x0) = 4x0,
      
      [H](x0) = 4x0 + 1,
      
      [I](x0) = 2x0
     orientation:
      G(I(x31)) = 8x31 >= 2x31 = I(x31)
      
      G(H(x32)) = 16x32 + 4 >= 4x32 + 1 = H(x32)
     problem:
      G(I(x31)) -> I(x31)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [G](x0) = x0 + 1,
       
       [I](x0) = x0 + 4
      orientation:
       G(I(x31)) = x31 + 5 >= x31 + 4 = I(x31)
      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:
      [B](x0) = x0 + 1,
      
      [I](x0) = 4x0 + 4,
      
      [W](x0) = 2x0 + 5
     orientation:
      W(W(x56)) = 4x56 + 15 >= 2x56 + 5 = W(x56)
      
      B(I(x57)) = 4x57 + 5 >= 2x57 + 5 = W(x57)
     problem:
      B(I(x57)) -> W(x57)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [B](x0) = 4x0 + 1,
       
       [I](x0) = x0 + 2,
       
       [W](x0) = 4x0
      orientation:
       B(I(x57)) = 4x57 + 9 >= 4x57 = W(x57)
      problem:
       
      Qed