YES

Problem:
 fac(s(x)) -> *(fac(p(s(x))),s(x))
 p(s(0())) -> 0()
 p(s(s(x))) -> s(p(s(x)))

Proof:
 DP Processor:
  DPs:
   fac#(s(x)) -> p#(s(x))
   fac#(s(x)) -> fac#(p(s(x)))
   p#(s(s(x))) -> p#(s(x))
  TRS:
   fac(s(x)) -> *(fac(p(s(x))),s(x))
   p(s(0())) -> 0()
   p(s(s(x))) -> s(p(s(x)))
  Usable Rule Processor:
   DPs:
    fac#(s(x)) -> p#(s(x))
    fac#(s(x)) -> fac#(p(s(x)))
    p#(s(s(x))) -> p#(s(x))
   TRS:
    p(s(0())) -> 0()
    p(s(s(x))) -> s(p(s(x)))
   Matrix Interpretation Processor: dim=2
    
    usable rules:
     p(s(0())) -> 0()
     p(s(s(x))) -> s(p(s(x)))
    interpretation:
     [p#](x0) = [0 1]x0,
     
     [fac#](x0) = [0 2]x0 + [1],
     
           [0]
     [0] = [2],
     
               [1 0]     [3]
     [p](x0) = [1 0]x0 + [0],
     
               [0 2]     [0]
     [s](x0) = [0 2]x0 + [2]
    orientation:
     fac#(s(x)) = [0 4]x + [5] >= [0 2]x + [2] = p#(s(x))
     
     fac#(s(x)) = [0 4]x + [5] >= [0 4]x + [1] = fac#(p(s(x)))
     
     p#(s(s(x))) = [0 4]x + [6] >= [0 2]x + [2] = p#(s(x))
     
                 [7]    [0]      
     p(s(0())) = [4] >= [2] = 0()
     
                  [0 4]    [7]    [0 4]    [0]             
     p(s(s(x))) = [0 4]x + [4] >= [0 4]x + [2] = s(p(s(x)))
    problem:
     DPs:
      
     TRS:
      p(s(0())) -> 0()
      p(s(s(x))) -> s(p(s(x)))
    Qed