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