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)-bounded by 0
       Automaton:
        {    a_0() -> 1*
         fac#_0(4) -> 2*
            s_0(1) -> 3*
            p_0(3) -> 4*
                 1 -> 4*}
       Strict:
        {}
       Qed