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 (star):
  
  strict:
   
  weak:
   I(0)(x) -> x
   F(0)(x) -> F(0)(I(0)(x))
   F(1)(G(0)(y)) -> F(1)(G(0)(y))
   F(0)(H(0)(x)) -> F(0)(H(0)(x))
   F(1)(y) -> F(1)(I(0)(I(0)(y)))
  critical peaks: 2
  F(H(x27),I(I(G(y)))) <-0|[]- F(H(x27),G(y)) -1|[]-> F(I(H(x27)),G(y))
  F(I(H(x)),G(x30)) <-1|[]- F(H(x),G(x30)) -0|[]-> F(H(x),I(I(G(x30))))
  Shift Processor lab=left (dd):
   
   strict:
    F(H(x27),G(y)) -> F(H(x27),I(I(G(y))))
    F(H(x27),G(y)) -> F(I(H(x27)),G(y))
    F(I(H(x27)),G(y)) -> F(H(x27),G(y))
    F(H(x27),G(y)) -> F(H(x27),I(I(G(y))))
    F(H(x27),I(I(G(y)))) -> F(H(x27),I(G(y)))
    F(H(x27),I(G(y))) -> F(H(x27),G(y))
    F(I(H(x27)),G(y)) -> F(H(x27),G(y))
    F(H(x),G(x30)) -> F(I(H(x)),G(x30))
    F(H(x),G(x30)) -> F(H(x),I(I(G(x30))))
    F(I(H(x)),G(x30)) -> F(H(x),G(x30))
    F(H(x),I(I(G(x30)))) -> F(H(x),I(G(x30)))
    F(H(x),I(G(x30))) -> F(H(x),G(x30))
    F(I(H(x)),G(x30)) -> F(H(x),G(x30))
    F(H(x),G(x30)) -> F(H(x),I(I(G(x30))))
   weak:
    F(H(x),y) -> F(H(x),I(I(y)))
    F(x,G(y)) -> F(I(x),G(y))
    I(x) -> x
   Shift Processor (ldh) lab=left (force):
    
    strict:
     
    weak:
     
    Rule Labeling Processor:
     
     strict:
      
     weak:
      
     rule labeling (right):
      F(H(x),y) -> F(H(x),I(I(y))): 0
      F(x,G(y)) -> F(I(x),G(y)): 1
      I(x) -> x: 0
     Decreasing Processor:
      The following diagrams are decreasing:
      peak:
       F(H(x27),I(I(G(y)))) <-0|[1,0]- F(H(x27),G(y)) -1|[1,1]-> F(I(H(x27)),G(y))
      joins:
       
       F(I(H(x27)),G(y)) -2|0[1,0]-> F(H(x27),G(y)) -0|[1,0]-> F(H(x27),I(I(G(y))))
      peak:
       F(I(H(x)),G(x30)) <-1|[1,1]- F(H(x),G(x30)) -0|[1,0]-> F(H(x),I(I(G(x30))))
      joins:
       F(I(H(x)),G(x30)) -2|0[1,0]-> F(H(x),G(x30)) -0|[1,0]-> F(H(x),I(I(G(x30))))
       
      Qed