Problem:
 g(x) -> h(k(x),x)
 g(x) -> x
 h(k(x),x) -> x
 k(c()) -> c()
 h(k(c()),c()) -> g(c())
 h(c(),c()) -> c()

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 6
   h(k(x),x) <-0|[]- g(x) -1|[]-> x
   x <-1|[]- g(x) -0|[]-> h(k(x),x)
   c() <-2|[]- h(k(c()),c()) -4|[]-> g(c())
   h(c(),c()) <-3|0[]- h(k(c()),c()) -2|[]-> c()
   h(c(),c()) <-3|0[]- h(k(c()),c()) -4|[]-> g(c())
   g(c()) <-4|[]- h(k(c()),c()) -2|[]-> c()
  Redundant Rules Transformation:
   g(x) -> x
   h(k(x),x) -> x
   k(c()) -> c()
   h(c(),c()) -> c()
   Church Rosser Transformation Processor (kb):
    g(x) -> x
    h(k(x),x) -> x
    k(c()) -> c()
    h(c(),c()) -> c()
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [k](x0) = 2x0 + 1,
      
      [c] = 0,
      
      [g](x0) = 2x0 + 1,
      
      [h](x0, x1) = 6x0 + 3x1 + 6
     orientation:
      g(x) = 2x + 1 >= x = x
      
      h(k(x),x) = 15x + 12 >= x = x
      
      k(c()) = 1 >= 0 = c()
      
      h(c(),c()) = 6 >= 0 = c()
     problem:
      
     Qed