YES

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

Proof:
 DP Processor:
  DPs:
   minus#(x,s(y)) -> p#(x)
   minus#(x,s(y)) -> minus#(p(x),y)
  TRS:
   p(0()) -> 0()
   p(s(x)) -> x
   minus(x,0()) -> x
   minus(x,s(y)) -> minus(p(x),y)
  Usable Rule Processor:
   DPs:
    minus#(x,s(y)) -> p#(x)
    minus#(x,s(y)) -> minus#(p(x),y)
   TRS:
    p(0()) -> 0()
    p(s(x)) -> x
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [minus#](x0, x1) = x1,
     
     [p#](x0) = 0,
     
     [s](x0) = 1x0 + 1,
     
     [p](x0) = -9x0 + 0,
     
     [0] = 8
    orientation:
     minus#(x,s(y)) = 1y + 1 >= 0 = p#(x)
     
     minus#(x,s(y)) = 1y + 1 >= y = minus#(p(x),y)
     
     p(0()) = 0 >= 8 = 0()
     
     p(s(x)) = -8x + 0 >= x = x
    problem:
     DPs:
      
     TRS:
      p(0()) -> 0()
      p(s(x)) -> x
    Qed