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

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   g(0)(x) -> x
   f(1)(x) -> f(1)(g(0)(x))
  critical peaks: 1
  f(b(),x) <-1|0[]- f(a(),x) -0|[]-> f(a(),g(x))
  Shift Processor lab=left (dd):
   
   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:
     [b] = 0,
     
     [g](x0) = x0,
     
     [f](x0, x1) = x0 + 4x1,
     
     [a] = 1
    orientation:
     f(a(),x) = 4x + 1 >= 4x = f(b(),x)
     
     f(a(),x) = 4x + 1 >= 4x + 1 = f(a(),g(x))
     
     f(a(),g(x)) = 4x + 1 >= 4x = f(b(),g(x))
     
     f(b(),g(x)) = 4x >= 4x = f(b(),x)
     
     f(a(),g(x)) = 4x + 1 >= 4x + 1 = f(a(),x)
     
     f(a(),x) = 4x + 1 >= 4x = 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:
      
     Decreasing Processor:
      The following diagrams are decreasing:
      peak:
       f(b(),x) <-1|0[1]- f(a(),x) -0|[1]-> f(a(),g(x))
      joins:
       
       f(a(),g(x)) -1|0[1]-> f(b(),g(x)) -2|1[0]-> f(b(),x)
      Qed