(VAR x y ) (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)))) )