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)))
  TDG 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)))
   graph:
    p#(s(s(x))) -> p#(s(x)) -> p#(s(s(x))) -> p#(s(x))
    fac#(s(x)) -> p#(s(x)) -> p#(s(s(x))) -> p#(s(x))
    fac#(s(x)) -> fac#(p(s(x))) -> fac#(s(x)) -> fac#(p(s(x)))
    fac#(s(x)) -> fac#(p(s(x))) -> fac#(s(x)) -> p#(s(x))
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 4/9
    DPs:
     fac#(s(x)) -> fac#(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)))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [fac#](x0) = x0 + 0,
      
      [0] = 0,
      
      [*](x0, x1) = -3x0 + 2x1 + 0,
      
      [p](x0) = -1x0 + 0,
      
      [fac](x0) = 3x0 + 1,
      
      [s](x0) = 3x0 + 1
     orientation:
      fac#(s(x)) = 3x + 1 >= 2x + 0 = fac#(p(s(x)))
      
      fac(s(x)) = 6x + 4 >= 5x + 3 = *(fac(p(s(x))),s(x))
      
      p(s(0())) = 2 >= 0 = 0()
      
      p(s(s(x))) = 5x + 3 >= 5x + 3 = s(p(s(x)))
     problem:
      DPs:
       
      TRS:
       fac(s(x)) -> *(fac(p(s(x))),s(x))
       p(s(0())) -> 0()
       p(s(s(x))) -> s(p(s(x)))
     Qed
    
    DPs:
     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)))
    Subterm Criterion Processor:
     simple projection:
      pi(p#) = 0
     problem:
      DPs:
       
      TRS:
       fac(s(x)) -> *(fac(p(s(x))),s(x))
       p(s(0())) -> 0()
       p(s(s(x))) -> s(p(s(x)))
     Qed