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

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