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

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   I(x) -> x
   F(x,G(y)) -> F(I(x),G(y))
   F(H(x),y) -> F(H(x),I(I(y)))
  weak:
   
  critical peaks: 2
   F(I(H(x)),G(x28)) <-1|[]- F(H(x),G(x28)) -2|[]-> F(H(x),I(I(G(x28))))
   F(H(x29),I(I(G(y)))) <-2|[]- F(H(x29),G(y)) -1|[]-> F(I(H(x29)),G(y))
  Closedness Processor (*strongly -- <=7 steps*):
   
   Qed