Problem:
 c() -> c()
 h(a(),h(f(b()),c())) -> c()

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