YES

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

Proof:
 DP Processor:
  DPs:
   +#(s(x),y) -> +#(x,y)
   -#(s(x),s(y)) -> -#(x,y)
  TRS:
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   -(0(),y) -> 0()
   -(x,0()) -> x
   -(s(x),s(y)) -> -(x,y)
  Usable Rule Processor:
   DPs:
    +#(s(x),y) -> +#(x,y)
    -#(s(x),s(y)) -> -#(x,y)
   TRS:
    
   Matrix Interpretation Processor: dim=4
    
    usable rules:
     
    interpretation:
     [-#](x0, x1) = [1 0 0 1]x0 + [1 1 1 1]x1,
     
     [+#](x0, x1) = [0 1 1 0]x0,
     
               [1 0 1 1]     [1]
               [0 0 1 1]     [0]
     [s](x0) = [0 1 1 0]x0 + [1]
               [1 1 0 1]     [0]
    orientation:
     +#(s(x),y) = [0 1 2 1]x + [1] >= [0 1 1 0]x = +#(x,y)
     
     -#(s(x),s(y)) = [2 1 1 2]x + [2 2 3 3]y + [3] >= [1 0 0 1]x + [1 1 1 1]y = -#(x,y)
    problem:
     DPs:
      
     TRS:
      
    Qed