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:
    [c] = 0,
    
    [k2](x0) = 2x0 + 4,
    
    [b] = 4,
    
    [f](x0) = x0 + 1,
    
    [d] = 0,
    
    [a] = 0,
    
    [k1](x0) = 4x0 + 1,
    
    [h](x0, x1) = x0 + x1 + 7
   orientation:
    f(h(k1(a()),k2(b()))) = 21 >= 8 = f(h(c(),d()))
    
    f(h(c(),k2(b()))) = 20 >= 8 = f(h(c(),d()))
    
    f(h(k1(a()),d())) = 9 >= 8 = f(h(c(),d()))
   problem:
    
   Qed