YES

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

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