YES
TRS:
 {minus(minus(x)) -> x,
   minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y)))),
   minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y)))),
      f(minus(x)) -> minus(minus(minus(f(x))))}
 DP:
  Strict:
   {minus#(*(x, y)) -> minus#(x),
    minus#(*(x, y)) -> minus#(y),
    minus#(*(x, y)) -> minus#(minus(x)),
    minus#(*(x, y)) -> minus#(minus(y)),
    minus#(*(x, y)) -> minus#(minus(minus(x))),
    minus#(*(x, y)) -> minus#(minus(minus(y))),
    minus#(+(x, y)) -> minus#(x),
    minus#(+(x, y)) -> minus#(y),
    minus#(+(x, y)) -> minus#(minus(x)),
    minus#(+(x, y)) -> minus#(minus(y)),
    minus#(+(x, y)) -> minus#(minus(minus(x))),
    minus#(+(x, y)) -> minus#(minus(minus(y))),
       f#(minus(x)) -> minus#(minus(minus(f(x)))),
       f#(minus(x)) -> minus#(minus(f(x))),
       f#(minus(x)) -> minus#(f(x)),
       f#(minus(x)) -> f#(x)}
  Weak:
  {minus(minus(x)) -> x,
    minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y)))),
    minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y)))),
       f(minus(x)) -> minus(minus(minus(f(x))))}
  EDG:
   {
    (minus#(+(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (minus#(+(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(x))
    (minus#(+(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(+(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(x))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(x))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(x))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(x))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(x))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(+(x, y)) -> minus#(minus(y)))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(+(x, y)) -> minus#(minus(x)))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(+(x, y)) -> minus#(y))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(+(x, y)) -> minus#(x))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(*(x, y)) -> minus#(minus(y)))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(*(x, y)) -> minus#(minus(x)))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(*(x, y)) -> minus#(y))
    (f#(minus(x)) -> minus#(minus(minus(f(x)))), minus#(*(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(x))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(+(x, y)) -> minus#(x))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(minus(minus(y))), minus#(*(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(x))
    (f#(minus(x)) -> f#(x), f#(minus(x)) -> f#(x))
    (f#(minus(x)) -> f#(x), f#(minus(x)) -> minus#(f(x)))
    (f#(minus(x)) -> f#(x), f#(minus(x)) -> minus#(minus(f(x))))
    (f#(minus(x)) -> f#(x), f#(minus(x)) -> minus#(minus(minus(f(x)))))
    (minus#(+(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(x))
    (minus#(+(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(x), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(+(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(x))
    (minus#(+(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(x), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(*(x, y)) -> minus#(x))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(*(x, y)) -> minus#(y))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(*(x, y)) -> minus#(minus(x)))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(*(x, y)) -> minus#(minus(y)))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(+(x, y)) -> minus#(x))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(+(x, y)) -> minus#(y))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(+(x, y)) -> minus#(minus(x)))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(+(x, y)) -> minus#(minus(y)))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (f#(minus(x)) -> minus#(minus(f(x))), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(x))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(x))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(y))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(+(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(minus(minus(x))), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (f#(minus(x)) -> minus#(f(x)), minus#(*(x, y)) -> minus#(x))
    (f#(minus(x)) -> minus#(f(x)), minus#(*(x, y)) -> minus#(y))
    (f#(minus(x)) -> minus#(f(x)), minus#(*(x, y)) -> minus#(minus(x)))
    (f#(minus(x)) -> minus#(f(x)), minus#(*(x, y)) -> minus#(minus(y)))
    (f#(minus(x)) -> minus#(f(x)), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (f#(minus(x)) -> minus#(f(x)), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (f#(minus(x)) -> minus#(f(x)), minus#(+(x, y)) -> minus#(x))
    (f#(minus(x)) -> minus#(f(x)), minus#(+(x, y)) -> minus#(y))
    (f#(minus(x)) -> minus#(f(x)), minus#(+(x, y)) -> minus#(minus(x)))
    (f#(minus(x)) -> minus#(f(x)), minus#(+(x, y)) -> minus#(minus(y)))
    (f#(minus(x)) -> minus#(f(x)), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (f#(minus(x)) -> minus#(f(x)), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(minus(x)), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(minus(y)), minus#(+(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(y), minus#(*(x, y)) -> minus#(minus(minus(y))))
    (minus#(*(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(x))
    (minus#(*(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(y))
    (minus#(*(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(minus(x)))
    (minus#(*(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(minus(y)))
    (minus#(*(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(minus(minus(x))))
    (minus#(*(x, y)) -> minus#(y), minus#(+(x, y)) -> minus#(minus(minus(y))))
   }
   SCCS:
    Scc:
     {f#(minus(x)) -> f#(x)}
    Scc:
     {minus#(*(x, y)) -> minus#(x),
      minus#(*(x, y)) -> minus#(y),
      minus#(*(x, y)) -> minus#(minus(x)),
      minus#(*(x, y)) -> minus#(minus(y)),
      minus#(*(x, y)) -> minus#(minus(minus(x))),
      minus#(*(x, y)) -> minus#(minus(minus(y))),
      minus#(+(x, y)) -> minus#(x),
      minus#(+(x, y)) -> minus#(y),
      minus#(+(x, y)) -> minus#(minus(x)),
      minus#(+(x, y)) -> minus#(minus(y)),
      minus#(+(x, y)) -> minus#(minus(minus(x))),
      minus#(+(x, y)) -> minus#(minus(minus(y)))}
    SCC:
     Strict:
      {f#(minus(x)) -> f#(x)}
     Weak:
     {minus(minus(x)) -> x,
       minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y)))),
       minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y)))),
          f(minus(x)) -> minus(minus(minus(f(x))))}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {minus#(*(x, y)) -> minus#(x),
       minus#(*(x, y)) -> minus#(y),
       minus#(*(x, y)) -> minus#(minus(x)),
       minus#(*(x, y)) -> minus#(minus(y)),
       minus#(*(x, y)) -> minus#(minus(minus(x))),
       minus#(*(x, y)) -> minus#(minus(minus(y))),
       minus#(+(x, y)) -> minus#(x),
       minus#(+(x, y)) -> minus#(y),
       minus#(+(x, y)) -> minus#(minus(x)),
       minus#(+(x, y)) -> minus#(minus(y)),
       minus#(+(x, y)) -> minus#(minus(minus(x))),
       minus#(+(x, y)) -> minus#(minus(minus(y)))}
     Weak:
     {minus(minus(x)) -> x,
       minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y)))),
       minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y)))),
          f(minus(x)) -> minus(minus(minus(f(x))))}
     POLY:
      Argument Filtering:
       pi(f) = [], pi(+) = [0,1], pi(*) = [0,1], pi(minus#) = 0, pi(minus) = 0
      Usable Rules:
       {}
      Interpretation:
       [+](x0, x1) = x0 + x1 + 1,
       [*](x0, x1) = x0 + x1 + 1
      Strict:
       {}
      Weak:
       {minus(minus(x)) -> x,
         minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y)))),
         minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y)))),
            f(minus(x)) -> minus(minus(minus(f(x))))}
      Qed