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)
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [minus#](x0, x1) = x1,
    
    [p#](x0) = 1,
    
    [minus](x0, x1) = 1x0 + x1 + 0,
    
    [s](x0) = 7x0 + 4,
    
    [p](x0) = -6x0 + 2,
    
    [0] = 0
   orientation:
    minus#(x,s(y)) = 7y + 4 >= 1 = p#(x)
    
    minus#(x,s(y)) = 7y + 4 >= y = minus#(p(x),y)
    
    p(0()) = 2 >= 0 = 0()
    
    p(s(x)) = 1x + 2 >= x = x
    
    minus(x,0()) = 1x + 0 >= x = x
    
    minus(x,s(y)) = 1x + 7y + 4 >= -5x + y + 3 = minus(p(x),y)
   problem:
    DPs:
     
    TRS:
     p(0()) -> 0()
     p(s(x)) -> x
     minus(x,0()) -> x
     minus(x,s(y)) -> minus(p(x),y)
   Qed