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: 0
      enrichment: match
      automaton:
       final states: {2,1}
       transitions:
        f80() -> 2*
        -{#,0}(2,4) -> 1*
        p0(3) -> 4*
        s0(2) -> 3*
        2 -> 4*
      problem:
       DPs:
        
       TRS:
        p(s(x)) -> x
      Qed