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

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