YES
Time: 0.001783
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:
  DP:
   {      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)}
  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)}
  EDG:
   {(floop#(s x, y) -> *#(s x, y), *#(x, s y) -> +#(*(x, y), x))
    (floop#(s x, y) -> *#(s x, y), *#(x, s y) -> *#(x, y))
    (*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(*(x, y), x))
    (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y))
    (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), +#(x, s y) -> +#(x, y))
    (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
    (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> *#(s x, y))
    (floop#(s x, y) -> floop#(x, *(s x, y)), floop#(s x, y) -> floop#(x, *(s x, y)))
    (fac# s x -> fac# x, fac# 0() -> 1#())
    (fac# s x -> fac# x, fac# s x -> fac# x)
    (fac# s x -> fac# x, fac# s x -> *#(s x, fac x))}
   SCCS (4):
    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 (1):
     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 (1):
     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 (1):
     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 (1):
     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