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

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  f(0(),0()) -> f(0(),1())
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [1] = 3,
    
    [f](x0, x1) = x0 + x1 + 1,
    
    [0] = 4
   orientation:
    f(0(),0()) = 9 >= 8 = f(0(),1())
   problem:
    
   Qed