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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 8
   f(a'(),a()) <-1|0[]- f(a(),a()) -0|[]-> b()
   f(a(),a'()) <-1|1[]- f(a(),a()) -0|[]-> b()
   f(a'(),a'()) <-2|[]- f(a'(),a'()) -3|[]-> f(a'(),a'())
   f(a'(),a'()) <-2|[]- f(a'(),a'()) -4|[]-> b()
   f(a'(),a'()) <-3|[]- f(a'(),a'()) -2|[]-> f(a'(),a'())
   f(a'(),a'()) <-3|[]- f(a'(),a'()) -4|[]-> b()
   b() <-4|[]- f(a'(),a'()) -2|[]-> f(a'(),a'())
   b() <-4|[]- f(a'(),a'()) -3|[]-> f(a'(),a'())
  Shift Processor lab=left (dd) (force):
   strict:
    f(a(),a()) -> f(a'(),a())
    f(a(),a()) -> b()
    f(a'(),a()) -> f(a'(),a'())
    b() -> f(a'(),a'())
    f(a(),a()) -> f(a(),a'())
    f(a(),a()) -> b()
    f(a(),a'()) -> f(a'(),a'())
    b() -> f(a'(),a'())
    f(a'(),a'()) -> f(a'(),a'())
    f(a'(),a'()) -> f(a'(),a'())
    f(a'(),a'()) -> f(a'(),a'())
    f(a'(),a'()) -> b()
    b() -> f(a'(),a'())
    f(a'(),a'()) -> b()
    f(a'(),a'()) -> f(a'(),a'())
    f(a'(),a'()) -> f(a'(),a'())
    f(a'(),a'()) -> f(a'(),a'())
    f(a'(),a'()) -> b()
    b() -> f(a'(),a'())
    f(a'(),a'()) -> b()
    f(a'(),a'()) -> b()
    f(a'(),a'()) -> f(a'(),a'())
    f(a'(),a'()) -> b()
    b() -> f(a'(),a'())
    f(a'(),a'()) -> b()
    f(a'(),a'()) -> f(a'(),a'())
    f(a'(),a'()) -> b()
    b() -> f(a'(),a'())
   weak:
    f(a(),a()) -> b()
    a() -> a'()
    f(a'(),x) -> f(x,x)
    f(x,a'()) -> f(x,x)
    f(a'(),a'()) -> b()
    b() -> f(a'(),a'())
   Shift Processor (ldh) lab=left (force):
    strict:
     
    weak:
     
    Rule Labeling Processor:
     strict:
      
     weak:
      
     rule labeling (right):
      f(a(),a()) -> b(): 3
      a() -> a'(): 2
      f(a'(),x) -> f(x,x): 0
      f(x,a'()) -> f(x,x): 0
      f(a'(),a'()) -> b(): 0
      b() -> f(a'(),a'()): 0
     Rule Labeling Processor:
      strict:
       
      weak:
       
      rule labeling (left):
       f(a(),a()) -> b(): 0
       a() -> a'(): 0
       f(a'(),x) -> f(x,x): 1
       f(x,a'()) -> f(x,x): 2
       f(a'(),a'()) -> b(): 0
       b() -> f(a'(),a'()): 0
      Decreasing Processor:
       The following diagrams are decreasing:
       peak:
        f(a'(),a()) <-1|0[==0,==1,=>2]- f(a(),a()) -0|[==0,==1,?=3]-> b()
       joins (1):
        f(a'(),a()) -1|1[==0,==1,=>2]-> f(a'(),a'())
        b() -5|[==0,==1,>>0]-> f(a'(),a'())
       peak:
        f(a(),a'()) <-1|1[==0,==1,=>2]- f(a(),a()) -0|[==0,==1,?=3]-> b()
       joins (1):
        f(a(),a'()) -1|0[==0,==1,=>2]-> f(a'(),a'())
        b() -5|[==0,==1,>>0]-> f(a'(),a'())
       peak:
        f(a'(),a'()) <-2|[=>1,==1,==0]- f(a'(),a'()) -3|[?=2,==1,==0]-> f(a'(),a'())
       joins (1):
        
        
       peak:
        f(a'(),a'()) <-2|[=?1,==1,==0]- f(a'(),a'()) -4|[>=0,==1,==0]-> b()
       joins (1):
        
        b() -5|[>=0,==1,==0]-> f(a'(),a'())
       peak:
        f(a'(),a'()) <-3|[=?2,==1,==0]- f(a'(),a'()) -2|[>=1,==1,==0]-> f(a'(),a'())
       joins (1):
        
        
       peak:
        f(a'(),a'()) <-3|[=?2,==1,==0]- f(a'(),a'()) -4|[>=0,==1,==0]-> b()
       joins (1):
        
        b() -5|[>=0,==1,==0]-> f(a'(),a'())
       peak:
        b() <-4|[=>0,==1,==0]- f(a'(),a'()) -2|[?=1,==1,==0]-> f(a'(),a'())
       joins (1):
        
        f(a'(),a'()) -4|[=>0,==1,==0]-> b()
       peak:
        b() <-4|[=>0,==1,==0]- f(a'(),a'()) -3|[?=2,==1,==0]-> f(a'(),a'())
       joins (1):
        
        f(a'(),a'()) -4|[=>0,==1,==0]-> b()
       Qed