YES

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

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