YES

Problem:
 g(a()) -> f(g(a()))
 g(b()) -> c(a())
 a() -> b()
 f(x) -> h(x)
 h(x) -> c(b())

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 1
   g(b()) <-2|0[]- g(a()) -0|[]-> f(g(a()))
  Shift Processor lab=left (dd) (force):
   strict:
    g(a()) -> g(b())
    g(a()) -> f(g(a()))
    g(b()) -> c(a())
    c(a()) -> c(b())
    f(g(a())) -> h(g(a()))
    h(g(a())) -> c(b())
   weak:
    g(a()) -> f(g(a()))
    g(b()) -> c(a())
    a() -> b()
    f(x) -> h(x)
    h(x) -> c(b())
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [c](x0) = 2x0,
     
     [g](x0) = x0 + 1,
     
     [b] = 0,
     
     [h](x0) = x0,
     
     [a] = 0,
     
     [f](x0) = x0
    orientation:
     g(a()) = 1 >= 1 = g(b())
     
     g(a()) = 1 >= 1 = f(g(a()))
     
     g(b()) = 1 >= 0 = c(a())
     
     c(a()) = 0 >= 0 = c(b())
     
     f(g(a())) = 1 >= 1 = h(g(a()))
     
     h(g(a())) = 1 >= 0 = c(b())
     
     a() = 0 >= 0 = b()
     
     f(x) = x >= x = h(x)
     
     h(x) = x >= 0 = c(b())
    problem:
     strict:
      g(a()) -> g(b())
      g(a()) -> f(g(a()))
      c(a()) -> c(b())
      f(g(a())) -> h(g(a()))
     weak:
      g(a()) -> f(g(a()))
      a() -> b()
      f(x) -> h(x)
      h(x) -> c(b())
    Polynomial Interpretation Processor:
     dimension: 1
     interpretation:
      [c](x0) = 2x0,
      
      [g](x0) = x0,
      
      [b] = 0,
      
      [h](x0) = x0,
      
      [a] = 2,
      
      [f](x0) = x0
     orientation:
      g(a()) = 2 >= 0 = g(b())
      
      g(a()) = 2 >= 2 = f(g(a()))
      
      c(a()) = 4 >= 0 = c(b())
      
      f(g(a())) = 2 >= 2 = h(g(a()))
      
      a() = 2 >= 0 = b()
      
      f(x) = x >= x = h(x)
      
      h(x) = x >= 0 = c(b())
     problem:
      strict:
       g(a()) -> f(g(a()))
       f(g(a())) -> h(g(a()))
      weak:
       g(a()) -> f(g(a()))
       f(x) -> h(x)
       h(x) -> c(b())
     Shift Processor (ldh) lab=left (force):
      strict:
       
      weak:
       
      Rule Labeling Processor:
       strict:
        
       weak:
        
       rule labeling (right):
        g(a()) -> f(g(a())): 1
        g(b()) -> c(a()): 0
        a() -> b(): 1
        f(x) -> h(x): 0
        h(x) -> c(b()): 0
       Rule Labeling Processor:
        strict:
         
        weak:
         
        rule labeling (left):
         g(a()) -> f(g(a())): 0
         g(b()) -> c(a()): 0
         a() -> b(): 0
         f(x) -> h(x): 0
         h(x) -> c(b()): 0
        Decreasing Processor:
         The following diagrams are decreasing:
         peak:
          g(b()) <-2|0[==0,==1,==1]- g(a()) -0|[==0,==1,==1]-> f(g(a()))
         joins (1):
          g(b()) -1|[==0,>>0,>>0]-> c(a()) -2|0[==0,>>0,==1]-> c(b())
          f(g(a())) -3|[==0,==1,>>0]-> h(g(a())) -4|[==0,==1,>>0]-> c(b())
         Qed