YES
TRS:
 { -(x, 0()) -> x,
  -(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0()),
   -(0(), y) -> 0(),
      p(0()) -> 0(),
     p(s(x)) -> x}
 DP:
  Strict:
   {-#(x, s(y)) -> -#(x, p(s(y))),
    -#(x, s(y)) -> p#(s(y))}
  Weak:
  { -(x, 0()) -> x,
   -(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0()),
    -(0(), y) -> 0(),
       p(0()) -> 0(),
      p(s(x)) -> x}
  EDG:
   {(-#(x, s(y)) -> -#(x, p(s(y))), -#(x, s(y)) -> -#(x, p(s(y))))
    (-#(x, s(y)) -> -#(x, p(s(y))), -#(x, s(y)) -> p#(s(y)))}
   SCCS:
    Scc:
     {-#(x, s(y)) -> -#(x, p(s(y)))}
    SCC:
     Strict:
      {-#(x, s(y)) -> -#(x, p(s(y)))}
     Weak:
     { -(x, 0()) -> x,
      -(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0()),
       -(0(), y) -> 0(),
          p(0()) -> 0(),
         p(s(x)) -> x}
     UR:
      {p(s(x)) -> x}
      BOUND:
       Bound: match(-raise)-DP-bounded by 1
       Automaton:
        {     p_1(11) -> 12*
              p_0(10) -> 8*
               p_0(9) -> 10*
               p_0(8) -> 8*
              s_1(10) -> 11*
               s_1(9) -> 11*
               s_1(8) -> 11*
              s_0(10) -> 9*
               s_0(9) -> 9*
               s_0(8) -> 9*
         -#_1(10, 12) -> 4*
          -#_1(9, 12) -> 4*
          -#_1(8, 12) -> 4*
         -#_0(10, 10) -> 4*
          -#_0(9, 10) -> 4*
          -#_0(8, 10) -> 4*
                   10 -> 8*
                    9 -> 10 | 8
                    8 -> 12 | 10}
       Strict:
        {}
       Qed