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

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.4):
  strict:
   
  weak:
   +(x,0()) -> x
   +(x,s(y)) -> s(+(x,y))
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   dbl(x) -> +(x,x)
   +(+(x,y),z) -> +(x,+(y,z))
   +(x,y) -> +(y,x)
   s(s(x)) -> s(x)
   s(x) -> s(s(x))
  original problem:
   +(x272,0()) -> x272
   +(0(),x274) -> x274
   +(s(x278),x277) -> s(+(x278,x277))
   +(x280,s(x279)) -> s(+(x280,x279))
   +(+(x283,x282),x281) -> +(x283,+(x282,x281))
   +(x304,x303) -> +(x303,x304)
   s(x410) -> s(s(x410))
   s(s(x434)) -> s(x434)
  critical peaks: 
   Shift Processor (no label):
    +(x272,0()) -> x272
    +(0(),x274) -> x274
    +(s(x278),x277) -> s(+(x278,x277))
    +(x280,s(x279)) -> s(+(x280,x279))
    +(+(x283,x282),x281) -> +(x283,+(x282,x281))
    +(x304,x303) -> +(x303,x304)
    s(x410) -> s(s(x410))
    s(s(x434)) -> s(x434)
    AT confluence processor
     Complete TRS T' of input TRS:
     +(x272,0()) -> x272
     +(0(),x274) -> x274
     +(s(x278),x277) -> s(+(x278,x277))
     +(x280,s(x279)) -> s(+(x280,x279))
     +(+(x283,x282),x281) -> +(x283,+(x282,x281))
     +(x304,x303) -> +(x303,x304)
     s(x410) -> s(s(x410))
     s(s(x434)) -> s(x434)
     
      T' = (P union S) with
     
      TRS P:+(+(x283,x282),x281) -> +(x283,+(x282,x281))
            +(x304,x303) -> +(x303,x304)
            s(x410) -> s(s(x410))
            s(s(x434)) -> s(x434)
     
      TRS S:+(x272,0()) -> x272
            +(0(),x274) -> x274
            +(s(x278),x277) -> s(+(x278,x277))
            +(x280,s(x279)) -> s(+(x280,x279))
     
     S is linear and P is reversible.
     
      CP(S,S) = 
     0() = 0(), s(x278) = s(+(x278,0())), s(x279) = s(+(0(),x279)), s(+(x1257,0())) = 
     s(x1257), s(+(x1259,s(x279))) = s(+(s(x1259),x279)), s(+(0(),x1262)) = 
     s(x1262), s(+(s(x278),x1264)) = s(+(x278,s(x1264)))
     
      CP(S,P union P^-1) = 
     +(x283,x282) = +(x283,+(x282,0())), +(x283,x281) = +(x283,+(0(),x281)), 
     x304 = +(0(),x304), +(x283,x282) = +(+(x283,x282),0()), x303 = +(0(),x303), 
     +(x282,x281) = +(0(),+(x282,x281)), x303 = +(x303,0()), +(x282,x281) = 
     +(+(0(),x282),x281), +(x283,x281) = +(+(x283,0()),x281), x304 = 
     +(x304,0()), +(s(+(x1347,x282)),x281) = +(s(x1347),+(x282,x281)), 
     s(+(x1349,x303)) = +(x303,s(x1349)), s(+(x1351,+(x282,x281))) = 
     +(+(s(x1351),x282),x281), +(x283,s(+(x1353,x281))) = +(+(x283,s(x1353)),x281), 
     s(+(x1355,x304)) = +(x304,s(x1355)), s(+(+(x283,x282),x1358)) = 
     +(x283,+(x282,s(x1358))), +(s(+(x283,x1360)),x281) = +(x283,+(s(x1360),x281)), 
     s(+(x304,x1362)) = +(s(x1362),x304), +(x283,s(+(x282,x1364))) = 
     +(+(x283,x282),s(x1364)), s(+(x303,x1366)) = +(s(x1366),x303)
     
      CP(P union P^-1,S) = 
     +(x1479,+(x1480,0())) = +(x1479,x1480), +(x1482,+(x1483,s(x279))) = 
     s(+(+(x1482,x1483),x279)), +(0(),x272) = x272, +(x274,0()) = x274, 
     +(x277,s(x278)) = s(+(x278,x277)), +(s(x279),x280) = s(+(x280,x279)), 
     +(s(s(x278)),x277) = s(+(x278,x277)), +(x280,s(s(x279))) = s(+(x280,x279)), 
     +(s(x1495),x277) = s(+(s(x1495),x277)), +(x280,s(x1496)) = s(+(x280,s(x1496))), 
     +(+(0(),x1498),x1499) = +(x1498,x1499), +(+(s(x278),x1501),x1502) = 
     s(+(x278,+(x1501,x1502))), +(s(x1511),x277) = s(+(s(x1511),x277)), 
     +(x280,s(x1512)) = s(+(x280,s(x1512)))
     
     
     We have to check termination of S:
     
     Bounds Processor:
      bound: 0
      enrichment: match
      automaton:
       final states: {2,1}
       transitions:
        s0(3) -> 2*
        +0(1,1) -> 3*
        f40() -> 1*
        1 -> 3*
        2 -> 3*
      problem:
       
      Qed