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()
 f(h(k1(a()),k2(b()))) -> f(h(c(),d()))
 f(h(c(),k2(b()))) -> f(h(c(),d()))
 f(h(k1(a()),d())) -> f(h(c(),d()))

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  f(h(k1(a()),k2(b()))) -> f(h(c(),d()))
  f(h(c(),k2(b()))) -> f(h(c(),d()))
  f(h(k1(a()),d())) -> f(h(c(),d()))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [k2](x0) = x0,
    
    [k1](x0) = 2x0,
    
    [h](x0, x1) = x0 + 4x1,
    
    [d] = 0,
    
    [c] = 0,
    
    [f](x0) = 2x0,
    
    [b] = 1,
    
    [a] = 0
   orientation:
    f(h(k1(a()),k2(b()))) = 8 >= 0 = f(h(c(),d()))
    
    f(h(c(),k2(b()))) = 8 >= 0 = f(h(c(),d()))
    
    f(h(k1(a()),d())) = 0 >= 0 = f(h(c(),d()))
   problem:
    f(h(k1(a()),d())) -> f(h(c(),d()))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [k1](x0) = x0 + 4,
     
     [h](x0, x1) = x0 + x1 + 1,
     
     [d] = 6,
     
     [c] = 1,
     
     [f](x0) = x0 + 4,
     
     [a] = 0
    orientation:
     f(h(k1(a()),d())) = 15 >= 12 = f(h(c(),d()))
    problem:
     
    Qed