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 (star):
  
  strict:
   
  weak:
   f(0)(x) -> h(0)(x)
  critical peaks: 1
  g(b()) <-2|0[]- g(a()) -0|[]-> f(g(a()))
  Matrix Interpretation Processor: dim=1, lab=right
   
   interpretation:
    [h(0)](x0) = 2x0,
    
    [f(0)](x0) = 2x0 + 1
   orientation:
    f(0)(x) = 2x + 1 >= 2x = h(0)(x)
   problem:
    
    strict:
     
    weak:
     
   Shift Processor lab=left (dd):
    
    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())
    Polynomial Interpretation Processor:
     dimension: 1
     interpretation:
      [h](x0) = x0,
      
      [c](x0) = x0x0,
      
      [b] = 0,
      
      [f](x0) = x0,
      
      [g](x0) = x0 + 1,
      
      [a] = 1
     orientation:
      g(a()) = 2 >= 1 = g(b())
      
      g(a()) = 2 >= 2 = f(g(a()))
      
      g(b()) = 1 >= 1 = c(a())
      
      c(a()) = 1 >= 0 = c(b())
      
      f(g(a())) = 2 >= 2 = h(g(a()))
      
      h(g(a())) = 2 >= 0 = c(b())
      
      a() = 1 >= 0 = b()
      
      f(x) = x >= x = h(x)
      
      h(x) = x >= 0 = c(b())
     problem:
      
      strict:
       g(a()) -> f(g(a()))
       g(b()) -> c(a())
       f(g(a())) -> h(g(a()))
      weak:
       g(a()) -> f(g(a()))
       g(b()) -> c(a())
       f(x) -> h(x)
       h(x) -> c(b())
     Polynomial Interpretation Processor:
      dimension: 1
      interpretation:
       [h](x0) = x0,
       
       [c](x0) = x0,
       
       [b] = 0,
       
       [f](x0) = x0,
       
       [g](x0) = x0x0 + 2,
       
       [a] = 0
      orientation:
       g(a()) = 2 >= 2 = f(g(a()))
       
       g(b()) = 2 >= 0 = c(a())
       
       f(g(a())) = 2 >= 2 = h(g(a()))
       
       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(): 0
         f(x) -> h(x): 0
         h(x) -> c(b()): 0
        Decreasing Processor:
         The following diagrams are decreasing:
         peak:
          g(b()) <-2|0[1,0,0]- g(a()) -0|[1,0,1]-> f(g(a()))
         joins:
          g(b()) -1|[0,0,0]-> c(a()) -2|0[0,0,0]-> c(b())
          f(g(a())) -3|[1,0,0]-> h(g(a())) -4|[1,0,0]-> c(b())
         Qed