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