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)))
    Matrix Interpretation Processor: dim=2
     
     interpretation:
      [fac#](x0) = [0 2]x0,
      
            [0]
      [0] = [0],
      
                    [1 0]     [0 0]  
      [*](x0, x1) = [0 0]x0 + [1 2]x1,
      
                [1 0]  
      [p](x0) = [1 0]x0,
      
                  [0 0]     [1]
      [fac](x0) = [3 2]x0 + [0],
      
                [0 1]     [0]
      [s](x0) = [0 2]x0 + [1]
     orientation:
      fac#(s(x)) = [0 4]x + [2] >= [0 2]x = fac#(p(s(x)))
      
                  [0 0]    [1]    [0 0]    [1]                       
      fac(s(x)) = [0 7]x + [2] >= [0 5]x + [2] = *(fac(p(s(x))),s(x))
      
                  [0]    [0]      
      p(s(0())) = [0] >= [0] = 0()
      
                   [0 2]    [1]    [0 1]    [0]             
      p(s(s(x))) = [0 2]x + [1] >= [0 2]x + [1] = 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)))
    KBO Processor:
     argument filtering:
      pi(s) = [0]
      pi(fac) = []
      pi(p) = 0
      pi(*) = 0
      pi(0) = []
      pi(p#) = [0]
     weight function:
      w0 = 1
      w(p#) = w(0) = w(*) = w(fac) = 1
      w(p) = w(s) = 0
     precedence:
      p# ~ fac ~ s > 0 ~ * ~ p
     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