YES

Problem:
 F(G(x,A(),B())) -> x
 G(F(H(C(),D())),x,y) -> H(K1(x),K2(y))
 K1(A()) -> C()
 K2(B()) -> D()

Proof:
 Church Rosser Transformation Processor (kb):
  F(G(x,A(),B())) -> x
  G(F(H(C(),D())),x,y) -> H(K1(x),K2(y))
  K1(A()) -> C()
  K2(B()) -> D()
  critical peaks: joinable
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [C] = 4,
     
     [K2](x0) = 3x0 + 1,
     
     [B] = 6,
     
     [F](x0) = x0,
     
     [D] = 0,
     
     [A] = 4,
     
     [K1](x0) = x0,
     
     [H](x0, x1) = 2x0 + x1,
     
     [G](x0, x1, x2) = x0 + 2x1 + 3x2 + 4
    orientation:
     F(G(x,A(),B())) = x + 30 >= x = x
     
     G(F(H(C(),D())),x,y) = 2x + 3y + 12 >= 2x + 3y + 1 = H(K1(x),K2(y))
     
     K1(A()) = 4 >= 4 = C()
     
     K2(B()) = 19 >= 0 = D()
    problem:
     K1(A()) -> C()
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [C] = 0,
      
      [A] = 2,
      
      [K1](x0) = x0 + 7
     orientation:
      K1(A()) = 9 >= 0 = C()
     problem:
      
     Qed