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