(0) Obligation:

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

f(f(x, y, a), z, w) → f(z, w, f(y, x, z))

Q is empty.