Problem:
 +(0(),y) -> y
 +(s(x),y) -> s(+(x,y))
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  +(0(),x62) -> x62
  +(x63,0()) -> x63
  +(x65,s(x64)) -> s(+(x65,x64))
  +(s(x67),x66) -> s(+(x67,x66))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [+](x0, x1) = 6x0 + 5x1 + 1,
    
    [0] = 0,
    
    [s](x0) = x0 + 4
   orientation:
    +(0(),x62) = 5x62 + 1 >= x62 = x62
    
    +(x63,0()) = 6x63 + 1 >= x63 = x63
    
    +(x65,s(x64)) = 5x64 + 6x65 + 21 >= 5x64 + 6x65 + 5 = s(+(x65,x64))
    
    +(s(x67),x66) = 5x66 + 6x67 + 25 >= 5x66 + 6x67 + 5 = s(+(x67,x66))
   problem:
    
   Qed