YES
Time: 0.010069
TRS:
 {  bin(x, 0()) -> s 0(),
  bin(s x, s y) -> +(bin(x, s y), bin(x, y)),
  bin(0(), s y) -> 0()}
 DP:
  DP:
   {bin#(s x, s y) -> bin#(x, y),
    bin#(s x, s y) -> bin#(x, s y)}
  TRS:
  {  bin(x, 0()) -> s 0(),
   bin(s x, s y) -> +(bin(x, s y), bin(x, y)),
   bin(0(), s y) -> 0()}
  UR:
   {}
   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))}
    STATUS:
     arrows: 0.000000
     SCCS (1):
      Scc:
       {bin#(s x, s y) -> bin#(x, y),
        bin#(s x, s y) -> bin#(x, s y)}
      
      SCC (2):
       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()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [bin](x0, x1) = 0,
         
         [+](x0, x1) = 0,
         
         [s](x0) = x0 + 1,
         
         [0] = 1,
         
         [bin#](x0, x1) = x0 + 1
        Strict:
         bin#(s x, s y) -> bin#(x, s y)
         2 + 1x + 0y >= 1 + 1x + 0y
         bin#(s x, s y) -> bin#(x, y)
         2 + 1x + 0y >= 1 + 1x + 0y
        Weak:
         bin(0(), s y) -> 0()
         0 + 0y >= 1
         bin(s x, s y) -> +(bin(x, s y), bin(x, y))
         0 + 0x + 0y >= 0 + 0x + 0y
         bin(x, 0()) -> s 0()
         0 + 0x >= 2
       Qed