Problem:
 H(F(x,y)) -> F(H(R(x)),y)
 F(x,K(y,z)) -> G(P(y),Q(z,x))
 H(Q(x,y)) -> Q(x,H(R(y)))
 Q(x,H(R(y))) -> H(Q(x,y))
 H(G(x,y)) -> G(x,H(y))

Proof:
 AT confluence processor
  Complete TRS T' of input TRS:
  H(F(x,y)) -> F(H(R(x)),y)
  F(x,K(y,z)) -> G(P(y),Q(z,x))
  H(G(x,y)) -> G(x,H(y))
  H(Q(x,y)) -> Q(x,H(R(y)))
  Q(x,H(R(y))) -> H(Q(x,y))
  
   T' = (P union S) with
  
   TRS P:H(Q(x,y)) -> Q(x,H(R(y)))
         Q(x,H(R(y))) -> H(Q(x,y))
  
   TRS S:H(F(x,y)) -> F(H(R(x)),y)
         F(x,K(y,z)) -> G(P(y),Q(z,x))
         H(G(x,y)) -> G(x,H(y))
  
  S is linear and P is reversible.
  
   CP(S,S) = 
  H(G(P(x209),Q(x210,x))) = F(H(R(x)),K(x209,x210))
  
   CP(S,P union P^-1) = 
  
   CP(P union P^-1,S) = 
  
  
  We have to check termination of S:
  
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [G](x0, x1) = x0 + 2x1 + 1,
    
    [Q](x0, x1) = 4x0 + x1,
    
    [P](x0) = x0 + 5,
    
    [K](x0, x1) = x0 + 4x1 + 2,
    
    [R](x0) = x0,
    
    [H](x0) = 4x0 + 3,
    
    [F](x0, x1) = 4x0 + 2x1 + 4
   orientation:
    H(F(x,y)) = 16x + 8y + 19 >= 16x + 2y + 16 = F(H(R(x)),y)
    
    F(x,K(y,z)) = 4x + 2y + 8z + 8 >= 2x + y + 8z + 6 = G(P(y),Q(z,x))
    
    H(G(x,y)) = 4x + 8y + 7 >= x + 8y + 7 = G(x,H(y))
   problem:
    H(G(x,y)) -> G(x,H(y))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [G](x0, x1) = 2x0 + 4x1 + 4,
     
     [H](x0) = 4x0 + 2
    orientation:
     H(G(x,y)) = 8x + 16y + 18 >= 2x + 16y + 12 = G(x,H(y))
    problem:
     
    Qed