YES

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

Proof:
 sorted: (order-sorted)
 0:a() -> a()
   f(h(a(),a())) -> f(b())
 1:c() -> b()
 -----
 sorts
   [0>2, 1>3, 2>3, 2>4, 4>5, 4>6, 5>7, 6>7]
 sort attachment (non-strict)
   a : 7
   f : 2 -> 0
   h : 6 x 5 -> 4
   b : 3
   c : 1
 -----
 0:a() -> a()
   f(h(a(),a())) -> f(b())
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.4):
    f(h(a(),a())) -> f(b())
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [h](x0, x1) = x0 + x1 + 4,
      
      [b] = 1,
      
      [a] = 2,
      
      [f](x0) = x0 + 7
     orientation:
      f(h(a(),a())) = 15 >= 8 = f(b())
     problem:
      
     Qed
 
 
 1:c() -> b()
   Church Rosser Transformation Processor:
    
    critical peaks: joinable
    Qed