YES

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

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