(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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))))

Q is empty.