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)-bounded by 1
       Automaton:
        {    p_1(2) -> 3*
             p_0(1) -> 1*
             s_1(1) -> 2*
             s_0(1) -> 1*
         -#_1(1, 3) -> 1*
         -#_0(1, 1) -> 1*
                  1 -> 3*}
       Strict:
        {}
       Qed