YES
TRS:
 {   p(s(x)) -> x,
  fact(s(x)) -> *(s(x), fact(p(s(x)))),
   fact(0()) -> s(0()),
  *(s(x), y) -> +(*(x, y), y),
   *(0(), y) -> 0(),
  +(x, s(y)) -> s(+(x, y)),
   +(x, 0()) -> x}
 DP:
  Strict:
   {fact#(s(x)) -> p#(s(x)),
    fact#(s(x)) -> fact#(p(s(x))),
    fact#(s(x)) -> *#(s(x), fact(p(s(x)))),
    *#(s(x), y) -> *#(x, y),
    *#(s(x), y) -> +#(*(x, y), y),
    +#(x, s(y)) -> +#(x, y)}
  Weak:
  {   p(s(x)) -> x,
   fact(s(x)) -> *(s(x), fact(p(s(x)))),
    fact(0()) -> s(0()),
   *(s(x), y) -> +(*(x, y), y),
    *(0(), y) -> 0(),
   +(x, s(y)) -> s(+(x, y)),
    +(x, 0()) -> x}
  EDG:
   {(*#(s(x), y) -> *#(x, y), *#(s(x), y) -> +#(*(x, y), y))
    (*#(s(x), y) -> *#(x, y), *#(s(x), y) -> *#(x, y))
    (fact#(s(x)) -> *#(s(x), fact(p(s(x)))), *#(s(x), y) -> +#(*(x, y), y))
    (fact#(s(x)) -> *#(s(x), fact(p(s(x)))), *#(s(x), y) -> *#(x, y))
    (*#(s(x), y) -> +#(*(x, y), y), +#(x, s(y)) -> +#(x, y))
    (+#(x, s(y)) -> +#(x, y), +#(x, s(y)) -> +#(x, y))
    (fact#(s(x)) -> fact#(p(s(x))), fact#(s(x)) -> p#(s(x)))
    (fact#(s(x)) -> fact#(p(s(x))), fact#(s(x)) -> fact#(p(s(x))))
    (fact#(s(x)) -> fact#(p(s(x))), fact#(s(x)) -> *#(s(x), fact(p(s(x)))))}
   SCCS:
    Scc:
     {+#(x, s(y)) -> +#(x, y)}
    Scc:
     {*#(s(x), y) -> *#(x, y)}
    Scc:
     {fact#(s(x)) -> fact#(p(s(x)))}
    SCC:
     Strict:
      {+#(x, s(y)) -> +#(x, y)}
     Weak:
     {   p(s(x)) -> x,
      fact(s(x)) -> *(s(x), fact(p(s(x)))),
       fact(0()) -> s(0()),
      *(s(x), y) -> +(*(x, y), y),
       *(0(), y) -> 0(),
      +(x, s(y)) -> s(+(x, y)),
       +(x, 0()) -> x}
     SPSC:
      Simple Projection:
       pi(+#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {*#(s(x), y) -> *#(x, y)}
     Weak:
     {   p(s(x)) -> x,
      fact(s(x)) -> *(s(x), fact(p(s(x)))),
       fact(0()) -> s(0()),
      *(s(x), y) -> +(*(x, y), y),
       *(0(), y) -> 0(),
      +(x, s(y)) -> s(+(x, y)),
       +(x, 0()) -> x}
     SPSC:
      Simple Projection:
       pi(*#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {fact#(s(x)) -> fact#(p(s(x)))}
     Weak:
     {   p(s(x)) -> x,
      fact(s(x)) -> *(s(x), fact(p(s(x)))),
       fact(0()) -> s(0()),
      *(s(x), y) -> +(*(x, y), y),
       *(0(), y) -> 0(),
      +(x, s(y)) -> s(+(x, y)),
       +(x, 0()) -> x}
     UR:
      {p(s(x)) -> x}
      BOUND:
       Bound: match(-raise)-DP-bounded by 0
       Automaton:
        {     a_0() -> 2*
         fact#_0(4) -> 1*
             s_0(2) -> 3*
             p_0(3) -> 4*
                  2 -> 4*}
       Strict:
        {}
       Qed