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
  TDG 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)) -> -#(x,p(s(y)))
    -#(x,s(y)) -> -#(x,p(s(y))) -> -#(x,s(y)) -> 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
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [-#](x0, x1) = 1/2x1,
      
      [if](x0, x1, x2) = 2,
      
      [p](x0) = 1/2x0,
      
      [greater](x0, x1) = 2x1 + 1/2,
      
      [s](x0) = 2x0 + 2,
      
      [-](x0, x1) = 5/2x0 + 2x1 + 2,
      
      [0] = 0
     orientation:
      -#(x,s(y)) = y + 1 >= 1/2y + 1/2 = -#(x,p(s(y)))
      
      -(0(),y) = 2y + 2 >= 0 = 0()
      
      -(x,0()) = 5/2x + 2 >= x = x
      
      -(x,s(y)) = 5/2x + 4y + 6 >= 2 = if(greater(x,s(y)),s(-(x,p(s(y)))),0())
      
      p(0()) = 0 >= 0 = 0()
      
      p(s(x)) = x + 1 >= x = x
     problem:
      DPs:
       
      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
     Qed