YES
TRS:
 {  p(s(x)) -> x,
  fac(s(x)) -> times(s(x), fac(p(s(x)))),
   fac(0()) -> s(0())}
 DP:
  Strict:
   {fac#(s(x)) -> p#(s(x)),
    fac#(s(x)) -> fac#(p(s(x)))}
  Weak:
  {  p(s(x)) -> x,
   fac(s(x)) -> times(s(x), fac(p(s(x)))),
    fac(0()) -> s(0())}
  EDG:
   {(fac#(s(x)) -> fac#(p(s(x))), fac#(s(x)) -> p#(s(x)))
    (fac#(s(x)) -> fac#(p(s(x))), fac#(s(x)) -> fac#(p(s(x))))}
   SCCS:
    Scc:
     {fac#(s(x)) -> fac#(p(s(x)))}
    SCC:
     Strict:
      {fac#(s(x)) -> fac#(p(s(x)))}
     Weak:
     {  p(s(x)) -> x,
      fac(s(x)) -> times(s(x), fac(p(s(x)))),
       fac(0()) -> s(0())}
     UR:
      {p(s(x)) -> x}
      BOUND:
       Bound: match(-raise)-DP-bounded by 1
       Automaton:
        {fac#_1(13) -> 14*
         fac#_0(10) -> 4*
            s_1(17) -> 18*
            s_1(15) -> 16*
            s_1(11) -> 12*
            s_0(10) -> 9*
             s_0(9) -> 9*
             s_0(7) -> 9*
            p_1(12) -> 13*
            p_0(10) -> 7*
             p_0(9) -> 10*
             p_0(7) -> 7*
                 18 -> 12*
                 17 -> 13*
                 16 -> 12*
                 15 -> 13*
                 14 -> 4*
                 11 -> 13*
                 10 -> 17 | 7
                  9 -> 15 | 10 | 7
                  7 -> 11 | 10}
       Strict:
        {}
       Qed