YES

Problem:
 -(0(),y) -> 0()
 -(x,0()) -> x
 -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0())
 p(0()) -> 0()
 p(s(x)) -> x

Proof:
 DP Processor:
  DPs:
   -#(x,s(y)) -> p#(s(y))
   -#(x,s(y)) -> -#(x,p(s(y)))
  TRS:
   -(0(),y) -> 0()
   -(x,0()) -> x
   -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0())
   p(0()) -> 0()
   p(s(x)) -> x
  EDG Processor:
   DPs:
    -#(x,s(y)) -> p#(s(y))
    -#(x,s(y)) -> -#(x,p(s(y)))
   TRS:
    -(0(),y) -> 0()
    -(x,0()) -> x
    -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0())
    p(0()) -> 0()
    p(s(x)) -> x
   graph:
    -#(x,s(y)) -> -#(x,p(s(y))) -> -#(x,s(y)) -> p#(s(y))
    -#(x,s(y)) -> -#(x,p(s(y))) -> -#(x,s(y)) -> -#(x,p(s(y)))
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 2/4
    DPs:
     -#(x,s(y)) -> -#(x,p(s(y)))
    TRS:
     -(0(),y) -> 0()
     -(x,0()) -> x
     -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0())
     p(0()) -> 0()
     p(s(x)) -> x
    Usable Rule Processor:
     DPs:
      -#(x,s(y)) -> -#(x,p(s(y)))
     TRS:
      p(s(x)) -> x
     Bounds Processor:
      bound: 1
      enrichment: match-dp
      automaton:
       final states: {4}
       transitions:
        -{#,0}(3,6) -> 4*
        s0(2) -> 2*
        s0(1) -> 2*
        s0(3) -> 5*
        p0(5) -> 6*
        p0(2) -> 1*
        p0(1) -> 1*
        -{#,1}(3,10) -> 4*
        p1(9) -> 10*
        s1(2) -> 9*
        s1(1) -> 9*
        1 -> 10,3
        2 -> 10,1,3
        3 -> 6*
      problem:
       DPs:
        
       TRS:
        p(s(x)) -> x
      Qed