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

Proof:
 Church Rosser Transformation Processor (kb):
  f(g(x),g(x)) -> f(x,h(x,g(c())))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [h](x0, x1) = x0 + x1 + 1,
    
    [c] = 0,
    
    [f](x0, x1) = 2x0 + x1 + 4,
    
    [g](x0) = x0 + 1
   orientation:
    f(g(x),g(x)) = 3x + 7 >= 3x + 6 = f(x,h(x,g(c())))
   problem:
    
   Qed