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

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