YES
TRS:
 {           1() -> s(0()),
        fac(0()) -> 1(),
        fac(0()) -> s(0()),
       fac(s(x)) -> *(s(x), fac(x)),
       *(x, 0()) -> 0(),
      *(x, s(y)) -> +(*(x, y), x),
   floop(0(), y) -> y,
  floop(s(x), y) -> floop(x, *(s(x), y)),
       +(x, 0()) -> x,
      +(x, s(y)) -> s(+(x, y))}
 DP:
  Strict:
   {      fac#(0()) -> 1#(),
         fac#(s(x)) -> fac#(x),
         fac#(s(x)) -> *#(s(x), fac(x)),
        *#(x, s(y)) -> *#(x, y),
        *#(x, s(y)) -> +#(*(x, y), x),
    floop#(s(x), y) -> *#(s(x), y),
    floop#(s(x), y) -> floop#(x, *(s(x), y)),
        +#(x, s(y)) -> +#(x, y)}
  Weak:
  {           1() -> s(0()),
         fac(0()) -> 1(),
         fac(0()) -> s(0()),
        fac(s(x)) -> *(s(x), fac(x)),
        *(x, 0()) -> 0(),
       *(x, s(y)) -> +(*(x, y), x),
    floop(0(), y) -> y,
   floop(s(x), y) -> floop(x, *(s(x), y)),
        +(x, 0()) -> x,
       +(x, s(y)) -> s(+(x, y))}
  EDG:
   {(floop#(s(x), y) -> floop#(x, *(s(x), y)), floop#(s(x), y) -> floop#(x, *(s(x), y)))
    (floop#(s(x), y) -> floop#(x, *(s(x), y)), floop#(s(x), y) -> *#(s(x), y))
    (fac#(s(x)) -> fac#(x), fac#(s(x)) -> *#(s(x), fac(x)))
    (fac#(s(x)) -> fac#(x), fac#(s(x)) -> fac#(x))
    (fac#(s(x)) -> fac#(x), fac#(0()) -> 1#())
    (fac#(s(x)) -> *#(s(x), fac(x)), *#(x, s(y)) -> +#(*(x, y), x))
    (fac#(s(x)) -> *#(s(x), fac(x)), *#(x, s(y)) -> *#(x, y))
    (+#(x, s(y)) -> +#(x, y), +#(x, s(y)) -> +#(x, y))
    (*#(x, s(y)) -> *#(x, y), *#(x, s(y)) -> *#(x, y))
    (*#(x, s(y)) -> *#(x, y), *#(x, s(y)) -> +#(*(x, y), x))
    (floop#(s(x), y) -> *#(s(x), y), *#(x, s(y)) -> *#(x, y))
    (floop#(s(x), y) -> *#(s(x), y), *#(x, s(y)) -> +#(*(x, y), x))
    (*#(x, s(y)) -> +#(*(x, y), x), +#(x, s(y)) -> +#(x, y))}
   SCCS:
    Scc:
     {+#(x, s(y)) -> +#(x, y)}
    Scc:
     {floop#(s(x), y) -> floop#(x, *(s(x), y))}
    Scc:
     {*#(x, s(y)) -> *#(x, y)}
    Scc:
     {fac#(s(x)) -> fac#(x)}
    SCC:
     Strict:
      {+#(x, s(y)) -> +#(x, y)}
     Weak:
     {           1() -> s(0()),
            fac(0()) -> 1(),
            fac(0()) -> s(0()),
           fac(s(x)) -> *(s(x), fac(x)),
           *(x, 0()) -> 0(),
          *(x, s(y)) -> +(*(x, y), x),
       floop(0(), y) -> y,
      floop(s(x), y) -> floop(x, *(s(x), y)),
           +(x, 0()) -> x,
          +(x, s(y)) -> s(+(x, y))}
     SPSC:
      Simple Projection:
       pi(+#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {floop#(s(x), y) -> floop#(x, *(s(x), y))}
     Weak:
     {           1() -> s(0()),
            fac(0()) -> 1(),
            fac(0()) -> s(0()),
           fac(s(x)) -> *(s(x), fac(x)),
           *(x, 0()) -> 0(),
          *(x, s(y)) -> +(*(x, y), x),
       floop(0(), y) -> y,
      floop(s(x), y) -> floop(x, *(s(x), y)),
           +(x, 0()) -> x,
          +(x, s(y)) -> s(+(x, y))}
     SPSC:
      Simple Projection:
       pi(floop#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {*#(x, s(y)) -> *#(x, y)}
     Weak:
     {           1() -> s(0()),
            fac(0()) -> 1(),
            fac(0()) -> s(0()),
           fac(s(x)) -> *(s(x), fac(x)),
           *(x, 0()) -> 0(),
          *(x, s(y)) -> +(*(x, y), x),
       floop(0(), y) -> y,
      floop(s(x), y) -> floop(x, *(s(x), y)),
           +(x, 0()) -> x,
          +(x, s(y)) -> s(+(x, y))}
     SPSC:
      Simple Projection:
       pi(*#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {fac#(s(x)) -> fac#(x)}
     Weak:
     {           1() -> s(0()),
            fac(0()) -> 1(),
            fac(0()) -> s(0()),
           fac(s(x)) -> *(s(x), fac(x)),
           *(x, 0()) -> 0(),
          *(x, s(y)) -> +(*(x, y), x),
       floop(0(), y) -> y,
      floop(s(x), y) -> floop(x, *(s(x), y)),
           +(x, 0()) -> x,
          +(x, s(y)) -> s(+(x, y))}
     SPSC:
      Simple Projection:
       pi(fac#) = 0
      Strict:
       {}
      Qed