(0) Obligation:

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

f(x, a) → x
f(x, g(y)) → f(g(x), y)

Q is empty.