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
  Usable Rule Processor:
   DPs:
    -#(x,s(y)) -> p#(s(y))
    -#(x,s(y)) -> -#(x,p(s(y)))
   TRS:
    p(s(x)) -> x
   Matrix Interpretation Processor: dim=4
    
    usable rules:
     p(s(x)) -> x
    interpretation:
     [p#](x0) = [1 0 0 0]x0,
     
     [-#](x0, x1) = [0 0 0 1]x1,
     
               [0 0 1 0]  
               [0 1 1 0]  
     [p](x0) = [0 0 1 1]x0
               [1 0 0 0]  ,
     
               [0 0 0 1]     [0]
               [0 0 1 0]     [1]
     [s](x0) = [1 1 1 0]x0 + [1]
               [0 0 0 1]     [1]
    orientation:
     -#(x,s(y)) = [0 0 0 1]y + [1] >= [0 0 0 1]y = p#(s(y))
     
     -#(x,s(y)) = [0 0 0 1]y + [1] >= [0 0 0 1]y = -#(x,p(s(y)))
     
               [1 1 1 0]    [1]         
               [1 1 2 0]    [2]         
     p(s(x)) = [1 1 1 1]x + [2] >= x = x
               [0 0 0 1]    [0]         
    problem:
     DPs:
      
     TRS:
      p(s(x)) -> x
    Qed