Problem:
 f(0(),0()) -> f(0(),1())
 f(1(),0()) -> f(0(),0())
 f(x,y) -> f(y,x)

Proof:
 Church Rosser Transformation Processor:
  
  strict:
   
  weak:
   
  critical peaks: 4
  f(0(),1()) <-0|[]- f(0(),0()) -2|[]-> f(0(),0())
  f(0(),0()) <-1|[]- f(1(),0()) -2|[]-> f(0(),1())
  f(0(),0()) <-2|[]- f(0(),0()) -0|[]-> f(0(),1())
  f(0(),1()) <-2|[]- f(1(),0()) -1|[]-> f(0(),0())
  Closedness Processor (*parallel*):
   
   strict:
    
   weak:
    
   Qed