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:
  
  strict:
   F(G(x,A(),B())) -> x
   G(F(H(C(),D())),x,y) -> H(K1(x),K2(y))
   K1(A()) -> C()
   K2(B()) -> D()
  weak:
   
  critical peaks: 1
  F(H(K1(A()),K2(B()))) <-1|0[]- F(G(F(H(C(),D())),A(),B())) -0|[]-> F(H(C(),D()))
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed