YES
TRS:
 {    bin(x, 0()) -> s(0()),
  bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)),
   bin(0(), s(y)) -> 0()}
 DP:
  Strict:
   {bin#(s(x), s(y)) -> bin#(x, y),
    bin#(s(x), s(y)) -> bin#(x, s(y))}
  Weak:
  {    bin(x, 0()) -> s(0()),
   bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)),
    bin(0(), s(y)) -> 0()}
  EDG:
   {(bin#(s(x), s(y)) -> bin#(x, y), bin#(s(x), s(y)) -> bin#(x, s(y)))
    (bin#(s(x), s(y)) -> bin#(x, y), bin#(s(x), s(y)) -> bin#(x, y))
    (bin#(s(x), s(y)) -> bin#(x, s(y)), bin#(s(x), s(y)) -> bin#(x, y))
    (bin#(s(x), s(y)) -> bin#(x, s(y)), bin#(s(x), s(y)) -> bin#(x, s(y)))}
   SCCS:
    Scc:
     {bin#(s(x), s(y)) -> bin#(x, y),
      bin#(s(x), s(y)) -> bin#(x, s(y))}
    SCC:
     Strict:
      {bin#(s(x), s(y)) -> bin#(x, y),
       bin#(s(x), s(y)) -> bin#(x, s(y))}
     Weak:
     {    bin(x, 0()) -> s(0()),
      bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)),
       bin(0(), s(y)) -> 0()}
     SPSC:
      Simple Projection:
       pi(bin#) = 0
      Strict:
       {bin#(s(x), s(y)) -> bin#(x, y)}
      EDG:
       {(bin#(s(x), s(y)) -> bin#(x, y), bin#(s(x), s(y)) -> bin#(x, y))}
       SCCS:
        Scc:
         {bin#(s(x), s(y)) -> bin#(x, y)}
        SCC:
         Strict:
          {bin#(s(x), s(y)) -> bin#(x, y)}
         Weak:
         {    bin(x, 0()) -> s(0()),
          bin(s(x), s(y)) -> +(bin(x, s(y)), bin(x, y)),
           bin(0(), s(y)) -> 0()}
         SPSC:
          Simple Projection:
           pi(bin#) = 0
          Strict:
           {}
          Qed